我遇到了这个术语 Hindley-Milner，不确定是否理解它的含义。
我已经阅读了以下帖子：
但是维基百科中没有单独的词条解释这个术语，而通常维基百科可以提供简明扼要的解释。
注意 - 现在已经添加了一个页面
它是什么？
哪些语言和工具实现或使用它？
请给出简洁的答案。
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.
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
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.)
您可以使用Google Scholar或CiteSeer找到原始论文--或者使用本地大学图书馆。第一篇论文太旧了，你可能需要找到期刊的装订本，我没有在网上找到它。我找到的另一篇文章的链接已经失效了，但可能还有其他的链接。您肯定能够找到引用这些论文的文章。
Hindley, Roger J，《组合逻辑中对象的主类型方案》，美国数学会交易，1969年。
Milner, Robin，《类型多态性理论》，计算机和系统科学杂志，1978年。
C#中的简单Hindley-Milner类型推断实现：
在不到650行的C#代码中对(Lisp风格的)S表达式进行Hindley-Milner类型推断
请注意，该实现仅涉及270行左右的C#代码（包括算法W以及支持它的少量数据结构）。
使用摘录：
// ...
var syntax =
new SExpressionSyntax().
Include
(
// Not-quite-Lisp-indeed; just tolen from our host, C#, as-is
SExpressionSyntax.Token("\\/\\/.*", SExpressionSyntax.Commenting),
SExpressionSyntax.Token("false", (token, match) => false),
SExpressionSyntax.Token("true", (token, match) => true),
SExpressionSyntax.Token("null", (token, match) => null),
// Integers (unsigned)
SExpressionSyntax.Token("[0-9]+", (token, match) => int.Parse(match)),
// String literals
SExpressionSyntax.Token("\\\"(\\\\\\n|\\\\t|\\\\n|\\\\r|\\\\\\\"|[^\\\"])*\\\"", (token, match) => match.Substring(1, match.Length - 2)),
// For identifiers...
SExpressionSyntax.Token("[\\$_A-Za-z][\\$_0-9A-Za-z\\-]*", SExpressionSyntax.NewSymbol),
// ... and such
SExpressionSyntax.Token("[\\!\\&\\|\\<\\=\\>\\+\\-\\*\\/\\%\\:]+", SExpressionSyntax.NewSymbol)
);
var system = TypeSystem.Default;
var env = new Dictionary<string, IType>();
// Classic
var @bool = system.NewType(typeof(bool).Name);
var @int = system.NewType(typeof(int).Name);
var @string = system.NewType(typeof(string).Name);
// Generic list of some `item' type : List<item>
var ItemType = system.NewGeneric();
var ListType = system.NewType("List", new[] { ItemType });
// Populate the top level typing environment (aka, the language's "builtins")
env[@bool.Id] = @bool;
env[@int.Id] = @int;
env[@string.Id] = @string;
env[ListType.Id] = env["nil"] = ListType;
//...
Action<object> analyze =
(ast) =>
{
var nodes = (Node[])visitSExpr(ast);
foreach (var node in nodes)
{
try
{
Console.WriteLine();
Console.WriteLine("{0} : {1}", node.Id, system.Infer(env, node));
}
catch (Exception ex)
{
Console.WriteLine(ex.Message);
}
}
Console.WriteLine();
Console.WriteLine("... Done.");
};
// Parse some S-expr (in string representation)
var source =
syntax.
Parse
(@"
(
let
(
// Type inference ""playground""
// Classic..
( id ( ( x ) => x ) ) // identity
( o ( ( f g ) => ( ( x ) => ( f ( g x ) ) ) ) ) // composition
( factorial ( ( n ) => ( if ( > n 0 ) ( * n ( factorial ( - n 1 ) ) ) 1 ) ) )
// More interesting..
( fmap (
( f l ) =>
( if ( empty l )
( : ( f ( head l ) ) ( fmap f ( tail l ) ) )
nil
)
) )
// your own...
)
( )
)
");
// Visit the parsed S-expr, turn it into a more friendly AST for H-M
// (see Node, et al, above) and infer some types from the latter
analyze(source);
// ...
...这将产生：
id : Function<`u, `u>
o : Function<Function<`z, `aa>, Function<`y, `z>, Function<`y, `aa>>
factorial : Function<Int32, Int32>
fmap : Function<Function<`au, `ax>, List<`au>, List<`ax>>
... Done.
length :: forall a. [a] -> Int这样的函数的所有实例都必须表现相同，而不管a是什么——它是不透明的；您对它一无所知。除非添加额外的类型约束（Haskell类型类），否则没有instanceof（Java泛型）或“鸭子类型”（C++模板）。通过参数性，您可以获得有关函数可以/不能执行的精确证明。 - Jon Purdy