¿Qué es Hindley-Milner?

Daniel, parte de este staff, nos ha hecho el favor de escribir este enunciado ya que conoce muy bien el tema.

Solución:

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

• Es compatible polimórfico funciones; 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 keys almacenado 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 enteros”, “lista de cadenas a enteros”, “lista de pares a enteros”, etc. En este caso, una ventaja de la señal del sistema Hindley-Milner es que cada término bien escrito tiene un tipo “mejor” único, que se llama tipo principal. El tipo principal de la función de longitud de lista es “para cualquier a, función 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 paramétrico polimorfismo. (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 se puede inferir sin requerir ninguna declaración de tipo u otras anotaciones del programador. (Esto es un mixed bendición, como cualquiera puede atestiguar que alguna vez haya 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 tipificados estáticamente. Dichos lenguajes de uso común incluyen

• La familia ML (ML estándar y Objective Caml)
• Haskell
• Limpio

Todos estos idiomas se han extendido al 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 contenga una lista de valores de tipo no especificado. Estos problemas se resuelven mediante una extensión llamada restricción de valor.)

Muchos otros lenguajes menores y herramientas basadas en lenguajes funcionales escritos 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.

Es posible que pueda encontrar los artículos originales utilizando Google Scholar o CiteSeer, o la biblioteca de su universidad local. El primero es lo suficientemente antiguo como para que tenga que encontrar copias encuadernadas del diario, no pude encontrarlo en línea. El vínculo que encontré para el otro estaba roto, pero podría haber otros. Seguramente podrá encontrar artículos que los citen.

Hindley, Roger J, El esquema de tipos principal de un objeto en lógica combinatoria., Transacciones de la American Mathematical Society, 1969.

Milner, Robin, Una teoría del polimorfismo de tipos, Revista de Ciencias de la Computación y Sistemas, 1978.

Implementación simple de inferencia de tipo Hindley-Milner 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 o más líneas de C # (para el algoritmo W propiamente dicho 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();

    // 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
    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