Hindley-Milner 是一种类型系统，它是许多著名的函数式编程语言类型系统的基础。Damas-Milner 是一种在 Hindley-Milner 类型系统中推断（推断？）类型的算法。
维基百科给出了算法的描述，据我所知，它相当于一个词：“统一”。这就是它的全部吗？如果是这样，那意味着有趣的部分是类型系统本身，而不是类型推断系统。
如果 Damas-Milner 不仅仅是统一，我想要一个 Damas-Milner 的描述，其中包括一个简单的示例，理想情况下，还有一些代码。
此外，这种算法通常被称为进行类型推断。它真的是一个推理系统吗？我以为这只是推断类型。
相关问题：
Damas Milner 只是对统一的结构化使用。
当它递归到一个 lambda 表达式时，它构成了一个新的变量名。当您在子术语中发现该变量以需要给定类型的方式使用时，它记录了该变量和该类型的统一。如果它试图统一两种没有意义的类型，比如说单个变量既是 Int 又是来自 a -> b 的函数，那么它会因为你做了坏事而对你大喊大叫。
此外，这种算法通常被称为进行类型推断。它真的是一个推理系统吗？我以为这只是推断类型。
推断类型是类型推断。检查类型注释对给定术语是否有效是类型检查。它们是不同的问题。
如果是这样，那意味着有趣的部分是类型系统本身，而不是类型推断系统。
通常说 Hindley-Milner 风格的类型系统在风口浪尖上是平衡的。如果您添加更多功能，则无法推断类型。因此，您可以在 Hindley-Milner 样式类型系统之上进行分层而不破坏其推理属性的类型系统扩展确实是现代函数式语言的有趣部分。在某些情况下，我们将类型推断和类型检查混合在一起，例如在 Haskell 中，许多现代扩展无法推断，但可以进行检查，因此它们需要类型注释来实现高级功能，例如多态递归。
维基百科给出了算法的描述，据我所知，它相当于一个词：“统一”。这就是它的全部吗？如果是这样，那意味着有趣的部分是类型系统本身，而不是类型推断系统。
IIRC，Damas-Milner 类型推断算法 W 的有趣部分在于它推断出可能的最一般类型。