Idris - 懒惰的评估问题

Question

考虑这个程序：

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

由于>>== 的右侧被声明为惰性并且!(nothing "a") 返回Nothing，我希望>>== 的右侧不会被评估。

但实际上它确实得到了评​​估，我不明白为什么......

更广泛地说，我正在尝试连接可能返回的 Eff 计算，并在我得到第一个 Nothing 时停止执行

Answer 1

脱糖！符号。

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

显然“a”、“b”和“end”都会被打印出来，但func可能不会被评估。

我认为您需要定义 >>== 才能作用于（某些）Eff 值，而不是直接作用于 Maybes。

HTH