什么是欣德利米尔纳？

我遇到过这个词欣德利-米尔纳，我不确定是否理解它的意思。

我已阅读以下帖子：

• 史蒂夫·叶格 -动态语言的反击 http://steve-yegge.blogspot.com/2008/05/dynamic-languages-strike-back.html
• 史蒂夫·叶格 -匹诺曹问题 http://steve-yegge.blogspot.com/2007/01/pinocchio-problem.html
• 丹尼尔·斯皮瓦克 -什么是欣德利米尔纳？ （为什么它很酷？） https://web.archive.org/web/20181118000004/http://www.codecommit.com/blog/scala/what-is-hindley-milner-and-why-is-it-cool

But there is no single entry for this term in wikipedia where usually offers me a concise explanation.
^{Note - one has now been added http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner}

它是什么？
什么语言和工具实现或使用它？
您能给出一个简洁的答案吗？

欣德利-米尔纳是类型系统由 Roger Hindley（研究逻辑）独立发现，后来由 Robin Milner（研究编程语言）独立发现。 Hindley-Milner 的优点是

• 它支持多态性功能;例如，一个函数可以为您提供与元素类型无关的列表长度，或者一个函数可以执行与树中存储的键类型无关的二叉树查找。

• 有时一个函数或值可以有不止一种类型，如长度函数的示例：它可以是“整数列表到整数”、“字符串列表到整数”、“对列表到整数”等等。在这种情况下，Hindley-Milner 系统的一个显着优势是每个类型正确的术语都有一个独特的“最佳”类型，这被称为主要类型。列表长度函数的主要类型是“对于任何a，来自列表的函数a到整数”。这里a是所谓的“类型参数”，即lambda 演算中的显式 but 大多数编程语言中隐含的。类型参数的使用解释了为什么 Hindley-Milner 是一个实现参数多态性。 （如果你用 ML 编写长度函数的定义，你可以这样看到类型参数：

   fun 'a length []      = 0
     | 'a length (x::xs) = 1 + length xs
  

• If一个项具有 Hindley-Milner 类型，那么无需任何类型声明即可推断主体类型或程序员的其他注释。 （这是一个好坏参半的事情，因为任何人都可以证明谁曾经处理过大量没有注释的机器学习代码。）

Hindley-Milner 是几乎所有静态类型函数语言的类型系统的基础。常用的此类语言包括

• ML家族（标准机器学习 http://en.wikipedia.org/wiki/Standard_ML and 客观凸轮 http://caml.inria.fr/)
• Haskell http://www.haskell.org
• Clean http://clean.cs.ru.nl/

所有这些语言都扩展了 Hindley-Milner； Haskell、Clean 和 Objective Caml 以雄心勃勃且不寻常的方式做到了这一点。 （需要扩展来处理可变变量，因为基本的 Hindley-Milner 可以使用例如保存未指定类型的值列表的可变单元格来破坏。此类问题可以通过称为值限制 http://users.cs.fiu.edu/~smithg/cop4555/valrestr.html.)

许多其他小语言和基于类型化函数语言的工具都使用 Hindley-Milner。

Hindley-Milner 是一个限制System F http://en.wikipedia.org/wiki/System_F，它允许更多类型，但是需要程序员注释.