3.6 Unification
La grande différence dans l'algorithme de typage du l-calcul et celui présenté ici provient
de l'algorithme d'unification. dans le premier cas, la fonction TYPE retournait la liste
des substitutions (l'unificateur principal UP) à appliquer pour que deux termes t1 et t2
vérifient UP(t1)=UP(t2). Cet algorithme bien que juste n'est pas forcément très efficace. En mini-ML,
Les substitutions trouvées sont immédiatement appliquées aux types en effectuant une modification physique
de ces types.
Deux problèmes se posent :
-
la vérification d'occurrences, quand une variable de type est remplacée par un autre type, ce second
type ne doit pas contenir d'occurrence de cette première variable. La fonction
occurs réalise
ce test.
- Lorsqu'une inconnue se voit attribuer comme valeur une autre inconnue, on crée une chaîne d'indirection
qu'il faut alors simplifier :
Var_type (ref (Var_type ( ref (Instanciated t)))) deviendra alors seulement t.
La fonction shorten réalise ce travail.
# let occurs n t = List.mem n (vars_of_type t);;
val occurs : int -> ml_type -> bool = <fun>
# let rec shorten = function
Var_type (vt) as tt ®
(match !vt with
Unknown _ ® tt
| Instanciated ((Var_type _) as t) ®
let t2 = shorten t in
vt := Instanciated t;
t2
| Instanciated t ® t
)
| t ® t;;
val shorten : ml_type -> ml_type = <fun>
La fonction unify_types prend deux types, modifie leur taille (par la fonction shorten)
et les rend égaux ou échoue.
# let rec unify_types (t1,t2) =
let lt1 = shorten t1 and lt2 = shorten t2
in
match (lt1,lt2) with
| Var_type ( {contents=Unknown n} as occn ),
Var_type {contents=Unknown m} ®
if n=m then () else occn:= Instanciated lt2
| Var_type ({contents=(Unknown n)} as occn), _ ®
if occurs n lt2
then raise (Type_error(Clash(lt1,lt2)))
else occn:=Instanciated lt2
| _ , Var_type ({contents=(Unknown n)}) ® unify_types (lt2,lt1)
| Const_type ct1, Const_type ct2 ®
if ct1=ct2 then () else raise (Type_error(Clash(lt1,lt2)))
| Pair_type (t1,t2), Pair_type (t3,t4) ®
unify_types (t1,t3); unify_types(t2,t4)
| List_type t1, List_type t2 ® unify_types (t1,t2)
| Fun_type (t1,t2), Fun_type (t3,t4) ®
unify_types (t1,t3); unify_types(t2,t4)
| _ ® raise(Type_error(Clash(lt1,lt2)));;
val unify_types : ml_type * ml_type -> unit = <fun>