如何编码采用免费(或更自由)monad的monadic参数的动作？

Question

大多数monadic函数采用纯参数并返回monadic值.但也有一些需要monadic论证,例如:

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编码此类操作的通用方法.

• 在两者中finally,forkIO问题是monadic参数的类型与结果不同.但是对于free,需要它们具有相同的类型,因为它IO a被替换为编码类型的类型变量,例如data MyFunctor x = Finally x x x,它只能编码IO a -> IO a -> IO a.

  在从零到协作线程的33行Haskell代码中,作者用来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
  

  分发>>=并建议更好的实现更复杂.并且还提供一个免费的本地实现MonadPlus 从去除自由.

  在自由它的加入实现

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

  为什么MPlus NonDetEff Bool而不是NonDetEff a a？有没有一种方法可以使它工作Free,我们需要数据类型作为仿函数,而不是使用CoYoneda仿函数？

• 因为forkExec我根本不知道如何进行.

Answer 1

我只会回答Freermonad 部分。回想一下定义：

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 bwhich 基本上是一个元组：

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