Quali sono i limiti di inferenza di tipo?
-
12-09-2019 - |
Domanda
Quali sono i limiti di inferenza di tipo? Quali sistemi di tipo non hanno alcun algoritmo generale di inferenza?
Soluzione
Joe Wells ha mostrato che tipo di inferenza è indecidibile per sistema F, che è la più elementare calcolo polimorfico lambda, scoperto indipendentemente da Girard e Reynolds. Questo è il risultato più importante che mostra i limiti di inferenza di tipo.
Ecco un problema importante che è ancora aperto: qual è il modo migliore per integrare Tipi Generalized algebrica dati in Hindley-Milner inferenza di tipo? Ogni anno Simon Peyton Jones esce con una nuove risposte, che si suppone sia meglio di risposta dell'anno precedente. Non ho letto la versione marzo 2009 e quindi non posso dire se credo che sarà definitiva.
Altri suggerimenti
Un sistema di valori-dipendente-tipo (o in breve sistema di tipo dipendente,) in grado di descrivere i tipi che dicono cose come: "Al tempo di valutazione (runtime), il valore di questa variabile sarà sempre pari al valore di tale variabile , che è calcolato con un diverso processo di valutazione". dedurre automaticamente questo tipo dal codice comporta prove automatiche di teoremi. Se l'insieme di teoremi è possibile esprimere è limitato a quelli automaticamente dimostrabile, che non sarebbe un problema, ma nel caso di lingue dipendente-digitati, questo non è generalmente il caso.
sistemi Quindi dipendentemente digitato non possono avere generale (e completo) l'inferenza di tipo.
Sono sicuro che qualcuno in grado di fornire una risposta formale e completa morale ...