Domanda

Ho incontrato questo termine Hindley-Milner, e non sono sicuro di capire cosa significhi.

Ho letto i seguenti post:

Ma non esiste una voce unica per questo termine su Wikipedia dove di solito mi offre una spiegazione concisa.
Nota - uno ha ora è stato aggiunto

Che cos'è?
Quali linguaggi e strumenti lo implementano o lo utilizzano?
Potresti per favore offrire una risposta concisa?

È stato utile?

Soluzione

Hindley-Milner è un sistema di tipi scoperto indipendentemente da Roger Hindley (che studiava la logica) e successivamente da Robin Milner (che studiava i linguaggi di programmazione).I vantaggi di Hindley-Milner sono

  • Supporta polimorfico funzioni;ad esempio, una funzione che può fornire la lunghezza dell'elenco indipendentemente dal tipo degli elementi, oppure una funzione esegue una ricerca nell'albero binario indipendentemente dal tipo di chiavi memorizzate nell'albero.

  • A volte una funzione o un valore può avere più di un tipo, come nell'esempio della funzione lunghezza:può essere "elenco di numeri interi in numeri interi", "elenco di stringhe in numeri interi", "elenco di coppie in numeri interi" e così via.In questo caso, un vantaggio significativo del sistema Hindley-Milner è questo ogni termine ben digitato ha un tipo "migliore" univoco, che si chiama tipo principale.Il tipo principale della funzione di lunghezza dell'elenco è "for any a, funzione dall'elenco di a all'intero".Qui a è un cosiddetto "parametro di tipo", ovvero esplicito nel lambda calcolo Ma implicito nella maggior parte dei linguaggi di programmazione.L'uso dei parametri di tipo spiega perché Hindley-Milner è un sistema che implementa parametrico polimorfismo.(Se scrivi una definizione della funzione di lunghezza in ML, puoi vedere il parametro di tipo in questo modo:

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

  • Se un termine ha quindi un tipo Hindley-Milner il tipo principale può essere dedotto senza richiedere alcuna dichiarazione di tipo o altre annotazioni del programmatore.(Questa è una benedizione mista, come può attestare chiunque abbia mai gestito una grossa porzione di codice ML senza annotazioni.)

Hindley-Milner è la base per il sistema di tipi di quasi tutti i linguaggi funzionali tipizzati staticamente.Tali lingue di uso comune includono

Tutte queste lingue hanno esteso l'Hindley-Milner;Haskell, Clean e Objective Caml lo fanno in modi ambiziosi e insoliti.(Le estensioni sono necessarie per gestire le variabili mutabili, poiché l'Hindley-Milner di base può essere sovvertito utilizzando, ad esempio, una cella mutabile che contiene un elenco di valori di tipo non specificato.Tali problemi vengono risolti da un'estensione chiamata the restrizione di valore.)

Molti altri linguaggi e strumenti minori basati su linguaggi funzionali digitati utilizzano Hindley-Milner.

Hindley-Milner è una restrizione di Sistema F, che consente più tipi ma quale richiede annotazioni da parte del programmatore.

Altri suggerimenti

Potresti riuscire a trovare i documenti originali utilizzando Google Scholar o CiteSeer o la biblioteca universitaria locale.Il primo è abbastanza vecchio che potresti dover trovare copie rilegate del diario, non sono riuscito a trovarlo online.Il collegamento che ho trovato per l'altro era interrotto, ma potrebbero essercene altri.Sarai sicuramente in grado di trovare documenti che li citano.

Hindley, Roger J, Lo schema dei tipi principali di un oggetto in logica combinatoria, Transazioni della Società Matematica Americana, 1969.

Milner, Robin, Una teoria del polimorfismo dei tipi, Giornale di scienze informatiche e di sistema, 1978.

Semplice implementazione dell'inferenza di tipo Hindley-Milner in C#:

Inferenza di tipo Hindley-Milner su espressioni S (Lisp), in meno di 650 righe di C#

Nota che l'implementazione è nell'ordine di sole 270 righe circa di C# (per l'algoritmo W vero e proprio e le poche strutture dati per supportarlo, comunque).

Estratto di utilizzo:

    // ...

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

    // ...

...che produce:

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.

Guarda anche Implementazione JavaScript di Brian McKenna su bitbucket, che aiuta anche a iniziare (ha funzionato per me).

'HTH,

Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow
scroll top