什么是欣德利-米尔纳？

Posted 2023-02-16

【中文标题】什么是欣德利-米尔纳？

【英文标题】：What is Hindley-Milner?

【发布时间】：2010-09-28 19:08:19

【问题描述】：

我遇到过这个词Hindley-Milner，我不确定是否理解它的意思。

我已阅读以下帖子：

史蒂夫·耶格-Dynamic Languages Strike Back 史蒂夫·耶格-The Pinocchio Problem 丹尼尔·斯皮瓦克 - What is Hindley-Milner? (and why is it cool?)

但是在 wikipedia 中没有一个条目通常会为我提供简明的解释。^{注意 - 有now been added}

这是什么？ 什么语言和工具实现或使用它？ 请您提供一个简洁的答案吗？

【参考方案1】：

您可以使用 Google Scholar 或 CiteSeer 或您当地的大学图书馆找到原始论文。第一个太老了，你可能得找杂志的装订本，我在网上找不到。我为另一个找到的链接已损坏，但可能还有其他链接。你肯定能找到引用这些的论文。

Hindley, Roger J, 组合逻辑中对象的主要类型方案, 美国数学学会汇刊，1969 年。

Milner, Robin，类型多态性理论，计算机与系统科学杂志，1978 年。

【讨论】：

后者可以在这里找到：citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.5276

前者：ams.org/journals/tran/1969-146-00/S0002-9947-1969-0253905-6/…

【参考方案2】：

Hindley-Milner 是一个类型系统，由 Roger Hindley（研究逻辑）和后来的 Robin Milner（研究编程语言）独立发现。 Hindley-Milner 的优点是

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

有时一个函数或值可以有一种以上的类型，例如length函数的例子：它可以是“整数到整数的列表”、“字符串到整数的列表”、 “整数对列表”，等等。在这种情况下，Hindley-Milner 系统的一个重要优势是每个类型良好的术语都有一个独特的“最佳”类型，称为主体类型。 list-length 函数的主要类型是“对于任何a，从a 列表到整数的函数”。这里a 是所谓的“类型参数”，它在 lambda 演算中是显式的，但在大多数编程语言中是隐式的。类型参数的使用解释了为什么 Hindley-Milner 是一个实现参数多态性的系统。 （如果您在 ML 中编写长度函数的定义，您可以看到类型参数：

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

如果项具有 Hindley-Milner 类型，则可以推断出主要类型，而无需程序员进行任何类型声明或其他注释。 （这是喜忧参半，因为任何人都可以证明曾经处理过大量没有注释的机器学习代码。）

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

ML 系列（Standard ML 和 Objective Caml） Haskell Clean

所有这些语言都扩展了 Hindley-Milner； Haskell、Clean 和 Objective Caml 以雄心勃勃和不同寻常的方式做到了这一点。 （处理可变变量需要扩展，因为基本的 Hindley-Milner 可以被颠覆，例如，使用包含未指定类型值列表的可变单元格。此类问题由名为 value restriction 的扩展处理。）

许多其他基于类型函数式语言的次要语言和工具使用 Hindley-Milner。

Hindley-Milner 是System F 的限制，它允许更多类型但需要程序员注释。

【讨论】：

@NormanRamsey 我知道这已经很老套了，但感谢您清理了让我无休止的烦恼：每次我提到 Hindley-milner 类型系统时，都会有人在谈论类型推断时说我已经开始质疑 HM 是一个类型系统还是仅仅是推理算法......谢谢你是为了我猜***误导人们关于这一点，以至于他们甚至让我感到困惑......

为什么它是 parametrically 多态的，而不是简单的多态？您给出的 Any 示例，我将其视为多态性的示例 - 可以使用子类型而不是定义中指定的超类型，而不是参数多态性 ala C++，其中实际类型由程序员指定以创建新功能。

@jcora：晚了几年，但为了未来读者的利益：由于parametricity 的属性，它被称为 parametric 多态性，这意味着对于您的任何类型插入，像length :: forall a. [a] -> Int 这样的函数的所有实例必须表现相同，而不管a——它是不透明的；你对此一无所知。除非您添加额外的类型约束（Haskell 类型类），否则没有 instanceof（Java 泛型）或“鸭子类型”（C++ 模板）。通过参数化，您可以获得一些关于函数能做什么/不能做什么的很好的证明。

“任何人都可以证明谁曾经处理过大量没有注释的机器学习代码。”。哦，是的。

【参考方案3】：

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

Hindley-Milner type inference over (Lisp-ish) S-expressions, in under 650 lines of C#

请注意，该实现仅在 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's javascript implementation，这也有助于入门（对我有用）。

'HTH,