haskell - 如何使用自由(或更自由)的单子(monad)对采用单子(monad)参数的 Action 进行编码？

Question

大多数 monadic 函数采用纯参数并返回一个 monadic 值。但是有一些也需要单子(monad)参数，例如:

mplus :: (MonadPlus m) => m a -> m a -> m a

finally :: IO a -> IO b -> IO a

forkIO :: m () -> m ThreadId

-- | From Control.Monad.Parallel
forkExec :: m a -> m (m a)

他们每个人似乎都提出了一个不同的问题，我无法掌握如何 的通用方法使用自由单子(monad)对此类 Action 进行编码。

在这两个 finally和 forkIO问题是 monadic 参数的类型与结果不同。但是免费需要它们是相同的类型，如 IO a被编码类型的类型变量替换，如 data MyFunctor x = Finally x x x ，它只会编码 IO a -> IO a -> IO a .

在 From zero to cooperative threads in 33 lines of Haskell code作者使用 Fork next next实现

cFork :: (Monad m) => Thread m Bool
cFork = liftF (Fork False True)

然后用它来实现

fork :: (Monad m) => Thread m a -> Thread m ()

其中输入和输出具有不同的类型。
但我不明白这是使用某个过程得出的，还是只是一个适用于这个特定目的的临时想法。

mplus特别令人困惑:天真的编码为

data F b = MZero | MPlus b b

分布在 >>=和 suggested better implementation更复杂。还有一个免费的 MonadPlus 的本地实现was removed from free .

在 freer它是通过添加来实现的

data NonDetEff a where
  MZero :: NonDetEff a
  MPlus :: NonDetEff Bool

为什么是 MPlus NonDetEff Bool而不是 NonDetEff a a ?有没有办法让它与 Free 一起工作？ ，我们需要数据类型是仿函数，而不是使用 CoYoneda functor ?

对于 forkExec我完全不知道如何进行。

Answer 1

我只会回答 Freer单子(monad)部分。回想一下定义:

data Freer f b where
    Pure :: b -> Freer f b
    Roll :: f a -> (a -> Freer f b) -> Freer f b

现在有了

data NonDetEff a where
  MZero :: NonDetEff a
  MPlus :: NonDetEff Bool

我们可以定义

type NonDetComp = Freer NonDetEff

当 Roll应用于 MPlus , a与 Bool 统一第二个参数的类型是 Bool -> NonDetEff b这基本上是一个元组:

tuplify :: (Bool -> a) -> (a, a)
tuplify f = (f True, f False)

untuplify :: (a, a) -> (Bool -> a)
untuplify (x, y) True  = x
untuplify (x, y) False = y

举个例子:

ex :: NonDetComp Int
ex = Roll MPlus $ Pure . untuplify (1, 2)

所以我们可以定义一个 MonadPlus非确定性计算的实例

instance MonadPlus NonDetComp where
    mzero       = Roll MZero Pure
    a `mplus` b = Roll MPlus $ untuplify (a, b)

并运行它们

run :: NonDetComp a -> [a]
run (Pure x)       = [x]
run (Roll MZero f) = []
run (Roll MPlus f) = let (a, b) = tuplify f in run a ++ run b