Algoritmo Hindley-Milner: utilizzo dei tipi per garantire l'applicazione dei binding

Question

Sto implementando l'algoritmo di inferenza del tipo Hindley-Milner, seguendo le esercitazioni di Mark Jones e Oleg Kiselyov. Entrambi questi hanno un'operazione "applica binding" con un tipo di forma approssimativamente

applyBindings :: TyEnv -> Type -> Type 

che applica i tyvar -> ty binding in TyEnv alla data Type. Ho trovato un errore comune nel mio codice dimenticare di chiamare applyBindings e non ottengo alcun aiuto dal sistema di tipi Haskell, dal momento che lo ty ha lo stesso tipo di applyBindings tyenv ty. Sto cercando un modo per far rispettare la seguente invariante nel sistema tipo:

quando si fa inferenza di tipo, attacchi devono essere applicate prima di restituire un risultato 'finale'

Quando fare inferenza di tipo per un lingua oggetto monomorfica, c'è un modo naturale per far rispettare questo, come attuato in ng scricciolo di Thornton unification-fd package: si definiscono due tipi di dati per Type s:

-- | Types not containing unification variables 
type Type = ...   -- (Fix TypeF) in wren's package 

-- | Types possibly containing unification variables 
type MutType = ...  -- (MutTerm IntVar TypeF) in wren's package 

e dare applyBindings del tipo

-- | Apply all bindings, returning Nothing if there are still free variables 
-- otherwise just 
applyBindings :: TyEnv -> MutType -> Maybe Type 

(questa funzione è effettivamente freeze . applyBindings dell'unificazione-fd). Ciò impone la nostra invariante: se dimentichiamo di applyBindings, otterremo un errore di tipo.

Questo è il tipo di soluzione che sto cercando, ma per le lingue oggetto con polimorfismo. L'approccio di cui sopra, così com'è, non si applica, dal momento che i nostri tipi di linguaggio oggetto possono avere variabili di tipo - in effetti, se ci sono variabili libere dopo l'applicazione di bind, non vogliamo restituire Nothing, ma vogliamo generalizzare oltre queste variabili.

Esiste una soluzione lungo le linee che descrivo, ad esempio una che fornisce applyBindings un tipo diverso da const id? I compilatori reali usano lo stesso punning (tra le variabili di unificazione e le variabili di tipo linguaggio oggetto) che fanno le esercitazioni di Mark e di Oleg?

Answer 1

sto prendendo una pugnalata al buio qui, perché penso che ci possono essere altri problemi con la soluzione che proponete, ma posso affrontare almeno una difficoltà:

• Il tipo di controllo dovrebbe avere diverse rappresentazioni per variabili di tipo unificazione e variabili di tipo linguaggio oggetto.

Questa variazione non è difficile da implementare, e in effetti penso che il controllo del tipo di GHC abbia funzionato in questo modo, almeno in una volta. Potresti voler controllare il documento Practical Type Inference for Arbitrary-Rank Types; l'appendice contiene molto codice molto utile.