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

Question

我最近一直在学习 λ 微积分。我了解无类型和有类型 λ 演算之间的区别。但是，我不太清楚 Hindley-Milner 类型系统 和 类型化 λ-演算 之间的区别。是关于parametric polymorphism 还是有其他区别？

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

Answer 1

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

Answer 2

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

现在，如果您要编写基于 类型化 λ-演算 的 strongly statically typed 编程语言，并希望省略 type annotations 允许类型为 inferred，则使用 type inference 并您很可能会使用 Hindley-Milner 类型系统或其变体。

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

1. 语法检查 - Lexer
2. 语义检查 - Parser
3. Type inference - Hindley-Milner type system
4. Type checking
5. ...

另一种思考方式是type system 具有一组type rules，而Hindley-Milner type system 是具有一组特定类型规则的特定类型系统。 Hindley-Milner type system 的主要优点之一是推断类型的时间效率很高，并且在 functional programming 中也有许多类型规则 sought，例如Let-polymorphism 和 parametric polymorphism。在现实世界中，如果您正在创建一种编程语言并希望推断类型，那么您希望在合理的时间内完成，例如秒。由于inferencing 可以导致combinatorial explosion，因此通常需要一组有效的规则，这也是Hindley-Milner type system 经常被使用或引用的主要原因之一。

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