21

http://hackage.haskell.org/package/free inControl.Monad.Free.Free允许访问任何给定的“免费单子” Functor。但是,它没有MonadFix实例。这是因为这样的实例无法编写,还是只是被遗漏了?

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

4

3 回答 3

14

考虑对做什么的描述mfix

一元计算的不动点。mfix f只执行f一次动作,最终的输出作为输入反馈。

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

现在,假设我们有一个特定的函数once,我们知道它总是只会创建一个Free构造函数,但是需要许多Pure构造函数来保存叶值。那么,'once' 的输出将只是与 typeFree f a的某个值同构的 type 值f a。有了这些知识,我们就可以安全地取消Free输出once,得到一个类型的值f a

现在,请注意,因为mfix需要“只执行一次操作”,所以对于符合要求的实例,除了在单个应用程序中创建之外,mfix once应该不包含额外的一元结构。once因此,我们可以推断,从中获得的值mfix once也必须与 type 的值同构f a

给定任何类型a -> f a为 some的函数Functor f,我们可以用 single 包装结果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直接轻松地编写。(而且我想mfixMonad约束重新实现它,使用liftM. 呃。)

于 2013-02-01T05:09:38.583 回答
5

好吧,受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 _|_

所以,至少,如果PureImpure构造函数是可区分的,那么我的实现mfix不满足法律。我想不出任何其他的实现,但这并不意味着它不存在。抱歉,我无法进一步阐明。

于 2013-02-01T03:50:02.433 回答
3

不,不能笼统地写出来,因为不是每个 Monad 都是 MonadFix 的实例。每个 Monad 都可以使用下面的 FreeMonad 来实现。如果您可以免费实现 MonadFix,那么您将能够从任何 Monad 派生 MonadFix,这是不可能的。但当然,您可以为 MonadFix 类定义一个 FreeFix。

我认为它可能看起来像这样,但这只是第三次猜测(尚未测试):

data FreeFix m a = FreeFix { runFreeFix :: (forall r. (r -> m r) -> m r) -> m a }

instance (Monad m) => Monad (FreeFix m) where
    return a = FreeFix $ \_-> do
        return a
    f >>= g = FreeFix $ \mfx -> do
        x <- runFreeFix f mfx
        runFreeFix (g x) mfx

instance (Monad m) => MonadFix (FreeFix m) where
    mfix f = FreeFix $ \mfx -> do
        mfx (\r->runFreeFix (f r) mfx)

这个想法是 m 是一个缺少 mfix 实现的 Monad;所以当 FreeFix 会被缩减时,mfix 需要是一个参数。

于 2013-02-07T11:29:30.383 回答