Hindley-Milner是一个类型系统，它是许多众所周知的函数式编程语言类型系统的基础。 Damas-Milner是一种在Hindley-Milner类型系统中推断（推断？）类型的算法。以CS101学生可以理解的方式描述Damas-Milner类型推断
Wikipedia给出了一个算法的描述，据我所知，这个算法等于一个单词：“统一”。这就是它的全部吗？如果是这样，那意味着有趣的部分是类型系统本身而不是类型推理系统。
如果Damas-Milner不仅仅是统一，我想要Damas-Milner的描述，其中包括一个简单的例子，最好是一些代码。
此外，这种算法经常被认为是做类型推断。它真的是一个推理系统吗？我认为这只是推断类型。
相关问题：
达马斯米尔纳仅仅是一个结构化的使用统一的。
当它递归到一个lambda表达式中时，它构成一个新的变量名称。当你在一个子项中找到那个需要给定类型的变量时，它会记录该变量和该类型的统一。如果它试图统一两种无意义的类型，比如说一个单独的变量既是一个Int又是一个来自 - > b的函数，那么它就会因为做坏事而嚷嚷你。
另外，这种算法经常被认为是做类型推断。它真的是一个推理系统吗？我认为这只是推断类型。
推导类型是类型推断。检查以查看该类型注释对于给定期限是否有效是类型检查。他们是不同的问题。
如果是这样，那意味着有趣的部分是类型系统本身而不是类型推断系统。
通常说Hindley-Milner风格类型的系统在风口上是平衡的。如果添加更多功能，则无法推断这些类型。因此，输入系统扩展可以在Hindley-Milner样式类型系统的顶层进行分层，而不会破坏其推理属性，这实际上是现代函数式语言的有趣部分。在某些情况下，我们将类型推理和类型检查混合在一起，例如在Haskell中，很多现代扩展都无法推断出来，但是可以检查，所以它们需要高级特性的类型注释，比如多态递归。
维基百科给出了一个算法的描述，据我所知，这个算法等于一个单词：“统一”。这就是它的全部吗？如果是这样，那意味着有趣的部分是类型系统本身而不是类型推理系统。
IIRC，Damas-Milner类型推理算法W的有趣部分是它推断了最普通的可能类型。