它们是同构的吗？
是的，它们在 Haskell 中是同构的。有关其他说明，请参阅What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package。
如果是，你如何证明？
让我们从定义执行转换的函数开始：
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) 是空的，没有可挖掘的递归位置。在这种情况下，对于某些z :: f Void，它必须等于fmap absurd z，因此：
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 函数进行编目，并查看它们是否都可以用这种形式表示。
我们如何在不依赖fixToMu 的情况下定义forall a. (f a -> a) -> a 函数？无论如何，它必须涉及使用作为参数提供的f a -> a 代数来获得a 结果。直接路线会将其应用于某些 f a 值。一个主要的警告是，由于a 是多态的，我们必须能够为a 的任何选择变出f 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 是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)
考虑到我们也可以从f (Moo f) 值中生成forall a. (f a -> a) -> a，因此将它们添加为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)
请注意，通过这样做，我们偷偷地从在一个f 层下应用alg 转移到在任意数量的f 层下递归应用alg。
接下来，我们可以注意到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
fromMoo 中的Empty 情况如何？这两种情况的唯一区别是，在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 是满射的，并且我们有所需的同构。
附录
在 cmets 中，就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 的影响。
这种惰性缓和反映了，正如本讨论中其他地方所提到的，惰性如何破坏固定点 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.