TD 4 - Algorithme W

Le but de ce TD est de programmer l'algorithme W pour mini-ML. On va considérer une version avec unification destructive.

Question 1. Types et variables de types

On commence par introduire la syntaxe abstraite des types.

type typ = 
  | Tint 
  | Tarrow of typ * typ
  | Tproduct of typ * typ
  | Tvar of tvar

and tvar = 
  { id : int; 
    mutable def : typ option }

Le type typ des types de mini-ML est mutuellement récursif avec le type tvar des variables de types. En effet, une variable de type contient une éventuelle définition (obtenue lors d'une unification), qui est un type. Ainsi { id = 1; def = None } est "encore" une variable de type, mais { id = 2; def = Some Tint } est une ancienne variable de type qui a été définie comme étant égale au type Tint et qui doit donc être désormais traitée exactement comme s'il s'agissait du type Tint. Pour faciliter la gestion des variables de types, on va introduire deux fonctions qui normalisent une expression de type en suivant les définitions contenues dans les variables de types.

Écrire une fonction

  val head : typ -> typ

qui normalise un type en tête, i.e., head t renvoie un type égal à t qui n'est pas de la forme Tvar { def = Some _}. Dit autrement, head t suit les définitions de variable de types en tête de t, tant qu'il y en a.

Écrire une fonction

  val canon : typ -> typ

qui normalise un type en intégralité, i.e., qui applique la fonction head ci-dessus en profondeur. Cette deuxième fonction sera utilisée uniquement pour l'affichage des types (dans le résultat d'une opération de typage ou dans les messages d'erreur).

Question 2. Unification

Pour signaler les erreurs d'unification, on se donne l'exception et la fonction suivante :

exception UnificationFailure of typ * typ

let unification_error t1 t2 = raise (UnificationFailure (canon t1, canon t2))

Écrire une fonction

  val occur : tvar -> typ -> bool

qui teste l'occurrence d'une variable de type dans un type (occur-check). On pourra supposer que la variable est non définie. En revanche, le type peut contenir des variables définies et il conviendra de lui appliquer head avant de l'examiner.

Écrire une fonction

  val unify : typ -> typ -> unit

réalisant l'unification de deux types. Là encore, il conviendra d'utiliser la fonction head sur les types passés en argument avant de les examiner.

Question 3. Variables libres d'un type

Pour construire l'ensemble des variables libres d'un type, on va utiliser le module Set de Caml. Pour cela, on commence par introduire un module V encapsulant le type tvar avec une fonction de comparaison. On en profite pour ajouter la fonction qui crée une nouvelle variable de type.

module V = struct
  type t = tvar
  let compare v1 v2 = Pervasives.compare v1.id v2.id
  let create = let r = ref 0 in fun () -> incr r; { id = !r; def = None }
end

On peut alors instancier le foncteur Set.Make :

module Vset = Set.Make(V)

Écrire une fonction

  val fvars : typ -> Vset.t

qui calcule l'ensemble des variables libres d'un type. Une fois encore, il convient d'utiliser la fonction head à bon escient pour ne considérer que les variables qui ne sont pas définies.

Question 4. Environnement de typage

On définit le type Caml suivant pour les schémas de types :

type schema = { vars : Vset.t; typ : typ }

On introduit alors des dictionnaires utilisant des chaînes de caractères comme clés

module Smap = Map.Make(String)

puis le type Caml suivant pour les environnements de typage :

type env = { bindings : schema Smap.t; fvars : Vset.t }

Le premier champ, bindings, contient les éléments de l'environnement de typage. Le second, fvars, contient l'ensemble de toutes les variables de types libres dans les entrées de bindings. Le champ fvars n'est là que pour éviter de recalculer à chaque fois l'ensemble des variables libres de l'environnement lors de l'opération de généralisation. Note : certaines de ces variables peuvent être définies entre le moment où elles se retrouvent dans cet ensemble et le moment où celui-ci est utilisé. Il conviendra donc de mettre à jour cet ensemble avant de s'en servir (par exemple en appliquant fvars (Tvar v) à chaque variable v et en faisant l'union des résultats).

Définir l'environnement de typage vide :

  val empty : env

Écrire la fonction

  val add : string -> typ -> env -> env

qui ajoute un élément dans un environnement de typage sans généralisation (elle sera utilisée pour le typage d'une fonction). On n'oubliera pas de mettre à jour le champ fvars de l'environnement.

Écrire la fonction

  val add_gen : string -> typ -> env -> env

qui ajoute un élément dans un environnement de typage en généralisant son type par rapport à toutes ses variables de types libres n'apparaissant pas dans l'environnement (elle sera utilisée dans le typage d'un let).

Écrire la fonction

  val find : string -> env -> typ

qui renvoie le type associé à un identificateur dans un environnement, après avoir remplacé toutes les variables du schéma correspondant par des variables de types fraîches. Attention : il peut y avoir plusieurs occurrences de la même variable dans le type et il convient bien entendu de les remplacer toutes par la même variable fraîche.

Question 5. Algorithme W

On se donne le type suivant pour les expressions de mini-ML :

type expression =
  | Var of string
  | Const of int
  | Op of string
  | Fun of string * expression
  | App of expression * expression
  | Pair of expression * expression
  | Let of string * expression * expression

Écrire la fonction

  val w : env -> expression -> typ

réalisant l'algorithme W.

Pour tester, on utilisera la fonction suivante

let typeof e = canon (w empty e)

Quelques tests positifs (l'expression en claire et le type attendu sont indiqués entre parenthèses) :

(* 1 : int *)
```
let t1 = typeof (Const 1)
```
(* fun x -> x : 'a -> 'a *)
```
let t2 = typeof (Fun ("x", Var "x")) 
```

(* fun x -> x+1 : int -> int *)

let t3 = typeof (Fun ("x", App (Op "+", Pair (Var "x", Const 1))))

(* fun x -> x+x : int -> int *)

let t4 = typeof (Fun ("x", App (Op "+", Pair (Var "x", Var "x"))))

(* let x = 1 in x+x : int *)

let t5 = typeof (Let ("x", Const 1, App (Op "+", Pair (Var "x", Var "x"))))

(* let id = fun x -> x in id 1 *)

let t6 = typeof (Let ("id", Fun ("x", Var "x"), App (Var "id", Const 1)));;

(* let id = fun x -> x in id id 1 *)

let t7 = typeof (Let ("id", Fun ("x", Var "x"), 
		     App (App (Var "id", Var "id"), Const 1)));;

(* let id = fun x -> x in (id 1, id (1,2)) : int * (int * int) *)

let t8 = typeof (Let ("id", Fun ("x", Var "x"),
		     Pair (App (Var "id", Const 1),
		     			  App (Var "id", Pair (Const 1, Const 2)))));;

Quelques tests négatifs :

(* 1 2 *)

let _ = typeof (App (Const 1, Const 2))

(* fun x -> x x *)

let _ = typeof (Fun ("x", App (Var "x", Var "x")))

(* (fun f -> +(f 1)) (fun x -> x) *)

let _ = typeof (App (Fun ("f", App (Op "+", App (Var "f", Const 1))),
	             Fun ("x", Var "x")));;

(* fun x -> (x 1, x (1,2)) *)

let _ = typeof (Fun ("x", Pair (App (Var "x", Const 1),
			       App (Var "x", Pair (Const 1, Const 2)))));;

(* fun x -> let z = x in (z 1, z (1,2)) *)

let _ = typeof (Fun ("x", 
		    Let ("z", Var "x",
			Pair (App (Var "z", Const 1),
			     App (Var "z", Pair (Const 1, Const 2))))));;

(* let distr_pair = fun f -> (f 1, f (1,2)) in distr_pair (fun x -> x) *)

let _ = typeof (Let ("distr_pair", 
		    Fun ("f", Pair (App (Var "f", Const 1),
				   App (Var "f", Pair (Const 1, Const 2)))),
		    App (Var "distr_pair", (Fun ("x", Var "x")))));;

retour à la page du cours