Algoritmo de Hindley-Milner:Usar tipos para garantizar que se apliquen los enlaces.

Question

Estoy implementando el algoritmo de inferencia de tipos Hindley-Milner, siguiendo los tutoriales de Marcos Jones y Oleg Kiseliov.Ambos tienen una operación de "aplicar enlaces" con un tipo aproximadamente de la forma

applyBindings :: TyEnv -> Type -> Type

que aplica el tyvar -> ty fijaciones en TyEnv a lo dado Type.He descubierto que es un error común en mi código olvidarme de llamar applyBindings, y no recibo ayuda del sistema de tipos de Haskell, ya que ty tiene el mismo tipo que applyBindings tyenv ty.Estoy buscando una manera de hacer cumplir la siguiente invariante en el sistema de tipos:

al realizar inferencia de tipos, se deben aplicar enlaces antes de devolver un resultado 'final'

Al realizar inferencia de tipos para un lenguaje de objetos monomórfico, existe una forma natural de aplicar esto, como se implementa en Wren ng Thorton. paquete unificación-fd:definimos dos tipos de datos para Types:

-- | 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

y dar applyBindings el tipo

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

(esta función es en realidad freeze . applyBindings en unificación-fd).Esto refuerza nuestra invariante - si nos olvidamos de applyBindings, entonces obtendremos un error de tipo.

Este es el tipo de solución que estoy buscando, pero para lenguajes de objetos con polimorfismo.El enfoque anterior, tal como está, no se aplica, ya que nuestros tipos de lenguaje objeto pueden tener variables de tipo; de hecho, si hay variables libres después de aplicar enlaces, no queremos devolver Nothing, pero queremos generalizar sobre estas variables.

¿Existe una solución según lo que describo, es decir?uno que da applyBindings un tipo diferente de const id?¿Los compiladores reales utilizan los mismos juegos de palabras (entre variables de unificación y variables de tipo de lenguaje objeto) que utilizan los tutoriales de Mark y Oleg?

Answer 1

Estoy apuñalando en la oscuridad aquí, porque creo que puede haber otros problemas con la solución que propones, pero puedo abordar al menos una dificultad:

• Su verificador de tipo debería tener diferente representaciones para variables de tipo unificación y variables de tipo de lenguaje objeto.

Esta variación no es difícil de implementar y, de hecho, creo que el verificador de tipos GHC funcionó de esta manera, al menos en un momento dado.Tal vez quieras revisar el papel. Inferencia de tipos práctica para tipos de rango arbitrario;El apéndice contiene mucho código muy útil.