Pergunta

Eu encontrei este termo Hindley-Milner , e eu não estou certo se entender o que isso significa.

Eu li as seguintes mensagens:

Mas não há nenhuma entrada única para este termo na Wikipedia onde normalmente me oferece uma explicação concisa.
Nota - um tem agora foi adicionado

O que é isso?
Que linguagens e ferramentas de implementação ou usá-lo?
Você poderia por favor oferecer uma resposta concisa?

Foi útil?

Solução

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

  • Ele suporta polimórfica funções; por exemplo, uma função que pode lhe dar o comprimento da lista independente do tipo de elementos, ou uma função faz um binário-árvore de pesquisa 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 comprimento: pode ser "lista de inteiros para inteiro", "lista de strings para integer", 'lista de pares para inteiro', e assim por diante. Neste caso, uma vantagem de sinal do sistema de Hindley-Milner é que cada termo bem tipado tem um "melhor" tipo único , que é chamado de tipo principais . O principal tipo de função a lista de comprimento é "para qualquer a, função da lista de a ao número inteiro". Aqui a é um chamado "parâmetro do tipo", que é explícito no lambda calculus e implícita na maioria das linguagens de programação . O uso de parâmetros de tipo explica por Hindley-Milner é um sistema que implementa paramétrico polimorfismo . (Se você escrever uma definição da função de comprimento no ML, você pode ver o parâmetro de tipo assim: 

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

  • Se um termo tem um tipo de Hindley-Milner, em seguida, o tipo de capital pode ser inferida sem exigir quaisquer declarações de tipo ou outras anotações pelo programador. (Esta é uma faca de dois gumes, como qualquer um pode atestar que já tenha sido tratado um grande pedaço de código ML sem anotações.)

Hindley-Milner é a base para o sistema de tipo de quase todas as línguas funcional de tipagem estática. Tais linguagens de uso comum incluem

Todas as línguas têm estendido Hindley-Milner; Haskell, Clean, and Objective Caml fazê-lo de forma ambiciosas e incomuns. (Extensões são necessárias para lidar com variáveis ??mutáveis, desde básica Hindley-Milner pode ser subvertida utilizando, por exemplo, uma célula mutável segurando uma lista de valores de tipo não especificado. Tais problemas são tratados por uma extensão chamada de restrição de valor .)

Muitas outras línguas menores e ferramentas baseadas em linguagens funcionais digitadas usar Hindley-Milner.

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

Outras dicas

Você pode ser capaz de encontrar os documentos originais usando Google Scholar ou CiteSeer - ou a sua biblioteca da universidade local. O primeiro é o suficiente velho que você pode ter que encontrar cópias encadernadas da revista, eu não poderia encontrá-lo online. O link que eu encontrei para o outro foi quebrado, mas pode haver outros. Você certamente vai ser capaz de encontrar artigos que citam estes.

Hindley, Roger J, O principal esquema de tipo de um objeto na lógica combinatória , Transações da American Mathematical Society de 1969.

Milner, Robin, A Theory of Type Polimorfismo , Jornal de computador eo sistema Ciências de 1978.

Simples Hindley-Milner implementação inferência de tipos em C #:

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

a execução é na gama de apenas 270 ou menos linhas de C # (W para o algoritmo adequado e as poucas estruturas de dados para o suportam, pelo menos).

Uso trecho: 

    // ...

    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 implementação JavaScript do Brian McKenna em bitbucket, o que também ajuda a obter iniciado (trabalhou para mim).

'HTH,

Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow
scroll top