可以为"免费"实现MonadFix吗？

Question

http://hackage.haskell.org/package/free在Control.Monad.Free.Free允许一个获得获得了"自由单子"对于任何给定Functor.但是,它没有MonadFix实例.这是因为这样的实例无法写入,还是只是被遗漏了？

如果不能写这样的实例,为什么不呢？

Answer 1

考虑以下内容的描述mfix:

monadic计算的固定点.仅mfix f执行f一次动作,最终输出作为输入反馈.

在上下文中Free,"执行"一词意味着创建层的"执行" Functor.因此,"仅一次"意味着在评估结果中mfix f,Pure构造函数中保存的值必须完全确定创建了多少层仿函数.

现在,假设我们有一个特定的函数once,我们知道它将始终只创建一个Free构造函数,但是Pure需要很多构造函数来保存叶值.那么,"一次"的输出将只是Free f a与某种类型的值同构的类型的值f a.有了这些知识,我们就可以安全地Free输出once,获得类型的值f a.

现在,请注意,因为mfix需要"仅执行一次操作",所以mfix once对于一致的实例,should 的结果不包含比once在单个应用程序中创建的更多的monadic结构.因此,我们可以推断出从中获得的值mfix once也必须与类型的值同构f a.

给定a -> f a一些类型的函数Functor f,我们可以用一个单独包装结果Free并获得a -> Free f a满足上述描述的类型函数once,并且我们已经确定我们可以解包结果mfix once以获得类型f a返回的值.

因此,符合条件的实例(Functor f) => MonadFix (Free f)意味着能够通过上述包装和展开来编写ffix :: (Functor f) => (a -> f a) -> f a适用于所有实例的函数Functor.

这显然不能证明你不能写这样的实例......但如果可能的话,那MonadFix将是完全多余的,因为你可以ffix直接写出来.(我想重新实现它就像mfix一个Monad约束,使用liftM.呃.)

Answer 2

好吧,受到MonadFix实例的启发Maybe,我尝试了这个(使用以下定义Free):

data Free f a
    = Pure a
    | Impure (f (Free f a))

instance (Functor f) => Monad (Free f) where
    return = Pure
    Pure x >>= f = f x
    Impure x >>= f = Impure (fmap (>>= f) x)

instance (Functor f) => MonadFix (Free f) where
    mfix f = let Pure x = f x in Pure x

法律是:

• 纯度: mfix (return . h) = return (fix h)
• 左萎缩: mfix (\x -> a >>= \y -> f x y) = a >>= \y -> mfix (\x -> f x y)
• 滑动:mfix (liftM h . f) = liftM h (mfix (f . h)),严格h
• 嵌套: mfix (\x -> mfix (f x)) = mfix (\x -> f x x)

纯度很容易证明 - 但我在试图证明左萎缩时遇到了一个问题:

mfix (\x -> a >>= \y -> f x y)
= let Pure x = (\x -> a >>= \y -> f x y) x in Pure x
= let Pure x = a >>= \y -> f x y in Pure x
-- case a = Pure z
  = let Pure x = Pure z >>= \y -> f x y in Pure x
  = let Pure x = f x z in Pure x
  = let Pure x = (\x -> f x z) x in Pure x
  = mfix (\x -> f x z)
  = Pure z >>= \y -> mfix (\x -> f x y)
-- case a = Impure t
  = let Pure x = Impure t >>= \y -> f x y in Pure x
  = let Pure x = Impure (fmap (>>= \y -> f x y) t) in Pure x
  = Pure _|_

但

  Impure t >>= \y -> mfix (\x -> f x y)
  = Impure (fmap (>>= \y -> mfix (\x -> f x y)) t)
  /= Pure _|_

所以,至少,如果Pure和Impure构造函数是可区分的,那么我的实现mfix不符合法律.我想不出任何其他实现,但这并不意味着它不存在.对不起,我无法进一步阐明.