Type inférence au problème de l'unification

Question

Quelqu'un a-t-il une idée de la façon dont le problème d'inférence de type

E > hd (cons 1 nil) : α0

avec l'environnement de frappe

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

peut être transféré dans un problème d'unification?

Toute aide serait vraiment appréciée!

Answer 1

Commencez par renommer les variables de type afin qu'aucune des variables de votre expression ne soit en conflit avec des variables de l'environnement de frappe. (Dans votre exemple, cela est déjà fait puisque l'expression référence {a0} et que l'environnement de frappe référence {a1, a2, a3}.

Deuxièmement, en utilisant de nouvelles variables de type, créez une variable de type pour chaque sous-expression de votre expression, en produisant quelque chose comme:

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

Troisièmement, générez un ensemble d’équations entre les variables de type qui doivent tenir. Vous pouvez le faire de bas en haut, de haut en bas ou d'une autre manière. Voir Heeren, Bastiaan. Messages d'erreur de type qualité supérieure. 2005. pour plus de détails sur les raisons pour lesquelles vous souhaitez choisir l'une ou l'autre manière. Cela se traduira par quelque chose comme:

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

Notez bien que si la même fonction était utilisée deux fois dans l'environnement de type, nous aurions besoin de plus de nouvelles variables de type (à la deuxième étape, ci-dessus) pour unifier avec, de sorte que nous ne fassions pas accidentellement tous les appels à l'utilisation suivante le même type. Je ne suis pas sûr de savoir comment expliquer cette partie plus clairement, désolé. Ici, nous sommes dans le cas facile, puisque HD et les inconvénients ne sont utilisés qu’une seule fois.

Quatrièmement, unifiez ces équations, ce qui donne (si je ne me suis pas trompé) quelque chose comme:

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

Réjouissez-vous, vous connaissez maintenant le type de chaque sous-expression de votre expression d'origine.

(En guise d’avertissement, je suis moi-même un amateur dans ce domaine et j’ai peut-être commis une erreur typographique ou trompé par mégarde quelque part ici.)