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 = mem n (vars_of_type t);;
*
occurs : int ® ml_type ® bool = áfunñ
let rec shorten = function
*
Var_type ( ref (Unknown )) as t ® t
*
Var_type (ref (Instanciated (Var_type as t)) as t1) ®
*
let t2 = shorten t in t1 := Instanciated tt2
*
Var_type (ref (Instanciated t)) ® t
*
t ® t
*
;;
*
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 (ref (Unknown n) as occn), Var_type (ref(Unknown m)) ®
*
if n=m then () else occn:= Instanciated lt2
*
Var_type (ref (Unknown n) as occn), ®
*
if occurs n lt2
*
then raise (type_error(Clash(lt1,lt2)))
*
else occn:=Instanciated lt2
*
, Var_type (ref(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)))
*
;;
*
unify_types : ml_type * ml_type ® unit = áfunñ