Idris - lazy evaluation Ausgabe

Question

dieses Programm vor:

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 

da die rechte Seite >>== faul deklariert und !(nothing "a") kehrt Nothing, ich würde erwarten, dass die rechte Seite von >>== würde nicht ausgewertet werden.

Aber eigentlich ist es ausgewertet werden, und ich kann nicht verstehen, warum ...

Allgemeiner gesagt, ich versuche Eff Berechnungen verketten, die vielleicht zurückkehren und die Ausführung zu stoppen, als ich die ersten Nothing

bekommen

Answer 1

Desugar der! Notation.

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

Klar "a", "b" und "Ende" werden alle gedruckt werden, aber func kann nicht ausgewertet werden.

Ich denke, Sie müssen definieren >>== auf (einige) Eff Werte, anstatt direkt auf Maybe s.

HTH