TD 6 - 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.

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 tester, on pourra se servir de la fonction d'affichage suivante :

let rec pp_typ fmt = function
  | Tproduct (t1, t2) -> Format.fprintf fmt "%a *@ %a" pp_atom t1 pp_atom t2
  | Tarrow (t1, t2) -> Format.fprintf fmt "%a ->@ %a" pp_atom t1 pp_typ t2
  | (Tint | Tvar _) as t -> pp_atom fmt t
and pp_atom fmt = function
  | Tint -> Format.fprintf fmt "int"
  | Tvar v -> pp_tvar fmt v
  | Tarrow _ | Tproduct _ as t -> Format.fprintf fmt "@[<1>(%a)@]" pp_typ t
and pp_tvar fmt = function
  | { def = None; id } -> Format.fprintf fmt "'%d" id
  | { def = Some t; id } -> Format.fprintf fmt "@[<1>('%d := %a)@]" id pp_typ t

On introduit ensuite un module V encapsulant le type tvar avec une fonction de comparaison et une fonction qui crée une nouvelle variable de type.

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

Question 1. Normalisation

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).

On pourra tester avec

let () =
  let a = V.create () in
  let b = V.create () in
  let ta = Tvar a in
  let tb = Tvar b in
  assert (head ta == ta);
  assert (head tb == tb);
  let ty = Tarrow (ta, tb) in
  a.def <- Some tb;
  assert (head ta == tb);
  assert (head tb == tb);
  b.def <- Some Tint;
  assert (head ta = Tint);
  assert (head tb = Tint);
  assert (canon ta = Tint);
  assert (canon tb = Tint);
  assert (canon ty = Tarrow (Tint, Tint))

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.

On pourra tester avec

let () =
  let a = V.create () in
  let b = V.create () in
  let ta = Tvar a in
  let tb = Tvar b in
  assert (occur a ta);
  assert (occur b tb);
  assert (not (occur a tb));
  let ty = Tarrow (ta, tb) in
  assert (occur a ty);
  assert (occur b ty);
  (* unifie 'a-> 'b et int->int *)
  unify ty (Tarrow (Tint, Tint));
  assert (canon ta = Tint);
  assert (canon ty = Tarrow (Tint, Tint));
  (* unifie 'c et int->int *)
  let c = V.create () in
  let tc = Tvar c in
  unify tc ty;
  assert (canon tc = Tarrow (Tint, Tint))

let cant_unify ty1 ty2 =
  try let _ = unify ty1 ty2 in false with UnificationFailure _ -> true

let () =
  assert (cant_unify Tint (Tarrow (Tint, Tint)));
  assert (cant_unify Tint (Tproduct (Tint, Tint)));
  let a = V.create () in
  let ta = Tvar a in
  unify ta (Tarrow (Tint, Tint));
  assert (cant_unify ta Tint)

Question 3. Variables libres d'un type

Pour représenter l'ensemble des variables libres d'un type, on utilise le module Set de Caml.

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.

On pourra tester avec

let () =
  assert (Vset.is_empty (fvars (Tarrow (Tint, Tint))));
  let a = V.create () in
  let ta = Tvar a in
  let ty = Tarrow (ta, ta) in
  assert (Vset.equal (fvars ty) (Vset.singleton a));
  unify ty (Tarrow (Tint, Tint));
  assert (Vset.is_empty (fvars ty))

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. Indication : On pourra introduire un module module Vmap = Map.Make(V) et se servir d'une valeur de type tvar Vmap.t pour représenter cette substitution.

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 les opérateurs (Op), on peut se contenter de Op "+" de type int * int -> int.

Pour tester, on utilisera la fonction suivante

let typeof e = canon (w empty e)

Quelques tests positifs (l'expression et le type attendu sont indiqués en commentaire) :

(* 1 : int *)
let () = assert (typeof (Const 1) = Tint)

(* fun x -> x : 'a -> 'a *)
let () = assert (match typeof (Fun ("x", Var "x")) with
  | Tarrow (Tvar v1, Tvar v2) -> V.equal v1 v2
  | _ -> false)

(* fun x -> x+1 : int -> int *)
let () = assert (typeof (Fun ("x", App (Op "+", Pair (Var "x", Const 1))))
                 = Tarrow (Tint, Tint))

(* fun x -> x+x : int -> int *)
let () = assert (typeof (Fun ("x", App (Op "+", Pair (Var "x", Var "x"))))
                 = Tarrow (Tint, Tint))

(* let x = 1 in x+x : int *)
let () =
  assert (typeof (Let ("x", Const 1, App (Op "+", Pair (Var "x", Var "x"))))
          = Tint)

(* let id = fun x -> x in id 1 *)
let () =
  assert (typeof (Let ("id", Fun ("x", Var "x"), App (Var "id", Const 1)))
          = Tint)

(* let id = fun x -> x in id id 1 *)
let () =
  assert (typeof (Let ("id", Fun ("x", Var "x"),
		       App (App (Var "id", Var "id"), Const 1)))
          = Tint)

(* let id = fun x -> x in (id 1, id (1,2)) : int * (int * int) *)
let () =
  assert (typeof (Let ("id", Fun ("x", Var "x"),
		       Pair (App (Var "id", Const 1),
			     App (Var "id", Pair (Const 1, Const 2)))))
          = Tproduct (Tint, Tproduct (Tint, Tint)))

(* app = fun f x -> let y = f x in y : ('a -> 'b) -> 'a -> 'b *)
let () =
  let ty =
    typeof (Fun ("f", Fun ("x", Let ("y", App (Var "f", Var "x"), Var "y"))))
  in
  assert (match ty with
    | Tarrow (Tarrow (Tvar v1, Tvar v2), Tarrow (Tvar v3, Tvar v4)) ->
        V.equal v1 v3 && V.equal v2 v4
    | _ -> false)

Quelques tests négatifs :

let cant_type e =
  try let _ = typeof e in false with UnificationFailure _ -> true

(* 1 2 *)
let () = assert (cant_type (App (Const 1, Const 2)))

(* fun x -> x x *)
let () = assert (cant_type (Fun ("x", App (Var "x", Var "x"))))

(* (fun f -> +(f 1)) (fun x -> x) *)
let () = assert (cant_type
                   (App (Fun ("f", App (Op "+", App (Var "f", Const 1))),
	                 Fun ("x", Var "x"))))

(* fun x -> (x 1, x (1,2)) *)
let () = assert (cant_type
                   (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 () = assert (cant_type
                   (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 () =
  assert (cant_type
            (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"))))))

solution

retour à la page du cours