Hindley-Milner 是什么？

你可以使用 Google Scholar 或 CiteSeer ——或者当地的大学图书馆——找到原始论文。第一本已经很旧了，你可能需要找到那本日记的装订本，我在网上找不到。我找到的另一个链接断了，但可能还有其他的。你肯定能找到引用这些的论文。

亨德利，罗杰 · J，组合子逻辑中对象的主类型方案, 美国数学学会汇刊，1969年。

米尔纳，罗宾，类型多态性理论，《计算机与系统科学杂志》 ，1978年。

Hindley-Milner 是由 Roger Hindley (研究逻辑)和 Robin Milner (研究编程语言)独立发现的 打字系统。Hindley-Milner 的优势是

• 它支持 多态性函数; 例如，一个函数可以提供独立于元素类型的列表长度，或者一个函数执行独立于存储在树中的键类型的二叉树查找。

• 有时候一个函数或值可以有 不止一种，就像长度函数的例子一样: 它可以是“从整数到整数的列表”，“从字符串到整数的列表”，“从对到整数的列表”，等等。在这种情况下，Hindley-Milner 系统的一个信号优势是 每个类型良好的术语都有一个独特的“最佳”类型，它被称为 主要类型主要类型。List-length 函数的主要类型是“对于任何 a，函数从 a列表到整数”。这里的 a是一个所谓的“类型参数”，它是 在 lambda 微积分中是显式的而不是 在大多数编程语言中是隐式的。类型参数的使用解释了为什么 Hindley-Milner 是一个实现 参数多态性的系统。(如果你用 ML 写一个长度函数的定义，你可以这样看到类型参数:

   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.)

Hindley-Milner is the basis for the type system of almost every statically typed functional language. Such languages in common use include

• The ML family (Standard ML and Objective Caml)
• Haskell
• Clean

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.)

Many other minor languages and tools based on typed functional languages use Hindley-Milner.

Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.

C # 中简单的 Hindley-Milner 类型推断实现:

Hindley-Milner 对(Lisp-ish) S- 表达式的类型推断，在 C # 的650行以下

注意，该实现只在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.

参见 bitbucket 上的 Brian McKenna 的 JavaScript 实现，它也有助于入门(对我有用)。

‘ HTH,