O que é Hindley-Milner?

Encontrei esse termo Hindley-Milner e não sei se entendi o que isso significa.

Eu li os seguintes posts:

• Steve Yegge - Revolução de idiomas dinâmicos
• Steve Yegge - O problema de Pinóquio
• Daniel Spiewak - O que é Hindley-Milner? (e por que é legal?)

Mas não há uma entrada única para esse termo na wikipedia, onde geralmente me oferece uma explicação concisa.
^{Nota - um foi adicionado agora}

O que é isso?
Quais idiomas e ferramentas implementam ou usam?
Você poderia oferecer uma resposta concisa?

Hindley-Milner é um sistema de tipos descoberto independentemente por Roger Hindley (que estava olhando para a lógica) e mais tarde por Robin Milner (que estava olhando para linguagens de programação). As vantagens da Hindley-Milner são

• Ele suporta funções polimórficas ; por exemplo, uma função que pode fornecer o comprimento da lista independente do tipo dos elementos, ou uma função faz uma pesquisa na árvore binária independente do tipo de chaves armazenadas na árvore.

• Às vezes, uma função ou valor pode ter mais de um tipo , como no exemplo da função length: pode ser "lista de números inteiros para número inteiro", "lista de cadeias de caracteres para número inteiro", "lista de pares para número inteiro" e assim por diante em. Nesse caso, uma vantagem de sinal do sistema Hindley-Milner é que cada termo bem digitado possui um tipo "melhor" único , chamado de tipo principal . O tipo principal da função de comprimento da lista é "para qualquer afunção da lista de apara inteiro". Aqui aestá o chamado "parâmetro de tipo", explícito no cálculo lambda, mas implícito na maioria das linguagens de programação .polimorfismo paramétrico . (Se você escrever uma definição da função length em ML, poderá ver o parâmetro type assim:

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

• Se um termo tiver um tipo Hindley-Milner, o tipo principal poderá ser inferido sem exigir nenhuma declaração de tipo ou outras anotações pelo programador. (Esta é uma bênção mista, como qualquer pessoa pode atestar quem já lidou com uma grande parte do código ML sem anotações.)

Hindley-Milner é a base para o sistema de tipos de quase todas as linguagens funcionais estaticamente tipadas. Esses idiomas de uso comum incluem

• A família ML ( ML padrão e Cam Objective )
• Haskell
• Limpar \ limpo

Todas essas línguas estenderam Hindley-Milner; Haskell, Clean e Objective Caml fazem isso de maneiras ambiciosas e incomuns. (São necessárias extensões para lidar com variáveis ​​mutáveis, uma vez que Hindley-Milner básico pode ser subvertido usando, por exemplo, uma célula mutável que contém uma lista de valores de tipo não especificado. Esses problemas são tratados por uma extensão chamada restrição de valor .)

Muitas outras linguagens e ferramentas secundárias baseadas em linguagens funcionais digitadas usam Hindley-Milner.

Hindley-Milner é uma restrição do Sistema F , que permite mais tipos, mas que requer anotações do programador .

Você pode encontrar os documentos originais usando o Google Scholar ou o CiteSeer - ou a biblioteca da universidade local. O primeiro tem idade suficiente para que você possa encontrar cópias encadernadas do diário, não consegui encontrá-lo online. O link que encontrei para o outro estava quebrado, mas pode haver outros. Você certamente encontrará documentos que os citam.

Hindley, Roger J, O esquema principal de um objeto na lógica combinatória , Transactions of the American Mathematics Society, 1969.

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

Implementação simples de inferência do tipo Hindley-Milner em C #:

Inferência do tipo Hindley-Milner sobre expressões S (Lisp-ish), em menos de 650 linhas de C #

Observe que a implementação está no intervalo de apenas 270 linhas de C # (para o algoritmo W adequado e para as poucas estruturas de dados que o suportam).

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

    // ...

... que produz:

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.

Veja também a implementação JavaScript de Brian McKenna no bitbucket, que também ajuda a começar (funcionou para mim).

«HTH,