Idris - question de l'évaluation paresseuse

Question

Tenir compte de ce programme:

module test 

import Effects 
import Effect.StdIO 

(>>==) : Maybe a -> Lazy (a -> Maybe b) -> Maybe b 
(>>==) Nothing (Delay map) = Nothing 
(>>==) (Just x) (Delay map) = map x 

nothing : String -> Eff (Maybe String) [STDIO] 
nothing s = do 
    putStrLn s 
    pure Nothing 

func : Maybe String -> String -> Maybe String 
func Nothing _ = Nothing 
func (Just s) t = Just (s ++ t) 

test : Eff() [STDIO] 
test = do 
    let m = !(nothing "a") >>== (func !(nothing "b")) 
    putStrLn "end" 

main : IO() 
main = run test 

depuis le côté droit de >>== est déclaré retours paresseux et !(nothing "a")Nothing, je me attends à ce que le côté droit de >>== ne serait pas évalué.

Mais en réalité, il ne s'évalué, et je ne comprends pas pourquoi ...

De façon plus générale, je suis en train de concaténer Eff calculs qui renvoient peut-être et d'arrêter l'exécution quand je reçois le premier Nothing

Answer 1

Desugar the! notation.

test = do 
    x <- nothing "a" 
    y <- nothing "b" 
    let m = x >>== (func y) 
    putStrLn "end" 

Il est clair que "a", "b" et "fin" seront tous imprimés, mais func ne peuvent pas être évalués.

Je pense que vous devrez définir >>== pour agir sur (certaines) Eff valeurs, plutôt que directement sur Maybe s.

HTH