单子不动点非直接极限的直觉阐释及剩余元素的数学依据

我们先从你给出的两个例子入手，拆解背后的核心差异：

例子1：Maybe单子的不动点Foo #

data Foo = Halt | Iter Foo

这是Maybe单子的不动点。我们来看对应的序列：

• Void：空类型，没有元素
• Maybe Void：仅包含Nothing（对应Halt）
• Maybe (Maybe Void)：包含Nothing、Just Nothing（对应Halt、Iter Halt）
• 以此类推，每一步都是在前一步的基础上添加一层Just（对应Iter）

这个序列的直接极限，本质是所有有限长度的迭代终止序列——也就是Halt、Iter Halt、Iter (Iter Halt)……这些都能通过有限次应用构造器得到。但Foo里还存在fix Iter，也就是无限嵌套的Iter (Iter (Iter ...))，这个元素不在直接极限里，因为它无法通过有限步构造出来。

例子2：Complex单子的不动点Bar #

data Bar = Bar Bar Bar

这是Complex单子（将类型映射为自身三次乘积的单子）的不动点。对应的序列：

• Void：空类型
• Complex Void：空类型的三次乘积还是空
• Complex (Complex Void)：依然是空类型
• 整个序列的直接极限自然是Void

但Bar里存在fix (join Bar)——也就是无限递归的Bar (Bar (...)) (Bar (...)) (Bar (...))。这个元素能存在，是因为它满足递归方程x = Bar x x x，而直接极限里没有它，因为有限步构造永远无法从空类型生成任何元素。

核心数学依据：初始代数 vs 最终余代数 #

这里的关键是两种不同的“不动点”定义，对应范畴论里的两个核心概念：

• 初始代数：对应序列的直接极限，只包含有限生成的元素——也就是可以通过有限次应用构造器得到的元素。它是“最小”的不动点，仅覆盖满足构造规则的有限元素。
• 最终余代数：包含所有有限和无限递归的元素，也就是我们在编程语言里实际使用的递归数据类型。它是“最大”的不动点，允许满足递归方程的无限元素存在。

在集合范畴中，直接极限只能得到初始代数；而我们写递归数据类型时，实际上是在支持无限递归的范畴（比如完全偏序CPO范畴，或者集合范畴的余完备扩张）中取最终余代数。这些范畴允许我们将无限链的“极限”作为合法元素，比如fix Iter就是无限链Halt ≤ Iter Halt ≤ Iter (Iter Halt) ≤ ...的最小上界，而Bar的唯一元素就是满足x = Bar x x x的无限递归解。

简单来说：直接极限管的是“有限构造出来的东西”，而递归数据类型的不动点还包含“无限递归的东西”——这就是两者的本质区别。

内容的提问来源于stack exchange，提问作者Dannyu NDos