惰性与严格语言中递归数据类型定义的差异及理论疑问

ML严格语言中的等价类型与无限列表 #

ML中等价的列表类型定义通常写成：

datatype 'a L = Empty | Cons of 'a * 'a L

从类型的语法定义来看，它并没有禁止无限列表的写法，但在严格求值的语义下，你无法构造出实际可使用的无限列表。因为严格求值要求构造器的所有参数必须完全求值完成才能生成构造器实例：如果你尝试写一个递归的无限列表（比如let rec inf = Cons(1, inf)），ML会立即尝试展开inf的定义，进入无限递归求值，最终导致栈溢出或程序挂起，永远无法得到一个合法的、可操作的值。

无法构造无限列表是否是缺陷？ #

这绝对不是缺陷，而是严格求值模型的设计选择。严格求值的核心优势是求值顺序完全可预测、内存和性能行为容易把控，非常适合系统级编程、性能敏感的场景；而惰性求值（如Haskell）允许无限结构，是为了更优雅地处理流、无限序列这类抽象，但代价是求值顺序不可控，可能带来意外的性能开销或内存泄漏。两者是不同设计目标下的合理取舍，不存在谁优谁劣，更谈不上缺陷。

ML如何排除无限列表？ #

ML并没有通过类型系统直接排除无限列表，而是通过求值语义限制了该类型的可达值集合。ML中'a L类型的合法值只能是有限递归结构：所有递归引用最终必须终止于Empty，因为严格求值要求每个构造器的参数都必须完全计算完毕，无限递归的构造永远无法生成一个完整的、可被程序正常使用的值，因此这类无限结构在ML中属于不可达的“幽灵”值，不会出现在实际可构造的类型成员中。

理论视角：类型取值集合与不动点 #

从域理论的角度，递归代数类型的取值集合确实对应某个类型构造函数的不动点，但严格语言和惰性语言对应的不动点类型不同：

• 对于ML这类严格语言，'a L类型的取值集合是类型构造函数F(X) = 1 + 'a * X的最小不动点（lfp）。最小不动点是所有前缀不动点的交集，仅包含有限的列表结构——因为它要求递归必须终止，对应有限的展开次数。
• 对于Haskell这类惰性语言，对应的是该构造函数的最大不动点（gfp）。最大不动点是所有后缀不动点的并集，既包含有限列表，也允许无限递归的列表结构存在。

类比阶乘这类递归函数：阶乘的递归定义对应的是其生成函数的最小不动点（仅包含有限输入下的合法值），和ML中列表类型的最小不动点逻辑一致。

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