什么是欣德利-米尔纳? [英] What is Hindley-Milner?
问题描述
我遇到了这个词 Hindley-Milner，我不确定是否理解它的意思.
I encountered this term Hindley-Milner, and I'm not sure if grasp what it means.
我已阅读以下帖子:
- Steve Yegge - 动态语言反击
- Steve Yegge - 匹诺曹问题
- Daniel Spiewak - 什么是 Hindley-Milner?(为什么它很酷?)
但维基百科中没有关于这个术语的单一条目，通常为我提供简洁的解释.
注意 - 现已添加
But there is no single entry for this term in wikipedia where usually offers me a concise explanation.
Note - one has now been added
这是什么?
实现或使用它的语言和工具是什么?
你能提供一个简洁的答案吗?
What is it?
What languages and tools implement or use it?
Would you please offer a concise answer?
推荐答案
Hindley-Milner 是一个 类型系统 由 Roger Hindley(他在研究逻辑)和后来由 Robin Milner(他正在研究编程语言).Hindley-Milner 的优点是
Hindley-Milner is a type system discovered independently by Roger Hindley (who was looking at logic) and later by Robin Milner (who was looking at programming languages). The advantages of Hindley-Milner are
支持多态函数；例如，一个函数可以为您提供与元素类型无关的列表长度，或者一个函数执行与树中存储的键类型无关的二叉树查找.
It supports polymorphic functions; for example, a function that can give you the length of the list independent of the type of the elements, or a function does a binary-tree lookup independent of the type of keys stored in the tree.
有时一个函数或值可以有多个类型，如长度函数的例子:它可以是整数到整数的列表"、字符串到整数的列表"整数"、整数对列表"等.在这种情况下，Hindley-Milner 系统的一个信号优势是每个类型良好的术语都有一个独特的最佳"类型，称为主要类型.列表长度函数的主要类型是对于任何a，函数从a 的列表到整数".这里的 a 是所谓的类型参数"，它在 lambda 演算中是显式的，但在大多数编程语言中是隐式的.类型参数的使用解释了为什么 Hindley-Milner 是一个实现参数多态性的系统.(如果你在 ML 中写了长度函数的定义，你可以这样看到类型参数:
Sometimes a function or value can have more than one type, as in the example of the length function: it can be "list of integers to integer", "list of strings to integer", "list of pairs to integer", and so on. In this case, a signal advantage of the Hindley-Milner system is that each well-typed term has a unique "best" type, which is called the principal type. The principal type of the list-length function is "for any a, function from list of a to integer". Here a is a so-called "type parameter," which is explicit in lambda calculus but implicit in most programming languages. The use of type parameters explains why Hindley-Milner is a system that implements parametric polymorphism. (If you write a definition of the length function in ML, you can see the type parameter thus:
fun 'a length [] = 0
| 'a length (x::xs) = 1 + length xs
如果一个术语具有 Hindley-Milner 类型，那么可以推断主体类型而无需程序员进行任何类型声明或其他注释.(这是喜忧参半，因为任何人都可以证明谁曾经处理过大量没有注释的机器学习代码.)
If a term has a Hindley-Milner type, then the principal type can be inferred without requiring any type declarations or other annotations by the programmer. (This is a mixed blessing, as anyone can attest who has ever been handled a large chunk of ML code with no annotations.)
Hindley-Milner 是几乎所有静态类型函数式语言的类型系统的基础.此类常用语言包括
Hindley-Milner is the basis for the type system of almost every statically typed functional language. Such languages in common use include
所有这些语言都扩展了 Hindley-Milner；Haskell、Clean 和 Objective Caml 以雄心勃勃且不寻常的方式做到了这一点.(需要扩展来处理可变变量，因为基本的 Hindley-Milner 可以被颠覆，例如使用一个包含未指定类型值列表的可变单元格.此类问题由名为 值限制.)
All these languages have extended Hindley-Milner; Haskell, Clean, and Objective Caml do so in ambitious and unusual ways. (Extensions are required to deal with mutable variables, since basic Hindley-Milner can be subverted using, for example, a mutable cell holding a list of values of unspecified type. Such problems are dealt with by an extension called the value restriction.)
许多其他基于类型化函数式语言的次要语言和工具使用 Hindley-Milner.
Many other minor languages and tools based on typed functional languages use Hindley-Milner.
Hindley-Milner 是对 System F 的限制，它允许更多类型但需要程序员的注释.
Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.
这篇关于什么是欣德利-米尔纳?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
