¿Qué es Hindley-Milner?

Encontré este término Hindley-Milner , y no estoy seguro de comprender lo que significa.

He leído las siguientes publicaciones:

• Steve Yegge - Lenguajes dinámicos contraatacan
• Steve Yegge - El problema de Pinocho
• Daniel Spiewak - ¿Qué es Hindley-Milner? (y por qué es genial?)

Pero no hay una sola entrada para este término en wikipedia, donde generalmente me ofrece una explicación concisa.
^{Nota : ahora se ha agregado uno}

¿Qué es?
¿Qué lenguajes y herramientas lo implementan o usan?
¿Podría por favor ofrecer una respuesta concisa?

Hindley-Milner es un sistema de tipos descubierto independientemente por Roger Hindley (que estaba buscando lógica) y más tarde por Robin Milner (que estaba buscando lenguajes de programación). Las ventajas de Hindley-Milner son

• Es compatible con funciones polimórficas ; por ejemplo, una función que puede darle la longitud de la lista independientemente del tipo de elementos, o una función realiza una búsqueda de árbol binario independiente del tipo de claves almacenadas en el árbol.

• A veces, una función o valor puede tener más de un tipo , como en el ejemplo de la función de longitud: puede ser "lista de enteros a entero", "lista de cadenas a entero", "lista de pares a entero", y así en. En este caso, una señal de ventaja del sistema Hindley-Milner es que cada término bien tipado tiene un tipo "mejor" único , que se denomina tipo principal . El tipo principal de la función de longitud de lista es "para cualquiera a, función de la lista de aal entero". Aquí ahay un llamado "parámetro de tipo", que es explícito en el cálculo lambda pero implícito en la mayoría de los lenguajes de programación .polimorfismo paramétrico . (Si escribe una definición de la función de longitud en ML, puede ver el parámetro de tipo así:

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

• Si un término tiene un tipo Hindley-Milner, entonces el tipo principal puede inferirse sin requerir declaraciones de tipo u otras anotaciones por parte del programador. (Esta es una bendición mixta, ya que cualquiera puede dar fe de quién ha manejado una gran parte del código ML sin anotaciones).

Hindley-Milner es la base del sistema de tipos de casi todos los lenguajes funcionales tipados estáticamente. Tales lenguajes de uso común incluyen

• La familia ML ( ML estándar y Caml objetivo )
• Haskell
• Limpiar

Todos estos idiomas han extendido Hindley-Milner; Haskell, Clean y Objective Caml lo hacen de formas ambiciosas e inusuales. (Se requieren extensiones para tratar con variables mutables, ya que Hindley-Milner básico se puede subvertir usando, por ejemplo, una celda mutable que contiene una lista de valores de tipo no especificado. Estos problemas se tratan mediante una extensión llamada restricción de valor ).

Muchos otros lenguajes y herramientas menores basados ​​en lenguajes funcionales mecanografiados utilizan Hindley-Milner.

Hindley-Milner es una restricción del Sistema F , que permite más tipos pero que requiere anotaciones por parte del programador .

Puede encontrar los documentos originales utilizando Google Scholar o CiteSeer, o la biblioteca de su universidad local. El primero es lo suficientemente viejo como para que tengas que encontrar copias encuadernadas del diario, no pude encontrarlo en línea. El enlace que encontré para el otro estaba roto, pero podría haber otros. Ciertamente podrá encontrar documentos que citan estos.

Hindley, Roger J, El esquema de tipo principal de un objeto en lógica combinatoria , Transactions of the American Mathematical Society, 1969.

Milner, Robin, A Theory of Type Polymorphism , Journal of Computer and System Sciences, 1978.

Implementación de inferencia de tipo Hindley-Milner simple en C #:

Inferencia de tipo Hindley-Milner sobre expresiones S (Lisp-ish), en menos de 650 líneas de C #

Tenga en cuenta que la implementación está en el rango de solo 270 líneas de C # (para el algoritmo W adecuado y las pocas estructuras de datos que lo admiten, de todos modos).

Extracto de uso:

    // ...

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

    // ...

... cuyos rendimientos:

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.

Vea también la implementación de JavaScript de Brian McKenna en bitbucket, que también ayuda a comenzar (funcionó para mí).

«HTH