Un algorithme d'unification entre types
Un langage de types:
|
|
| ty |
::= |
ty ® ty | ty * ty | int
| var |
|
Substitution:
Une substitution est une fonction s: var ® ty étendue aux
types telle que:
-
s(t1 ® t2) = s(t1) ® s(t2)
-
s(t1 * t2) = s(t1) * s(t2)
-
s(int) = int
Unification:
Deux types t1 et t2 sont unifiables, ce que l'on notera
t1 º t2, s'il existe une substitution
s telle que:
s(t1) = s(t2)