我最近一直在学习 λ 演算。我理解无类型和有类型 λ 演算之间的区别。但是，我不太清楚 之间的区别。 Hindley-Milner 型系统 和 类型化 λ 演算 .是关于parametric polymorphism或者还有其他区别吗？
谁能清楚地指出两者之间的差异(和相似之处)？
最佳答案
我看之间关系的方式类型化 λ 演算 和 Hindley-Milner 型系统 是类型化 λ 演算 是 λ-演算添加类型。你可以做类型化 λ 演算 不需要 Hindley-Milner 型系统 ，例如所有类型都被声明，它们不被推断。
现在如果你要写一个 strongly statically typed基于的编程语言类型化 λ 演算 并想省略 type annotations允许类型为 inferred然后 type inference被使用，并且很可能你会使用 Hindley-Milner 型系统 或者它的一个变种。
另一种思考方式是在创建基于 的编程语言时类型化 λ 演算 是编译器会有 phases ，其中之一将使用 Hindley-Milner 型系统 .阶段的顺序是:
另一种思考方式是 type system有一套type rules还有那个 Hindley-Milner type system是具有特定类型规则集的特定类型系统。 Hindley-Milner type system的主要好处之一是推断类型的时间效率高，并且还有许多类型规则sought在 functional programming ，例如Let-polymorphism和 parametric polymorphism .在现实世界中，如果您正在创建一种编程语言并希望推断类型，那么您希望在合理的时间内完成，例如秒。自 inferencing可能导致 combinatorial explosion经常寻求一套有效的规则，这就是为什么 Hindley-Milner type system 的主要原因之一。被如此频繁地使用或引用。
适用于基于 的现实世界编程语言类型化 λ 演算 见 System F .
关于functional-programming - 简单类型的 lambda 演算与 Hindley-Milner 类型系统，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/52595339/