functional programming - ¿Qué es Hindley-Milner?

functional-programming types

Question

Me encontré con este término Hindley-Milner , y no estoy seguro de entender 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 usualmente me ofrece una explicación concisa.
^{Nota : ahora se ha agregado uno}

¿Qué es?
¿Qué idiomas y herramientas implementar o usar?
¿Podría por favor ofrecer una respuesta concisa?

Answer 1

Es posible que pueda encontrar los documentos originales con Google Scholar o CiteSeer, o la biblioteca de su universidad local. La primera es lo suficientemente antigua como para que tenga que encontrar copias encuadernadas de la revista, no pude encontrarla en línea. El enlace que encontré para el otro estaba roto, pero podría haber otros. Seguramente podrá encontrar documentos que los citen.

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

Milner, Robin, Una teoría del tipo de polimorfismo , Revista de informática y ciencias del sistema, 1978.

Answer 2

Hindley-Milner es un sistema de tipos descubierto de forma independiente por Roger Hindley (que estudiaba la lógica) y más tarde por Robin Milner (que estudiaba los 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 los 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 ventaja de la señal del sistema Hindley-Milner es que cada término bien tipado tiene un único "mejor" tipo , que se denomina tipo principal . El tipo principal de la función list-length es "para cualquier función a, de la lista de a a entero". Aquí a es un llamado "parámetro de tipo", que es explícito en cálculo lambda pero implícito en la mayoría de los lenguajes de programación . El uso de parámetros de tipo explica por qué Hindley-Milner es un sistema que implementa 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 de Hindley-Milner, el tipo de principal se puede inferir sin requerir ninguna declaración de tipo u otras anotaciones por parte del programador. (Esto es una bendición mixta, ya que cualquiera puede atestiguar a quién se le ha administrado una gran porción de código ML sin anotaciones).

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

• La familia ML ( Estándar ML y Objetivo Caml )
• Haskell
• Clean

Todos estos lenguajes han extendido a Hindley-Milner; Haskell, Clean y Objective Caml lo hacen de maneras ambiciosas e inusuales. (Se requieren extensiones para manejar variables mutables, ya que el Hindley-Milner básico se puede subvertir usando, por ejemplo, una celda mutable que contiene una lista de valores de tipo no especificado. Tales problemas son tratados por una extensión llamada restricción de valor ).

Muchos otros lenguajes menores y herramientas basadas en lenguajes funcionales tipados usan Hindley-Milner.

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

Answer 3

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

Hindley-Milner tipo de inferencia sobre (Lisp-ish) S-expresiones, 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 soportan, 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.

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

''HTH,