Quali sono i limiti di inferenza di tipo?

Question

Quali sono i limiti di inferenza del tipo? Quali sistemi di tipi non hanno un algoritmo di inferenza generale?

Answer 1

Joe Wells ha mostrato che tipo di inferenza è indecidibile per il sistema   F, che è la più elementare calcolo polimorfico lambda, scoperto indipendentemente da Girard e Reynolds . Questo è il risultato più importante che mostra i limiti dell'inferenza di tipo.

Ecco un problema importante che è ancora aperto: qual è il modo migliore per integrare i tipi di dati algebrici generalizzati in inferenza di tipo Hindley-Milner? Ogni anno Simon Peyton Jones propone nuove risposte, che è presumibilmente migliore della risposta dell'anno precedente. Non ho letto la versione di marzo 2009 e quindi non posso dire se credo che sarà definitiva.

Answer 2

Un sistema di tipo valore dipendente (o in breve, sistema di tipo dipendente) può descrivere tipi che dicono cose come: "Al momento della valutazione (runtime), il valore di questa variabile sarà sempre uguale al valore di quello variabile, che viene calcolata con un diverso processo di valutazione ". La deduzione automatica di questo tipo dal codice comporta prove automatiche di teoremi. Se l'insieme di teoremi che puoi esprimere è limitato a quelli automaticamente dimostrabili, non sarebbe un problema, ma nel caso di linguaggi tipizzati in modo dipendente, questo in genere non è il caso.

Quindi i sistemi tipizzati in modo dipendente non possono avere l'inferenza di tipo generale (e completa).

Sono sicuro che qualcuno in grado di fornire una risposta formale e completa morale ...