以 CS101 学生可以理解的方式描述 Damas-Milner 类型推理
Hindley-Milner 是一个类型系统，它是许多众所周知的函数式编程语言的类型系统的基础。 Damas-Milner 是一种在 Hindley-Milner 类型系统中推断（推导？）类型的算法。
维基百科给出了该算法的描述，据我所知可以说，就一个字：“统一”。 这就是全部内容了吗？ 如果是这样，那就意味着有趣的部分是类型系统本身而不是类型推断系统。
如果 Damas-Milner 不仅仅是统一，我想要一个对 Damas-Milner 的描述，其中包括一个简单的示例，最好还包括一些代码。
此外，该算法通常被认为可以进行类型推断。 它真的是一个推理系统吗？ 我以为这只是推导类型。
相关问题：
Hindley-Milner is a type system that is the basis of the type systems of many well known functional programming languages. Damas-Milner is an algorithm that infers (deduces?) types in a Hindley-Milner type system.
Wikipedia gives a description of the algorithm which, as far as I can tell, amounts to a single word: "unification." Is that all there is to it? If so, that means that the interesting part is the type system itself not the type inference system.
If Damas-Milner is more than unification, I would like a description of Damas-Milner that includes a simple example and, ideally, some code.
Also, this algorithm is often said to do type inference. Is it really an inference system? I thought it was only deducing the types.
Related questions:
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
IIRC，Damas-Milner 类型推断算法 W 的有趣部分是它推断出最常见的可能类型。
IIRC, the interesting part of the Damas-Milner type inference Algorithm W is that it infers the most general types possible.
达马斯·米尔纳只是统一的结构化运用。
当它递归到 lambda 表达式时，它会构成一个新的变量名称。 当您在子术语中发现以需要给定类型的方式使用该变量时，它会记录该变量和该类型的统一。 如果它试图统一两种没有意义的类型，比如说单个变量既是 Int 又是来自 -> 的函数。 b、然后它会因为你做了坏事而对你大喊大叫。
推导类型就是类型推断。 检查类型注释对于给定术语是否有效就是类型检查。 它们是不同的问题。
人们普遍认为 Hindley-Milner 风格的字体系统在尖点上保持平衡。 如果添加更多功能，就无法推断类型。 因此，您可以在 Hindley-Milner 风格的类型系统之上进行类型系统扩展，而不破坏其推理属性，这确实是现代函数式语言的有趣部分。 在某些情况下，我们混合类型推断和类型检查，例如在 Haskell 中，许多现代扩展无法推断，但可以检查，因此它们需要类型注释来实现高级功能，例如多态递归。
Damas Milner is just a structured use of unification.
When it recurses into a lambda expression it makes up a new variable name. When you, in a sub-term, find that variable used in a way that would require a given type, it records the unification of that variable and that type. If it ever tries to unify two types that don't make sense, like saying that an individual variable is both an Int and a function from a -> b, then it yells at you for doing something bad.
Deducing the types is type inference. Checking to see that type annotations are valid for a given term is type checking. They are different problems.
It is commonly said that Hindley-Milner style type systems are balanced on a cusp. If you add much more functionality it becomes impossible to infer the types. So type system extensions that you can layer on top of a Hindley-Milner style type system without destroying its inference properties are really the interesting parts of modern functional languages. In some cases, we mix type inference and type checking, for instance in Haskell a lot of modern extensions can't be inferred, but can be checked, so they require type annotations for advanced features, like polymorphic recursion.