2.2 Synthèse par unification
2.2.1 Unification
On va rappeler l'algorithme d'unification, dans le cas simple qui est le
nôtre. On considère une signature ne comportant qu'un seul symbole, une
fonction a d'arité 2 (c'est la flèche ® des types).
Les variables que nous considérerons sont celles de l'ensemble P.
Rappelons qu'une substitution est une application
P® T ( T est l'ensemble des termes bâtis sur cette signature),
et qu'on peut appliquer une substitution s à un terme sÎ T, ce
qui donne un terme s s :
-
xs=s(x)
- (a(s,t))s=a(s s,t s)
Cela permet de définir la composée s;t de deux substitutions
comme une substitution.
Le problème consiste à résoudre des équations dans cette signature,
et de trouver la solution la plus générale possible. Pour donner un sens
à cela, il faut mettre un ordre sur les substitutions.
Définition 4 On dit que s est plus général que t s'il existe une substitution
u telle que u;s=t.
Si s,tÎ T, unifier s et t, c'est trouver une
substitution s telle que s s=t s. Alors le résultat est le
suivant :
Théorème 4 Pour tous s,tÎ T unifiable, il existe un unificateur qui est
plus général que tous les autres. On l'appelle unificateur principal,
et on le note UP(s,t).
La preuve de ce théorème ne présente d'intérêt que par l'algorithme
d'unification qu'elle propose, qui calcule cet unificateur principal ou
échoue. Nous rappelons à présent cet algorithme. On remarquera qu'ici
la seule cause d'échec possible est celle qui résulte du test d'occurrence
d'une variable.
On notera [s/a] la substitution qui envoie a sur s
et toutes les autres variables sur elles-mêmes. Alors, on définit la
fonction UP qui prend deux termes et rend une substitution inductivement
par :
-
UP(a,s)=[s/a] si a ne figure pas dans s, et
echec si non.
- UP(s,a)=[s/a] si a ne figure pas dans s, et
echec si non.
- si s=UP(s,s') et t=UP(t s,t' s), alors
UP(a(s,t),a(s',t')=t;s).
Justification de l'algorithme (ce n'est pas une preuve rigoureuse).
Le seul cas non trivial est celui où l'on a à unifier
a(s1,t1) avec a(s2,t2). Alors si
s=UN(s1,s2), alors s1 s= s2 s et si
t=UN(t1 s, t2 s), alors (t1 s)t=(t2 s)t, c'est-à-dire
t1 u=t2 u où u=t;s. On voit facilement que u est un
unificateur de nos deux termes de départ.
Voici l'algorithme d'unification dans le cas des types simples.
La syntaxe abstraite des types :
type Type = Tvar of string Arrow of Type * Type;;
*
Type Type defined.
On représente les substitutions par des listes de couples
chaîne de caractère, terme, Voici l'application d'une substitution
à un type :
let substitute s =
*
let rec sub_rec = function
*
(Tvar a) as alpha ® (try assoc a s with Not_found ® alpha)
*
Arrow(T1,T2) ® Arrow(sub_rec T1, sub_rec T2)
*
in sub_rec
*
;;
*
substitute : (string * Type) list ® Type ® Type = áfunñ
et voici la composition de deux substitutions :
let compsubst s t =
*
(map (function (a,T) ® (a,substitute s T)) t) @ s;;
*
compsubst : (string * Type) list ® (string * Type) list ® (string * Type) list
*
= áfunñ
La fonction occur teste l'existence
d'une variable dans un type.
let occur a =
*
let rec occ_rec = function
*
Tvar b ® b=a
*
Arrow(T1,T2) ® occ_rec T1 or occ_rec T2
*
in occ_rec
*
;;
*
occur : string ® Type ® bool = áfunñ
La fonction unify calcule l'unificateur principal pour deux types simples.
Elle retourne cet unificateur quand il existe ou échoue en déclenchant l'exception
Failure "unify".
let rec unify = function
*
(Tvar a), T ®
*
if T=Tvar a then [ ]
*
else if occur a T then raise (Failure ``unify'')
*
else [ a,T ]
*
T,Tvar a ® if occur a T then raise (Failure ``unify'')
*
else [ a,T ]
*
Arrow(S1,S2), Arrow(T1,T2) ®
*
let s=unify(S1,T1)
*
in
*
compsubst (unify(substitute s S2,
*
substitute s T2)) s;;
*
unify : Type * Type ® (string * Type) list = áfunñ
Les exemples suivants calculent l'unificateur principal de deux types.
Cette substitution est ensuite appliquée aux types pour vérifier
leur égalité après substitution.
-
Un des cas les plus simples où une variable de type est substituée par une autre :
let T1=(Tvar ``
x'');;
*
T1 : Type = Tvar ``x''
let T2=(Tvar ``y'');;
*
T2 : Type = Tvar ``y''
let s1 = unify (T1,T2);;
*
s1 : (string * Type) list = [ ``x'', Tvar ``y'' ]
substitute s1 T1 = substitute s1 T2;;
*
- : bool = true
- Un cas classique où une variable est substituée par un type fonctionnel :
let T3 = (Arrow (Tvar ``
a'', Arrow (Tvar ``b'',Tvar ``c'')));;
*
T3 : Type = Arrow (Tvar ``a'', Arrow (Tvar ``b'', Tvar ``c''))
let T4 = (Arrow (Arrow (Tvar ``d'',Tvar ``e''), (Arrow (Tvar ``f'',Tvar ``g''))));;
*
T4 : Type = Arrow (Arrow (Tvar ``d'', Tvar ``e''), Arrow (Tvar ``f'', Tvar ``g''))
let s2 = unify (T3,T4);;
*
s2 : (string * Type) list = [ ``a'', Arrow (Tvar ``d'', Tvar ``e'') ``b'', Tvar ``f''
*
``c'', Tvar ``g'' ]
substitute s2 T3;;
*
- : Type = Arrow (Arrow (Tvar ``d'', Tvar ``e''), Arrow (Tvar ``f'', Tvar ``g''))
substitute s2 T4;;
*
- : Type = Arrow (Arrow (Tvar ``d'', Tvar ``e''), Arrow (Tvar ``f'', Tvar ``g''))
- Un exemple où l'unification fait disparaitre presque toutes les
variables :
let T5 = (Arrow (Arrow (Tvar ``
d'',Tvar ``a''), (Arrow (Tvar ``a'',Tvar ``g''))));;
*
T5 : Type = Arrow (Arrow (Tvar ``d'', Tvar ``a''), Arrow (Tvar ``a'', Tvar ``g''))
let T6 = (Arrow (Arrow (Tvar ``a'',Tvar ``e''), (Arrow (Tvar ``a'',Tvar ``d''))));;
*
T6 : Type = Arrow (Arrow (Tvar ``a'', Tvar ``e''), Arrow (Tvar ``a'', Tvar ``d''))
let s3 = unify (T5,T6);;
*
s3 : (string * Type) list = [ ``d'', Tvar ``e'' ``a'', Tvar ``e'' ``g'', Tvar ``e'' ]
substitute s3 T5 = substitute s3 T6;;
*
- : bool = true
- Enfin un cas d'échec :
unify (T3,T5);;
*
Uncaught exception: Failure "unify"
On peut maintenant donner l'algorithme de typage.
2.2.2 Typage
On définit une fonction T qui prend un contexte et un terme M et rend
un couple constitué d'une substitution et du type cherché pour M
dans ce contexte (on produit le type le plus général possible).
Cette substitution rendue par l'algorithme s'applique aux variables de type
du contexte, et contient les contraintes produites par le typage du terme.
-
T(x,C)=(C(x),id)
- Pour calculer T(l x.M,C), on introduit une nouvelle variable de type
a, et on essaie de typer M dans le nouveau contexte (x:a)C ;
soit (s,s)=T(M,(x:a)C). Alors le type cherché est
s(a)®s, et on rend la substitution s.
- Pour calculer T(MN,C), on calcule
(s,s)=T(M,C), et (t,t)=T(N,Cs), car il faut tenir compte des
contraintes induites par le typage de M. On veut pouvoir appliquer M à
N, et pour cela il faut que M ait un type fonctionnel dans le contexte
courant, c'est-à-dire que s t soit de la forme t®f
où f est un type à déterminer. Pour cela, on calcule
l'unificateur principal u de s t et t®a où a est une
nouvelle variable de type. On rend le type
u(a), et la substitution u;t;s.
Voici le programme de typage en Caml :
Le type term pour la représentation des l-termes et la fonction
gensym pour la création des variables de type sont définis ainsi :
type term= Var of string
*
2 Abs of string * term
*
2 App of term * term;;
*
Type term defined.
let gensym =
*
let c = ref 0 in
*
function s ® (c:=!c+1 s^(string_of_int !c));;
*
gensym : string ® string = áfunñ
La fonction suivante TYPE suit très exactement l'algorithme de typage indiqué
ci-dessus.
let rec TYPE C = function
*
Var x ® assoc x C , [ ]
*
Abs(x,M) ® let alpha=gensym ``a''
*
in
*
let (sigma,s) = TYPE ((x,Tvar alpha)::C) M
*
in
*
Arrow( (try assoc alpha s with ® Tvar alpha),
*
sigma), s
*
App(M,N) ® let (sigma,s)=TYPE C M
*
in
*
let (tau,t) = TYPE (map (function (x,phi) ®
*
(x,substitute s phi)) C) N
*
in
*
let alpha=gensym ``a''
*
in
*
let u= unify(substitute t sigma, Arrow(tau,Tvar alpha))
*
in
*
(try assoc alpha u with ® Tvar alpha),
*
compsubst u (compsubst t s)
*
;;
*
TYPE : (string * Type) list ® term ® Type * (string * Type) list = áfunñ
La fonction print_type donne un affichage lisible des types.
let print_type t =
*
let rec ptype = function
*
Tvar x ® print_string x
*
Arrow (x,y) ® print_string ``('' ptype xprint_string `` -> ''
*
ptype yprint_string ``)''
*
in
*
ptype tprint_newline()
*
;;
*
print_type : Type ® unit = áfunñ
Les exemples suivants reprennent des termes déjà définis.
-
A :
let A = Abs ( ``
x'' , Abs (``y'' , App (Var ``x'', Var ``y'') ));;
*
A : term = Abs (``x'', Abs (``y'', App (Var ``x'', Var ``y'')))
TYPE [ ] A;;
*
- : Type * (string * Type) list = Arrow (Arrow (Tvar ``a2'', Tvar ``a3''),
*
Arrow (Tvar ``a2'', Tvar ``a3'')),
*
[ ``a1'', Arrow (Tvar ``a2'', Tvar ``a3'') ]
print_type (fst (TYPE [ ] A));;
*
((a5 -> a6) -> (a5 -> a6))
*
- : unit = ()
- S :
let S = Abs( ``
x'' ,
*
Abs ( ``y'' ,
*
Abs ( ``z'', App ( App (Var ``x'' , Var ``z'' ) ,
*
App (Var ``y'',Var ``z'') ) )));;
*
S : term = Abs (``x'', Abs (``y'', Abs (``z'', App (App (Var ``x'', Var ``z''),
*
App (Var ``y'', Var ``z'')))))
print_type (fst (TYPE [ ] S));;
*
((a9 -> (a11 -> a12)) -> ((a9 -> a11) -> (a9 -> a12)))
*
- : unit = ()
- D :
let delta = Abs ( ``
x'' , App (Var ``x'' , Var ``x'' ));;
*
delta : term = Abs (``x'', App (Var ``x'', Var ``x''))
print_type (fst (TYPE [ ] delta));;
*
Uncaught exception: Failure "unify"