Types principaux en mini-ML

Samuel Mimram

1 Inférence de type par résolution d’équations

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 typable

2 Résolution d’équations en place

Dans 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 =
  | TVar of tvar ref
  ...

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.