Tipo de inferencia al problema de unificación

Question

¿Alguien tiene una idea de cómo el problema de inferencia de tipo

E > hd (cons 1 nil) : α0

con el entorno de escritura

                E={
                   hd : list(α1 ) → α1 ,
                   cons : α2 → list(α2 ) → list(α2 ),
                   nil : list(α3 ),
                   1 : int
                }

se puede transferir en un problema de unificación?

¡Cualquier ayuda sería realmente apreciada!

Answer 1

Primero, cambie el nombre de las variables de tipo para que ninguna de las variables en su expresión colisione con las variables en el entorno de escritura. (En su ejemplo, esto ya está hecho ya que la expresión hace referencia a {a0}, y el entorno de escritura hace referencia a {a1, a2, a3}.

Segundo, usando nuevas variables de tipo, cree una variable de tipo para cada subexpresión dentro de su expresión, produciendo algo como:

nil : a4
1 : a5
cons : a6
(cons 1 nil) : a7
hd : a8
hd (cons 1 nil) : a0 // already had a type variable

Tercero, generar un conjunto de ecuaciones entre las variables de tipo que deben contener. Puede hacerlo de abajo hacia arriba, de arriba hacia abajo o de otras maneras. Ver Heeren, Bastiaan. Mensajes de error de tipo de calidad superior. 2005. para obtener más detalles sobre por qué es posible que desee elegir de una forma u otra. Esto resultará en algo como:

a4 = list(a3) // = E(nil)
a5 = int // = E(1)
a6 = a2 -> list(a2) -> list(a2) // = E(cons)

// now it gets tricky, since we need to deal with application for the first time
a5 = a2 // first actual param of cons matches first formal param of cons
a4 = list(a2) // second actual param of cons matches type of second formal param of cons
a7 = list(a2) // result of (cons 1 nil) matches result type of cons with 2 params

a8 = list(a1) -> a1 // = E(hd)    

// now the application of hd
a7 = list(a1) // first actual param of hd matches type of first formal param of hd
a0 = a1 // result of hd (cons 1 nil) matches result type of hd with 1 param

Tenga en cuenta con cuidado que si la misma función se usara desde el entorno de tipo dos veces, necesitaríamos más variables de tipo nuevas (en el segundo paso, arriba) para unificar, de modo que no haríamos accidentalmente todas las llamadas a contras del mismo tipo No estoy seguro de cómo explicar esta parte más claramente, lo siento. Aquí estamos en el caso fácil, ya que hd y contras solo se usan una vez.

Cuarto, unifique estas ecuaciones, dando como resultado (si no me he equivocado) algo como:

a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int

Alégrate, ahora sabes el tipo de cada subexpresión en tu expresión original.

(Advertencia justa, soy un poco aficionado a mí mismo en estos asuntos, y bien podría haber cometido un error tipográfico o haber hecho trampa involuntariamente en algún lugar aquí).