Nous implémenter l’inférence de type par résolution de systèmes d’équations.
En partant du TD précédent définir des types typ
et prog
pour les types et les programmes de mini-ML sans annotations de type. Les types contiennent en particulier des variables de types indexées par les entiers, pour lesquels on introduit la notation
type tvar = int
Définir une fonction fresh
de type unit -> typ
qui génère une variable de type « fraîche », c’est-à-dire dont l’index est incrémenté à chaque appel.
On introduit le type
type eqs = (typ * typ) list
pour les systèmes d’équations de type. Définir une fonction equations
de type
string * typ) list -> prog -> typ * eqs (
qui prend comme arguments un environnement de typage et un programme et génère un type pour ce programme et un système d’équations à satisfaire. Cette fonction pourra lever une exception Not_typable
lorsque le programme n’est pas typable. Vérifier que pour le programme
(fun x → fun y → 1) true
le type est X
et le système d’équations est de la forme
[Y → (Z → int) = bool → X]
On introduit le type
type subst = tvar -> typ
pour les substitutions de types. Définir
la substitution identité id
de type subst
la fonction replace
de type
tvar -> typ -> subst
telle que replace x a
est la substitution qui remplace x
par a
(et laisse inchangées les autres variables)
Définir une fonction apply
de type subst -> typ -> typ
qui applique une substitution à un type (apply σ t
calcule t[σ]
).
Définir une fonction apply_eqs
de type subst -> eqs -> eqs
qui applique une substitution à un système d’équations.
Définir une fonction comp
de type subst -> subst -> subst
qui calcule la composée de deux substitutions (comp τ σ
calcule la substitution τ∘σ
, telle que t[τ∘σ] = t[σ][τ]
).
Définir une fonction occurs
de type tvar -> typ -> bool
qui indique si une variable apparaît dans un a type.
Définir une fonction unify
de type eqs -> subst
qui calcule un unificateur le plus général d’un système d’équations. La fonction lèvera une exception Not_solvable
si le système n’admet pas de solution.
Définir une fonction infer
de type (string * typ) list -> prog -> typ
qui infère le type principal d’un programme.
Tester votre fonction en vérifiant que
(fun x → x)
a le type X → X
(fun x → fun y → (y, x)) 1
a le type X → (X * int)
(fun f → fun x → f x)
a le type (X → Y) → X → Y
(2 + true)
n’est pas typable(fun x → y)
n’est pas typable(fun x → x x) (fun x → x x)
n’est pas typable(fun f → (f 1, f true)) (fun x → x)
n’est pas typableDans la pratique, l’unification telle que décrite ci-dessus est assez lourde à mettre en place : chaque substitution nécessite de parcourir tous les types pour remplacer les variables. Une technique classique pour éviter cela est d’implémenter les variables par des références, ce qui permet de modifier le contenu de toutes les variables à la fois. On définit donc maintenant le type des variables et le type de types de la façon suivante :
type tvar = Free of int | Link of typ
and typ =
of tvar ref
| TVar ...
Une variable dont la référence contient Free n
est la variable libre d’indice n
, tandis que si elle contient Link a
cela signifie qu’elle a été remplacée par le type a
. On rappelle que le type des références est défini en interne comme un enregistrement de la façon suivante (ne recopiez pas le code ci-dessous) :
type 'a ref = { mutable contents : 'a }
Ceci est utile pour faire du filtrage de motifs sur des références.
En partant du code de la section précédente, dans un nouveau fichier, modifiez le type typ
comme indiqué ci-dessus et copiez le type prog
des programmes.
Définir une fonction fresh
de type unit -> typ
qui crée des variables fraîches.
Définir une fonction occurs
de type int -> typ -> bool
qui détermine si une variable apparaît dans un type.
Définir une fonction eq
de type typ -> typ -> unit
qui rend deux types égaux en substituant des variables si nécessaire. La fonction lèvera une exception Not_typable
si ça n’est pas possible. On fera attention à ne pas créer de types « cycliques » : quand on remplace une variable X
par un type A
, on s’assurera que X
n’apparaît pas dans A
.
Par exemple, eq
appliquée à X → (X, Y)
et int → Z
va remplacer X
par int
et Z
par (int, Y)
.
Définir une fonction infer
de type (string * typ) list -> prog -> typ
qui infère le type le plus général d’un programme.
Tester votre fonction sur les exemples de la section précédente.