Cos’è Hindley-Milner?

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

Ho letto i seguenti post:

  • Steve Yegge – Dynamic Languages ​​Strike Back
  • Steve Yegge – Il problema di Pinocchio
  • Daniel Spiewak – Che cos’è Hindley-Milner? (e perché è bello?)

Ma non c’è una singola voce per questo termine in wikipedia dove di solito mi offre una spiegazione concisa.
Nota : ne è stato aggiunto uno

Che cos’è?
Quali lingue e strumenti implementano o usano?
Per favore, offrite una risposta concisa?

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

  • Supporta funzioni polimorfiche ; per esempio, una funzione che può darti la lunghezza della lista indipendentemente dal tipo di elementi, oppure una funzione fa una ricerca ad albero binario indipendente 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 di lunghezza: può essere “lista di interi in numeri interi”, “lista di stringhe in numeri interi”, “lista di coppie in numeri interi”, e così via sopra. In questo caso, un vantaggio di segnale del sistema Hindley-Milner è che ogni termine ben tipizzato ha un unico tipo “migliore” , che è chiamato il tipo principale . Il tipo principale della funzione list-length è “per ogni a , funzione dall’elenco di a all’intero”. Qui a è un cosiddetto “parametro di tipo”, che è esplicito nel calcolo lambda ma implicito nella maggior parte dei linguaggi di programmazione . L’uso dei parametri di tipo spiega perché Hindley-Milner è un sistema che implementa il polimorfismo parametrico . (Se si scrive una definizione della funzione di lunghezza in ML, è ansible vedere il parametro tipo in questo modo:

      fun 'a length [] = 0 | 'a length (x::xs) = 1 + length xs 
  • Se un termine ha un tipo Hindley-Milner, allora il tipo principale può essere dedotto senza richiedere dichiarazioni di tipo o altre annotazioni da parte del programmatore. (Questa è una benedizione mista, in quanto chiunque può attestare chi sia mai stato 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

  • La famiglia ML ( Standard ML e Objective Caml )
  • Haskell
  • Pulito

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

Molte altre lingue e strumenti minori basati su linguaggi funzionali digitati utilizzano Hindley-Milner.

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

Potresti riuscire a trovare i documenti originali utilizzando Google Scholar o CiteSeer o la tua biblioteca universitaria locale. Il primo è abbastanza vecchio da dover trovare copie rilegate del diario, non potrei trovarlo online. Il collegamento che ho trovato per l’altro era rotto, ma potrebbero essercene altri. Sarai certamente in grado di trovare documenti che citano questi.

Hindley, Roger J, Lo schema tipo principale di un object in logica combinatoria , Transactions of the American Mathematical Society, 1969.

Milner, Robin, una teoria del tipo polimorfismo , rivista di informatica e scienze del sistema, 1978.

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

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

Notare che l’implementazione è nell’intervallo di solo 270 linee di C # (per l’algoritmo W corretto e le poche strutture dati per supportarlo, comunque).

Estratto di 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 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 ( ( fg ) => ( ( x ) => ( f ( gx ) ) ) ) ) // composition ( factorial ( ( n ) => ( if ( > n 0 ) ( * n ( factorial ( - n 1 ) ) ) 1 ) ) ) // More interesting.. ( fmap ( ( fl ) => ( 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 HM // (see Node, et al, above) and infer some types from the latter analyze(source); // ... 

… che produce:

 id : Function<`u, `u> o : Function, Function<`y, `z>, Function<`y, `aa>> factorial : Function fmap : Function, List<`au>, List<`ax>> ... Done. 

Vedi anche l’implementazione JavaScript di Brian McKenna su bitbucket, che aiuta anche a iniziare (ha funzionato per me).

‘HTH,