20
Quali sono i limiti di inferenza del tipo? Quali sistemi di tipi non hanno un algoritmo di inferenza generale?Quali sono i limiti di inferenza di tipo?
A
risposta
11
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.
5
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 ...
Quindi Algorithm W copre il più grande sottoinsieme possibile di System F che è decidibile? –
@ott: Non sono un teorico di tipo a punta, ma scommetto il mio simbolo | - che System F ha sottoinsiemi decidibili multipli e incomparabili. Per non parlare della possibilità di estensioni (GADT, vincoli di uguaglianza, tipi qualificati). È piena occupazione per la folla a punta :-) –
@Norman Ramsey: interessante. Non so se i teorici del tipo sono a punta di puntino, ma i documenti che ho visto sembrano essere molto lontani dalla realtà e non so se la teoria dei tipi diventerà mainstream e ampiamente accettata; devi ancora imparare la ML per capire anche le basi. –