Fix 和 Mu 同构

Question

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

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

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

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

Answer 1

它们是同构的吗？

是的，它们在 Haskell 中是同构的。请参阅Ed Kmett 的递归方案包中的 Fix、Mu 和 Nu 之间的区别是什么以获取一些附加说明。

如果是，你如何证明？

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

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))。我们可以使用归纳法来证明它 must be t，至少对于有限的t（它在无限结构中变得更加微妙 - 请参阅本答案末尾的附录）。有两种可能需要考虑：

• unfix t :: f (Fix f)是空的，没有可挖掘的递归位置。在这种情况下，fmap absurd z对于 some 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 tt :: Fix fforall a. (f a -> a) -> a

我们如何在forall a. (f a -> a) -> a不依赖 的情况下定义一个函数fixToMu？无论如何，它必须涉及使用f a -> a作为参数提供的代数来获得a结果。直接路线会将其应用于某个f a值。一个主要的警告是，由于a是多态的，我们必须能够f a为 的任何选择召唤所述值a。只要f-values 恰好存在，这就是一个可行的策略。在这种情况下，我们可以这样做：

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是 a 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值可以被注入到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 tsome的形式t :: Fix f。因此，fixToMu是满射，我们有所需的同构。

附录

在评论中，就归纳论证在cata Fix t = t推导中的适用性提出了一个密切相关的问题。至少，函子定律和参数性确保fmap (cata Fix)不会产生额外的工作（例如，它不会扩大结构，或引入额外的递归位置以进行挖掘），这证明了为什么进入递归位置就是全部在推导的归纳步骤中很重要。既然如此，如果t是一个有限结构，f (Fix t)最终会达到空的基本情况，一切都清楚了。t然而，如果我们允许无穷大，我们可以fmap在fmapafter 之后无限下降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。

这种懒惰的缓刑反映了，正如在本讨论的其他地方提到的，懒惰如何破坏不动点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.