Stavo leggendo un documento di ricerca su Haskell e su come HList è implementato e mi chiedo quando le tecniche descritte sono e non sono decidibili per il controllo di tipo. Inoltre, poiché puoi fare cose simili con GADT, mi chiedevo se il controllo del tipo GADT fosse sempre decidibile.Fundeps e GADTs: quando si sceglie la verifica del tipo decidibile?
Preferirei citazioni se ne hai, quindi posso leggere/capire le spiegazioni.
Grazie!
Credo che il controllo del tipo GADT sia sempre decidibile; è inferenza che è indecidibile, in quanto richiede una maggiore unificazione degli ordini. Ma un correttore di tipo GADT è una forma ristretta dei correttori di prove che vedi ad es. Coq, dove i costruttori costruiscono il termine di prova. Ad esempio, il classico esempio dell'inclusione del calcolo lambda in GADT ha un costruttore per ciascuna regola di riduzione , quindi se vuoi trovare la forma normale di un termine, devi dire quali costruttori ti porteranno ad esso. Il problema dell'arresto è stato spostato nelle mani dell'utente :-)
Questo è un buon punto. Quindi immagino di essere interessato a quando l'inferenza di tipo GADT di GHC è decidibile. –
Probabilmente l'avete già visto, ma ci sono una raccolta di articoli su questo argomento nella ricerca Microsoft: Type Checking papers. Il primo descrive l'algoritmo decidibile effettivamente usato nel compilatore Haskell di Glasgow.
I documenti di riferimento sono buoni documenti, ma non sembrano rispondere alla mia domanda. –
Questa domanda potrebbe essere meglio indirizzata agli autori del documento di ricerca. È un po 'esoterico per Stack Overflow. (Ho sempre avuto un grande successo contattando i ricercatori per un commento. Di solito sono estasiato * qualcuno * sta leggendo il loro lavoro.) –
Penso che questo atteggiamento (le domande teoriche non hanno alcun rapporto con un forum pragmatico) sia dannoso e obsoleto. Gli approcci pratici dovrebbero essere aperti alle nuove tecnologie, perché queste tecnologie possono probabilmente migliorare le attività quotidiane nel prossimo futuro. es: caratteristiche funzionali in C#/python. – rcreswick
Detto questo, il commento di Chirs è probabilmente corretto, praticamente parlando. Vorrei che non fosse però. – rcreswick