functional-programming - 简单类型的 lambda 演算与 Hindley-Milner 类型系统

Question

我最近一直在学习 λ-演算。我了解无类型和有类型 λ 演算之间的区别。但是，我不太清楚Hindley-Milner 类型系统和类型化 λ-calculus之间的区别。是关于参数多态性还是有其他差异？

谁能清楚地指出两者之间的差异（和相似之处）？

score 2 · Accepted Answer

我看待类型化 λ-演算和Hindley-Milner 类型系统之间关系的方式是，类型化 λ-演算是添加了类型的λ-演算。您可以在不需要Hindley-Milner 类型系统的情况下进行类型化的 λ-演算，例如，所有类型都已声明，它们不会被推断。

现在，如果您要编写基于类型化 λ 演算的强静态类型编程语言，并希望省略类型注释以允许推断类型，则使用类型推断，您很可能会使用Hindley-Milner 类型系统或它。

考虑这一点的另一种方法是，在创建基于类型化 λ-演算的编程语言时，编译器将具有阶段，其中一个将使用Hindley-Milner 类型系统。阶段的顺序是：

另一种思考方式是，类型系统具有一组类型规则，而Hindley-Milner 类型系统是具有一组特定类型规则的特定类型系统。Hindley-Milner 类型系统的主要优点之一是推断类型的时间效率很高，并且还具有函数式编程中寻求的许多类型规则，例如Let 多态性和参数多态性。在现实世界中，如果您正在创建一种编程语言并希望推断类型，那么您希望在合理的时间内完成，例如几秒钟。由于推理可以导致组合爆炸经常寻求一组有效的规则，这就是为什么经常使用或引用Hindley-Milner 类型系统的主要原因之一。

对于基于类型化 λ 演算的现实世界编程语言，请参见System F。

score 1 · Accepted Answer

区别在于 lambda 演算有许多类型系统，Hindley-Milner 就是其中之一。Hindley-Milner 是一个具有参数多态性的类型系统。这就是我们在当今编程语言中所说的泛型。

2 回答 2