haskell - Fix 和 Mu 同构

Question

在 recursion-schemes 包定义了以下类型:

newtype Fix f = Fix (f (Fix f))

newtype Mu f = Mu (forall a. (f a -> a) -> a)

它们是同构的吗？如果是，你如何证明？

Answer 1

Are they isomorphic?

是的，它们在 Haskell 中是同构的。见 What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package一些补充说明。

If so, how do you prove it?

让我们从定义执行转换的函数开始:

muToFix :: Mu f -> Fix f
muToFix (Mu s) = s Fix

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)

为了证明这些函数见证了同构，我们必须证明:

muToFix . fixToMu = id
fixToMu . muToFix = id

来自 Fix然后回来

同构的一个方向比另一个更直接:

muToFix (fixToMu t) = t
muToFix (fixToMu t)  -- LHS
muToFix (Mu (\f -> cata f t))
(\f -> cata f t) Fix
cata Fix t  -- See below.
t  -- LHS = RHS

上面的最后一段， cata Fix t = t ，可以通过 cata的定义来验证:

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

cata Fix t ，那么，是 Fix (fmap (cata Fix) (unfix t)) .我们可以用归纳法证明它一定是 t ，至少对于有限 t (无限结构会变得更加微妙 - 请参阅本答案末尾的附录)。有两种可能需要考虑:

unfix t :: f (Fix f)是空的，没有可挖掘的递归位置。在这种情况下，它必须等于 fmap absurd z一些 z :: f Void ， 因此:

cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (fmap (cata Fix) (fmap absurd z))
Fix (fmap (cata Fix . absurd) z)
-- fmap doesn't do anything on an empty structure.
Fix (fmap absurd z)
Fix (unfix t)
t

unfix t不是空的。那样的话，我们至少知道fmap (cata Fix)除了申请之外什么也做不了cata Fix在递归位置上。这里的归纳假设是，这样做将使这些位置保持不变。然后我们有:

cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (unfix t)  -- Induction hypothesis.
t

(最终， cata Fix = id 是 Fix :: f (Fix f) -> Fix x 是初始 F 代数的推论。直接诉诸这个事实
在这个证明的上下文中，可能是太多的捷径。)

来自 Mu然后回来

给定 muToFix . fixToMu = id ，证明 fixToMu . muToFix = id足以证明:

那个muToFix是单射的，或

那个fixToMu是满射的。

让我们采用第二个选项，并查看相关定义:

newtype Mu f = Mu (forall a. (f a -> a) -> a)

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)

fixToMu那么，作为满射，意味着，给定任何特定的 Functor f , 类型 forall a. (f a -> a) -> a 的所有函数可以定义为 \alg -> cata alg t ，对于某些特定的 t :: Fix f .然后，任务变成对 forall a. (f a -> a) -> a 进行编目。函数，看看是否所有的函数都可以用那种形式表达。

我们如何定义 forall a. (f a -> a) -> a功能不依赖 fixToMu ?无论如何，它必须涉及使用 f a -> a代数作为参数提供以获得 a结果。直接的途径是将它应用到一些 f a值(value)。一个主要的警告是，因为 a是多态的，我们必须能够变出说 f a任何选择的值(value) a .只要 f，这是一个可行的策略- 值恰好存在。在这种情况下，我们可以这样做:

fromEmpty :: Functor f => f Void -> forall a. (f a -> a) -> a
fromEmpty z = \alg -> alg (fmap absurd z)

为了使符号更清晰，让我们为可以用来定义 forall a. (f a -> a) -> a 的事物定义一个类型。职能:

data Moo f = Empty (f Void)

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Empty z) = \alg -> alg (fmap absurd z)

除了直接路线，还有另一种可能性。鉴于 f是 Functor ，如果我们有一个 f (Moo f)我们可以两次应用代数，第一次应用在外 f 下层，通过 fmap和 fromMoo :

fromLayered :: Functor f => f (Moo f) -> forall a. (f a -> a) -> a
fromLayered u = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

考虑到我们也可以制作 forall a. (f a -> a) -> a出 f (Moo f)值，将它们添加为 Moo 的情况是有意义的。 :

data Moo f = Empty (f Void) | Layered (f (Moo f))

因此， fromLayered可以合并到 fromMoo :

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo = \case
    Empty z -> \alg -> alg (fmap absurd z)
    Layered u -> \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

请注意，通过这样做，我们偷偷地从应用 alg 转移了。下一个 f递归应用层 alg下任意数量 f层。

接下来，我们可以注意到 f Void值可以注入(inject) Layered构造函数:

emptyLayered :: Functor f => f Void -> Moo f
emptyLayered z = Layered (fmap absurd z)

这意味着我们实际上并不需要 Empty构造函数:

newtype Moo f = Moo (f (Moo f))

unMoo :: Moo f -> f (Moo f)
unMoo (Moo u) = u

Empty呢？案例在 fromMoo ?两种情况的唯一区别在于，在 Empty案例，我们有 absurd而不是 \moo -> fromMoo moo alg .自所有 Void -> a功能是 absurd ，我们不需要单独的 Empty如果有:

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Moo u) = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

一个可能的外观调整是翻转 fromMoo参数，因此我们不需要将参数写入 fmap作为一个 lambda:

foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg (Moo u) = alg (fmap (foldMoo alg) u)

或者，更无意义:

foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg = alg . fmap (foldMoo alg) . unMoo

在这一点上，再看一下我们的定义表明一些重命名是有序的:

newtype Fix f = Fix (f (Fix f))

unfix :: Fix f -> f (Fix f)
unfix (Fix u) = u

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

fromFix :: Functor f => Fix f -> forall a. (f a -> a) -> a
fromFix t = \alg -> cata alg t

它是:所有 forall a. (f a -> a) -> a函数的形式为 \alg -> cata alg t一些 t :: Fix f .因此， fixToMu是满射的，我们有所需的同构。

附录

在评论中，对 cata Fix t = t 中归纳论证的适用性提出了一个密切相关的问题。推导。至少，仿函数定律和参数性确保 fmap (cata Fix)不会产生额外的工作(例如，它不会扩大结构，或引入额外的递归位置来挖掘)，这证明了为什么在推导的归纳步骤中进入递归位置是最重要的。既然如此，如果 t是一个有限结构，空 f (Fix t)的基本情况最终会到达，一切都清楚了。如果我们允许 t然而，要成为无限，我们可以继续无休止地下降， fmap之后 fmap之后 fmap ，从未达到基本情况。

然而，无限结构的情况并不像最初看起来那么糟糕。惰性首先使无限结构可行，它允许我们懒惰地消耗无限结构:

GHCi> :info ListF
data ListF a b = Nil | Cons a b
    -- etc.
GHCi> ones = Fix (Cons 1 ones)
GHCi> (\(Fix (Cons a _)) -> a) (cata Fix ones)
1
GHCi> (\(Fix (Cons _ (Fix (Cons a _)))) -> a) (cata Fix ones)
1

虽然递归位置的连续性无限延伸，但我们可以在任何点停止并从周围的 ListF 中获得有用的结果。功能上下文。需要重申的是，此类上下文不受 fmap 的影响。 ，因此我们可能消耗的结构的任何有限段都不会受到 cata Fix 的影响。 .

这种懒惰的缓刑反射(reflect)了，正如在本讨论的其他地方提到的，懒惰如何破坏不动点之间的区别 Mu , Fix和 Nu .不偷懒， Fix不足以编码高效的核心递归，因此我们必须切换到 Nu ，最大不动点。这是差异的一个小示范:

GHCi> :set -XBangPatterns
GHCi> -- Like ListF, but strict in the recursive position.
GHCi> data SListF a b = SNil | SCons a !b deriving Functor
GHCi> ones = Nu (\() -> SCons 1 ()) ()
GHCi> (\(Nu c a) -> (\(SCons a _) -> a) (c a)) ones
1
GHCi> ones' = Fix (SCons 1 ones')
GHCi> (\(Fix (SCons a _)) -> a) ones'
^CInterrupted.