Descrivi l'inferenza di tipo Damas-Milner in modo che uno studente CS101 possa capire

Question

Hindley-Milner è un sistema di tipi che è alla base dei sistemi di tipi di molti ben noti linguaggi di programmazione funzionale. Damas-Milner è un algoritmo che deduce (deduce?) Tipi in un sistema di tipo Hindley-Milner.

Wikipedia fornisce una descrizione dell'algoritmo che, per quanto posso dire, equivale a una singola parola: "unificazione". È tutto lì? Se è così, ciò significa che la parte interessante è il sistema di tipo in sé e non il sistema di inferenza di tipo.

Se Damas-Milner è più dell'unificazione, vorrei una descrizione di Damas-Milner che includa un semplice esempio e, idealmente, un codice.

Inoltre, si dice spesso che questo algoritmo faccia inferenza di tipo. È davvero un sistema di inferenza? Pensavo che fosse solo la deduzione dei tipi.

domande correlate:

• What is Hindley Miller?
• Type inference to unification problem

Answer 1

Damas Milner è solo un uso strutturato di unificazione.

Quando ricorre in un'espressione lambda, costituisce un nuovo nome di variabile. Quando, in un sotto-termine, trovi quella variabile usata in un modo che richiederebbe un determinato tipo, registra l'unificazione di quella variabile e quel tipo. Se mai tenta di unificare due tipi che non hanno senso, come dire che una variabile individuale è sia un Int che una funzione da un -> b, allora ti urla addosso per aver fatto qualcosa di male.

Inoltre, si dice spesso che questo algoritmo faccia un'inferenza di tipo. È davvero un sistema di inferenza? Pensavo che fosse solo la deduzione dei tipi.

Dedurre i tipi è un'inferenza di tipo. Il controllo per vedere che le annotazioni del tipo sono valide per un determinato termine è il controllo del tipo. Sono problemi diversi.

In tal caso, ciò significa che la parte interessante è il tipo di sistema in sé e non il sistema di inferenza del tipo.

Si dice comunemente che i sistemi tipo stile Hindley-Milner sono bilanciati a cuspide. Se aggiungi molte più funzionalità diventa impossibile dedurne i tipi. Quindi digitare le estensioni di sistema che puoi sovrapporre a un sistema di tipo di stile Hindley-Milner senza distruggere le sue proprietà di inferenza sono in realtà le parti interessanti dei moderni linguaggi funzionali. In alcuni casi, mescoliamo inferenza di tipo e controllo del tipo, ad esempio in Haskell molte estensioni moderne non possono essere dedotte, ma possono essere verificate, quindi richiedono annotazioni di tipo per funzioni avanzate, come la ricorsione polimorfica.

Answer 2

Wikipedia fornisce una descrizione dell'algoritmo che, per quanto posso dire, equivale a una singola parola: "unificazione". È tutto lì? Se è così, ciò significa che la parte interessante è il sistema di tipo in sé e non il sistema di inferenza di tipo.

IIRC, la parte interessante dell'algoritmo di inferenza di tipo Damas-Milner W è che deduce i tipi più generali possibili.