如何使用自由（或自由器）单子对需要单子参数的操作进行编码？

Question

大多数单子函数需要纯参数并返回一个单子值。但是有一些函数还需要单子参数，例如：

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)

他们似乎都带来了不同的问题，我无法掌握使用自由单子编码此类操作的通用方法。

• In both finally and forkIO the problem is that the monadic argument is of a different type than the result. But for free one would need them to be of the same type, as IO a gets replaced by the type variable of the encoding type, like data MyFunctor x = Finally x x x, which would only encode IO a -> IO a -> IO a.

  In From zero to cooperative threads in 33 lines of Haskell code the author uses Fork next next to fist implement

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

  and then uses it to implement

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

  where the input and output have different types. But I don't understand if this was derived using some process or just an ad-hoc idea that works for this particular purpose.

• mplus is in particular confusing: a naive encoding as

  data F b = MZero | MPlus b b
  

  distributes over >>= and a suggested better implementation is more complicated. And also a native implementation of a free MonadPlus was removed from free.

  In freer it's implemented by adding

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

  Why is MPlus NonDetEff Bool instead of NonDetEff a a? And is there a way how to make it work with Free, where we need the data type to be a functor, other than using the CoYoneda functor?

• For forkExec I have no idea how to proceed at all.

- Petr

---

您IP地址为143.198.54.68，由于运营成本限制，当前对于免费用户的使用频率限制为每个IP每72小时10次对话，如需解除限制，请点击左下角设置图标按钮（手机用户先点击左上角菜单按钮）。 - user2407038

@user2407038 我理解你的意思。但我对“机械编码整个接口，让解释器担心实现细节”的方法很感兴趣。 - Petr

Answer 1

我只回答关于Freer单子部分的问题。先回忆一下定义：

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

- effectfully