Fundeps e GADT:Quando è decidibile il controllo del tipo?

Question

Stavo leggendo un documento di ricerca su Haskell e su come viene implementato HList e mi chiedevo quando le tecniche descritte sono e non sono decidibili per il controllo del tipo.Inoltre, poiché puoi fare cose simili con i GADT, mi chiedevo se il controllo del tipo GADT fosse sempre decidibile.

Preferirei le citazioni se le hai, così posso leggere/capire le spiegazioni.

Grazie!

Answer 1

Credo che il controllo del tipo GADT sia sempre decidibile;è un'inferenza che è indecidibile, poiché richiede un'unificazione di ordine superiore.Ma un controllore di tipo GADT è una forma limitata dei controllori di prova che vedi ad es.Coq, dove i costruttori costruiscono il termine di prova.Ad esempio, il classico esempio di incorporamento del lambda calcolo nei GADT ha un costruttore per ciascuno regola di riduzione, quindi se vuoi trovare la forma normale di un termine, devi dirgli quali costruttori ti porteranno a trovarla.Il problema dell'arresto è stato spostato nelle mani dell'utente :-)

Answer 2

Probabilmente lo hai già visto, ma è disponibile una raccolta di articoli su questo problema presso Microsoft Research: Digitare Controllo documenti.Il primo descrive l'algoritmo decidibile effettivamente utilizzato nel compilatore Glasgow Haskell.