3
このプログラムを考えてみましょ遅延評価の問題:イドリス -
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
されているので、私は>>==
の右手側は評価されないだろうと予想されます。
しかし、実際には、評価を受けるん、と私は理由を理解することはできません...私は最初Nothing
より広く、私は多分返すEff
計算を連結し、実行を停止しようとしています
私が実際に希望することは計算が '「b」は、'印刷されないこと「」 '、'ので、何も後に停止することです。私は 'do'表記が間違った文脈、すなわち' Maybe'の代わりに 'Eff'で働いているので、これは起こらないと思います。ハスケルでは、私は 'MaybeT'モナドトランスを使ってこの問題に取り組んでいますが、Idrisに類似したものがありますか?従属型は私に何かクリーナーをさせることができるのですか? – marcosh
'EXCEPTION()'エフェクトを追加します。 '何も' 'raise()'を呼び出すと、あなたが何を持っていても動作する定義済みのハンドラがすでにあります。 –