idris - Idris 中的链式效应

Question

在玩了一下 Idris 及其效果教程示例后，我终于弄清楚了如何链接效果。不确定链是否是正确的词，但我基本上是指一种效果是根据另一种效果实现的。

在这个例子中，我有一个效果，我称之为 Lower。它直接调用IO。然后我有一个我称之为 Higher 的 Effect，我打算使用 Lower 来实现它的处理程序而不是直接调用 IO(或者就此而言，在它附近的任何地方提到 IO)。

我终于解决了一个我无法弄清楚的小问题:

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 评论。如果我将 lgreet 定义移动到 where 子句中，它将无法编译并显示以下错误消息:

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

而如果我把它放在外面它工作正常，产生预期的输出:

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

Answer 1

好的，问题找到了，idris 在推断 data Higher 定义中这个函数的类型时遇到了问题:

\_ => ()

明确指定类型可以解决问题:

data Higher : Effect where

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