Idrisの連鎖効果

Question

少しのIdrisとそのエフェクトのチュートリアルの例を演奏した後、私は最終的にどのように連鎖するのかを考え出しました。鎖が正しい単語であるかどうかはわかりませんが、基本的には別の意味で1つの効果が実装されていることを意味します。

この例では、Lowerと呼ぶエフェクトがあります。直接IOを呼び出します。それから私はHigherと呼ぶEffectを持っています。私は、IOを直接呼び出すのではなく、Lowerを使ってハンドラを実装しようと考えています。

私は最終的にそれは私が把握カント小さな問題で動作するようになった：

module Main 

import Effects 

data Lower : Effect where 

    LLog : String -> Lower()() (\_ =>()) 
    LGreet : String -> Lower()() (\_ =>()) 
    LFarewell : String -> Lower()() (\_ =>()) 

Handler Lower IO where 

    handle _ (LLog msg) k = do 
    putStrLn $ "log: " ++ msg 
    k()() 

    handle _ (LGreet msg) k = do 
    putStrLn $ "greeting: " ++ msg 
    k()() 

    handle _ (LFarewell msg) k = do 
    putStrLn $ "farewell: " ++ msg 
    k()() 

LOWER : EFFECT 
LOWER = MkEff() Lower 

data Higher : Effect where 

    HGreet : String -> Higher()() (\_ =>()) 
    HFarewell : String -> Higher()() (\_ =>()) 

lgreet : String -> Eff() [LOWER] 
lgreet msg = do 
    call $ LGreet msg 
    call $ LLog "greeting received" 

lfarewell : String -> Eff() [LOWER] 
lfarewell msg = do 
    call $ LFarewell msg 
    call $ LLog "farewell received" 

(Monad m, Handler Lower m) => Handler Higher m where 

    handle _ (HGreet msg) k = 
    do 
     runInit [()] (lgreet msg) 
     k()() 

    {- FIXME: This doesnt work, why ? 
    where 
     lgreet : String -> Eff() [LOWER] 
     lgreet msg = do 
     call $ LGreet msg 
     call $ LLog "greeting received" 
    -} 

    handle _ (HFarewell msg) k = 
    do 
     runInit [()] (lfarewell msg) 
     k()() 

HIGHER : EFFECT 
HIGHER = MkEff() Higher 

dummy : Eff() [HIGHER] 
dummy = do 
    call $ HGreet "hi" 
    call $ HFarewell "bye" 

main : IO() 
main = do 
    runInit [()] dummy 

は、私が上記の作っFIXMEコメントを参照してください。

When checking type of Effects.Main.Higher, m implementation of Effects.Handler, method handle, lgreet: 
Type mismatch between 
     () (Type of (\underscore =>()) x) 
and 
     Type (Expected type) 
chain1.idr:64:6:When checking right hand side of main with expected type 
     IO() 

Can't find implementation for Handler Higher IO 

はそれが正常に動作外で、私はそれを維持する場合のに対して、意図した出力を生成します：私は、where句内のlgreet定義を移動した場合、それは次のエラーメッセージでコンパイルに失敗し

greeting: hi 
log: greeting received 
farewell: bye 
log: farewell received 

Answer 1

[OK]をが見つから問題、イドリスはトラブル高いデータの定義に、この関数の型を推論をしている：明示的に型を指定

\_ =>() 

は、問題を修正：

data Higher : Effect where 

    HGreet : String -> Higher Unit Unit (the (Unit->Type) (\_ =>())) 
    HFarewell : String -> Higher()() (the (Unit->Type) (\_ =>()))