TP 15 (Mines-Pont) : Inférence de type

Solution

type ('a, 'b) dict =
  | Empty
  | Node of ('a, 'b) dict * 'a * 'b * ('a, 'b) dict


let creer_dictionnaire () = Empty


let rec trouver cle = function
  | Empty -> None
  | Node (gauche, cle_noeud, valeur, droite) ->
  if cle = cle_noeud then Some valeur
  else if cle < cle_noeud then trouver cle gauche
      else trouver cle droite


let rec inserer cle valeur = function
  | Empty -> Node (Empty, cle, valeur, Empty)
  | Node (gauche, cle_noeud, valeur_noeud, droite) ->
      if cle = cle_noeud then Node (gauche, cle, valeur, droite)
      else if cle < cle_noeud then
        Node (inserer cle valeur gauche, cle_noeud, valeur_noeud, droite)
      else Node (gauche, cle_noeud, valeur_noeud, inserer cle valeur droite)


let rec map_dict f = function
  | Empty -> Empty
  | Node (gauche, cle, valeur, droite) ->
      Node (map_dict f gauche, cle, f valeur, map_dict f droite)


let rec fold_dict f dictionnaire accumulateur =
  match dictionnaire with
  | Empty -> accumulateur
  | Node (gauche, cle, valeur, droite) ->
      let accumulateur = fold_dict f gauche accumulateur in
      let accumulateur = f accumulateur cle valeur in
      fold_dict f droite accumulateur


let valeur_associee nom dictionnaire =
  match trouver nom dictionnaire with
  | Some valeur -> valeur
  | None -> failwith ("identifiant inconnu : " ^ nom)


(* Inférence avec annotation de paramètre *)

type typ1 =
  | Int
  | Arrow of typ1 * typ1
  | Product of typ1 * typ1
;;

type expression1 =
  | Var of string
  | Const of int
  | Op of string
  | Fun of string * typ1 * expression1
  | App of expression1 * expression1
  | Couple of expression1 * expression1
  | Let of string * expression1 * expression1
;;
let print_typ1 typ =
  let rec aux = function
    | Int -> print_string "int"
    | Product (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " * ";
      aux droite;
        print_string ")"
    | Arrow (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " -> ";
      aux droite;
        print_string ")"
  in
  aux typ


let print_expression1 expression =
  let rec aux = function
    | Var nom -> print_string nom
    | Const entier -> print_int entier
    | Op operateur -> print_string operateur
    | Fun (nom, typ, corps) ->
        print_string "fun ";
        print_string nom;
        print_string " : ";
        print_typ1 typ;
        print_string " -> ";
        aux corps
    | App (fonction, argument) ->
        print_string "(";
        aux fonction;
        print_string " ";
        aux argument;
        print_string ")"
    | Couple (gauche, droite) ->
        print_string "(";
        aux gauche;
        print_string ", ";
        aux droite;
        print_string ")"
    | Let (nom, valeur, corps) ->
        print_string "let ";
        print_string nom;
        print_string " = ";
        aux valeur;
        print_string " in ";
        aux corps
  in
  aux expression


let typ_expr expression =
  let rec aux environnement = function
    | Var nom -> valeur_associee nom environnement
    | Const _ -> Int
    | Op _ -> Arrow (Product (Int, Int), Int)
    | Fun (nom, typ_argument, corps) ->
        let environnement = inserer nom typ_argument environnement in
        Arrow (typ_argument, aux environnement corps)
    | App (fonction, argument) ->
        let typ_fonction = aux environnement fonction in
        let typ_argument = aux environnement argument in
        begin
          match typ_fonction with
          | Arrow (attendu, resultat) when attendu = typ_argument -> resultat
          | Arrow _ -> failwith "argument de type incorrect"
          | _ -> failwith "application d'une expression non fonctionnelle"
        end
    | Couple (gauche, droite) -> Product (aux environnement gauche, aux environnement droite)
    | Let (nom, valeur, corps) ->
        let typ_valeur = aux environnement valeur in
        aux (inserer nom typ_valeur environnement) corps
  in
  aux (creer_dictionnaire ()) expression


(* Inférence sans annotation *)

type typ2 =
  | Int
  | Arrow of typ2 * typ2
  | Product of typ2 * typ2
  | Tvar of int
;;


type expression2 =
  | Var of string
  | Const of int
  | Op of string
  | Fun of string * expression2
  | App of expression2 * expression2
  | Couple of expression2 * expression2
  | Let of string * expression2 * expression2
;;


let print_typ2 typ =
  let rec aux = function
    | Int -> print_string "int"
    | Tvar numero -> print_int numero
    | Product (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " * ";
      aux droite;
        print_string ")"
    | Arrow (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " -> ";
      aux droite;
        print_string ")"
  in
  aux typ


let print_expression2 expression =
  let rec aux = function
    | Var nom -> print_string nom
    | Const entier -> print_int entier
    | Op operateur -> print_string operateur
    | Fun (nom, corps) ->
        print_string "fun ";
        print_string nom;
        print_string " -> ";
        aux corps
    | App (fonction, argument) ->
        print_string "(";
        aux fonction;
        print_string " ";
        aux argument;
        print_string ")"
    | Couple (gauche, droite) ->
        print_string "(";
        aux gauche;
        print_string ", ";
        aux droite;
        print_string ")"
    | Let (nom, valeur, corps) ->
        print_string "let ";
        print_string nom;
        print_string " = ";
        aux valeur;
        print_string " in ";
        aux corps
  in
  aux expression


let compteur_types = ref 0


let reset_compteur_types () = compteur_types := 0


let nouvelle_variable_type () =
  let resultat = !compteur_types in
  incr compteur_types;
  resultat


let rec remplacer_variable variable remplacement = function
  | Int -> Int
  | Tvar numero when numero = variable -> remplacement
  | Tvar numero -> Tvar numero
  | Arrow (gauche, droite) ->
      Arrow (remplacer_variable variable remplacement gauche, remplacer_variable variable remplacement droite)
  | Product (gauche, droite) ->
      Product (remplacer_variable variable remplacement gauche, remplacer_variable variable remplacement droite)


let rec appliquer substitution = function
  | Int -> Int
  | Tvar numero ->
      begin
        match trouver numero substitution with
        | None -> Tvar numero
        | Some typ -> appliquer substitution typ
      end
  | Arrow (gauche, droite) -> Arrow (appliquer substitution gauche, appliquer substitution droite)
  | Product (gauche, droite) ->
      Product (appliquer substitution gauche, appliquer substitution droite)


let rec variable_libre_dans variable typ =
  match typ with
  | Int -> false
  | Tvar numero -> numero = variable
  | Arrow (gauche, droite) | Product (gauche, droite) ->
      variable_libre_dans variable gauche || variable_libre_dans variable droite


let ajouter_substitution substitution variable typ =
  let typ = appliquer substitution typ in
  let substitution = map_dict (remplacer_variable variable typ) substitution in
  inserer variable typ substitution


let rec unification substitution typ_gauche typ_droite =
  let typ_gauche = appliquer substitution typ_gauche in
  let typ_droite = appliquer substitution typ_droite in
  if typ_gauche = typ_droite then substitution
  else
    match (typ_gauche, typ_droite) with
    | Arrow (g1, d1), Arrow (g2, d2) ->
        let substitution = unification substitution g1 g2 in
        unification substitution d1 d2
    | Product (g1, d1), Product (g2, d2) ->
        let substitution = unification substitution g1 g2 in
        unification substitution d1 d2
    | Tvar variable, typ | typ, Tvar variable ->
        if variable_libre_dans variable typ then failwith "types non unifiables"
        else ajouter_substitution substitution variable typ
    | _ -> failwith "types non unifiables"


let w_sans_polymorphisme expression =
  let rec inferer environnement substitution = function
    | Var nom -> (substitution, appliquer substitution (valeur_associee nom environnement))
    | Const _ -> (substitution, Int)
    | Op _ -> (substitution, Arrow (Product (Int, Int), Int))
    | Fun (nom, corps) ->
        let variable = Tvar (nouvelle_variable_type ()) in
        let environnement = inserer nom variable environnement in
        let substitution, typ_corps = inferer environnement substitution corps in
        (substitution, Arrow (appliquer substitution variable, typ_corps))
    | App (fonction, argument) ->
        let substitution, typ_fonction = inferer environnement substitution fonction in
        let substitution, typ_argument = inferer environnement substitution argument in
        let resultat = Tvar (nouvelle_variable_type ()) in
        let substitution = unification substitution typ_fonction (Arrow (typ_argument, resultat)) in
        (substitution, appliquer substitution resultat)
    | Couple (gauche, droite) ->
        let substitution, typ_gauche = inferer environnement substitution gauche in
        let substitution, typ_droite = inferer environnement substitution droite in
        (substitution, Product (appliquer substitution typ_gauche, appliquer substitution typ_droite))
    | Let _ -> failwith "les expressions Let ne sont pas traitées dans cette version"
  in
  reset_compteur_types ();
  let _, typ = inferer (creer_dictionnaire ()) (creer_dictionnaire ()) expression in
  typ


(* Inférence avec polymorphisme *)

type schema = Schema of int list * typ2


let ajouter_unique element liste =
  if List.mem element liste then liste else element :: liste


let union liste1 liste2 = List.fold_left (fun acc element -> ajouter_unique element acc) liste2 liste1


let difference liste1 liste2 = List.filter (fun element -> not (List.mem element liste2)) liste1


let rec variables_libres_type = function
  | Int -> []
  | Tvar numero -> [ numero ]
  | Arrow (gauche, droite) | Product (gauche, droite) ->
      union (variables_libres_type gauche) (variables_libres_type droite)


let variables_libres_schema (Schema (variables_quantifiees, typ)) =
  difference (variables_libres_type typ) variables_quantifiees


let variables_libres_env environnement =
  fold_dict
    (fun acc _ schema -> union acc (variables_libres_schema schema))
    environnement []


let rec appliquer_bloquees bloquees substitution = function
  | Int -> Int
  | Tvar numero when List.mem numero bloquees -> Tvar numero
  | Tvar numero ->
      begin
        match trouver numero substitution with
        | None -> Tvar numero
        | Some typ -> appliquer_bloquees bloquees substitution typ
      end
  | Arrow (gauche, droite) ->
      Arrow (appliquer_bloquees bloquees substitution gauche, appliquer_bloquees bloquees substitution droite)
  | Product (gauche, droite) ->
      Product (appliquer_bloquees bloquees substitution gauche, appliquer_bloquees bloquees substitution droite)


let appliquer_schema substitution (Schema (variables_quantifiees, typ)) =
  Schema (variables_quantifiees, appliquer_bloquees variables_quantifiees substitution typ)


let appliquer_env substitution environnement = map_dict (appliquer_schema substitution) environnement


let generaliser environnement typ =
  let variables = difference (variables_libres_type typ) (variables_libres_env environnement) in
  Schema (variables, typ)


let instancier (Schema (variables, typ)) =
  let substitution =
    List.fold_left
      (fun acc variable -> inserer variable (Tvar (nouvelle_variable_type ())) acc)
      (creer_dictionnaire ()) variables
  in
  appliquer substitution typ


let w expression =
  let rec inferer environnement substitution = function
    | Var nom ->
        let schema = valeur_associee nom environnement in
        (substitution, instancier (appliquer_schema substitution schema))
    | Const _ -> (substitution, Int)
    | Op _ -> (substitution, Arrow (Product (Int, Int), Int))
    | Fun (nom, corps) ->
        let variable = Tvar (nouvelle_variable_type ()) in
        let environnement = inserer nom (Schema ([], variable)) environnement in
        let substitution, typ_corps = inferer environnement substitution corps in
        (substitution, Arrow (appliquer substitution variable, typ_corps))
    | App (fonction, argument) ->
        let substitution, typ_fonction = inferer environnement substitution fonction in
        let environnement = appliquer_env substitution environnement in
        let substitution, typ_argument = inferer environnement substitution argument in
        let resultat = Tvar (nouvelle_variable_type ()) in
        let substitution = unification substitution typ_fonction (Arrow (typ_argument, resultat)) in
        (substitution, appliquer substitution resultat)
    | Couple (gauche, droite) ->
        let substitution, typ_gauche = inferer environnement substitution gauche in
        let environnement = appliquer_env substitution environnement in
        let substitution, typ_droite = inferer environnement substitution droite in
        (substitution, Product (appliquer substitution typ_gauche, appliquer substitution typ_droite))
    | Let (nom, valeur, corps) ->
        let substitution, typ_valeur = inferer environnement substitution valeur in
        let environnement = appliquer_env substitution environnement in
        let schema = generaliser environnement (appliquer substitution typ_valeur) in
        inferer (inserer nom schema environnement) substitution corps
  in
  reset_compteur_types ();
  let _, typ = inferer (creer_dictionnaire ()) (creer_dictionnaire ()) expression in
  typ

Dans ce TP, on implémente progressivement un inféreur de types pour un mini-langage fonctionnel à la OCaml.

• Sujet PDF
• Fichier de départ

Déduction naturelle

1. Donner sur papier une dérivation en déduction naturelle du séquent

$$\vdash ((a \to b) \land (b \to c)) \to (a \lor b) \to c$$

Correction

Avec $\Gamma = \{(a \to b) \land (b \to c),\ a \lor b\}$.

Dictionnaire persistant

2. Implémenter une structure persistante de dictionnaire à l'aide d'arbres binaires de recherche dans un type ('a, 'b) dict.

Seules trois opérations sont nécessaires dans la suite :

• créer un dictionnaire vide ;
• récupérer la valeur associée à une clé ;
• insérer une paire clé-valeur.

Correction

type ('a, 'b) dict =
  | Empty
  | Node of ('a, 'b) dict * 'a * 'b * ('a, 'b) dict

let creer_dictionnaire () = Empty

let rec trouver cle = function
  | Empty -> None
  | Node (gauche, cle_noeud, valeur, droite) ->
      let comparaison = Stdlib.compare cle cle_noeud in
      if comparaison = 0 then Some valeur
      else if comparaison < 0 then trouver cle gauche
      else trouver cle droite

let rec inserer cle valeur = function
  | Empty -> Node (Empty, cle, valeur, Empty)
  | Node (gauche, cle_noeud, valeur_noeud, droite) ->
      let comparaison = Stdlib.compare cle cle_noeud in
      if comparaison = 0 then Node (gauche, cle, valeur, droite)
      else if comparaison < 0 then
        Node (inserer cle valeur gauche, cle_noeud, valeur_noeud, droite)
      else
        Node (gauche, cle_noeud, valeur_noeud, inserer cle valeur droite)

Les opérations trouver et inserer sont en $O(h)$ où $h$ est la hauteur de l'arbre, donc en $O(n)$ au pire sans équilibrage.

Inférence avec annotation des paramètres

On considère d'abord le langage et les types suivants.

type typ1 =
  | Int
  | Arrow of typ1 * typ1
  | Product of typ1 * typ1

type expression1 =
  | Var of string
  | Const of int
  | Op of string
  | Fun of string * typ1 * expression1
  | App of expression1 * expression1
  | Couple of expression1 * expression1
  | Let of string * expression1 * expression1

On suppose que tous les opérateurs Op ont le type (int * int) -> int.

3. Déterminer le type de l'expression suivante :

Let ("f",
Fun ("x", Int, App (Op "+", Couple (Var "x", Const 1))),
App (Var "f", Const 2))

Correction

fun (x : int) -> + (x, 1) est de type int -> int. On applique ensuite f à 2, donc l'expression entière a le type int.

4. En donner une dérivation dans le système de typage fourni.

Correction

5. Écrire print_typ1 : typ1 -> unit et print_expression1 : expression1 -> unit.

Correction

let print_typ1 typ =
  let rec aux = function
    | Int -> print_string "int"
    | Product (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " * ";
      aux droite;
        print_string ")"
    | Arrow (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " -> ";
      aux droite;
        print_string ")"
  in
  aux typ

let print_expression1 expression =
  let rec aux = function
    | Var nom -> print_string nom
    | Const entier -> print_int entier
    | Op operateur -> print_string operateur
    | Fun (nom, typ, corps) ->
        print_string "fun ";
        print_string nom;
        print_string " : ";
        print_typ1 typ;
        print_string " -> ";
        aux corps
    | App (fonction, argument) ->
        print_string "(";
        aux fonction;
        print_string " ";
        aux argument;
        print_string ")"
    | Couple (gauche, droite) ->
        print_string "(";
        aux gauche;
        print_string ", ";
        aux droite;
        print_string ")"
    | Let (nom, valeur, corps) ->
        print_string "let ";
        print_string nom;
        print_string " = ";
        aux valeur;
        print_string " in ";
        aux corps
  in
  aux expression

6. Écrire typ_expr : expression1 -> typ1, qui lève une erreur si l'expression n'est pas typable.

Correction

let typ_expr expression =
  let rec aux environnement = function
    | Var nom -> valeur_associee nom environnement
    | Const _ -> Int
    | Op _ -> Arrow (Product (Int, Int), Int)
    | Fun (nom, typ_argument, corps) ->
        let environnement = inserer nom typ_argument environnement in
        Arrow (typ_argument, aux environnement corps)
    | App (fonction, argument) ->
        let typ_fonction = aux environnement fonction in
        let typ_argument = aux environnement argument in
        begin
          match typ_fonction with
          | Arrow (attendu, resultat) when attendu = typ_argument -> resultat
          | Arrow _ -> failwith "argument de type incorrect"
          | _ -> failwith "application d'une expression non fonctionnelle"
        end
    | Couple (gauche, droite) -> Product (aux environnement gauche, aux environnement droite)
    | Let (nom, valeur, corps) ->
        let typ_valeur = aux environnement valeur in
        aux (inserer nom typ_valeur environnement) corps
  in
  aux (creer_dictionnaire ()) expression

Inférence sans annotation

On retire ensuite les annotations de type des paramètres et on introduit des variables de type.

type typ2 =
  | Int
  | Arrow of typ2 * typ2
  | Product of typ2 * typ2
  | Tvar of int

type expression2 =
  | Var of string
  | Const of int
  | Op of string
  | Fun of string * expression2
  | App of expression2 * expression2
  | Couple of expression2 * expression2
  | Let of string * expression2 * expression2

Dans toute cette partie, on ne considère que des expressions sans Let.

7. Écrire print_typ2 et print_expression2.

Correction

Le principe est identique à la question 5, avec un cas supplémentaire pour Tvar.

let print_typ2 typ =
  let rec aux = function
    | Int -> print_string "int"
    | Tvar numero -> print_int numero
    | Product (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " * ";
      aux droite;
        print_string ")"
    | Arrow (gauche, droite) ->
        print_string "(";
      aux gauche;
        print_string " -> ";
      aux droite;
        print_string ")"
  in
  aux typ

let print_expression2 expression =
  let rec aux = function
    | Var nom -> print_string nom
    | Const entier -> print_int entier
    | Op operateur -> print_string operateur
    | Fun (nom, corps) ->
        print_string "fun ";
        print_string nom;
        print_string " -> ";
        aux corps
    | App (fonction, argument) ->
        print_string "(";
        aux fonction;
        print_string " ";
        aux argument;
        print_string ")"
    | Couple (gauche, droite) ->
        print_string "(";
        aux gauche;
        print_string ", ";
        aux droite;
        print_string ")"
    | Let (nom, valeur, corps) ->
        print_string "let ";
        print_string nom;
        print_string " = ";
        aux valeur;
        print_string " in ";
        aux corps
  in
  aux expression

8. Donner une dérivation du jugement de type

$$\vdash \texttt{fun f -> fun g -> fun x -> f (g x)} : (1 \to 2) \to (0 \to 1) \to 0 \to 2$$

Correction

Dans l'environnement

$$f : 1 \to 2,\ g : 0 \to 1,\ x : 0$$

on obtient successivement :

• x : 0 ;
• g x : 1 ;
• f (g x) : 2.

En réintroduisant ensuite les trois abstractions, on déduit

$$(1 \to 2) \to (0 \to 1) \to 0 \to 2$$

9. Écrire appliquer : (int, typ2) dict -> typ2 -> typ2.

Correction

let rec appliquer substitution = function
  | Int -> Int
  | Tvar numero ->
      begin
        match trouver numero substitution with
        | None -> Tvar numero
        | Some typ -> appliquer substitution typ
      end
  | Arrow (gauche, droite) -> Arrow (appliquer substitution gauche, appliquer substitution droite)
  | Product (gauche, droite) -> Product (appliquer substitution gauche, appliquer substitution droite)

10. Écrire unification : (int, typ2) dict -> typ2 -> typ2 -> (int, typ2) dict.

Correction

let rec unification substitution typ_gauche typ_droite =
  let typ_gauche = appliquer substitution typ_gauche in
  let typ_droite = appliquer substitution typ_droite in
  if typ_gauche = typ_droite then substitution
  else
    match (typ_gauche, typ_droite) with
    | Arrow (g1, d1), Arrow (g2, d2) ->
        let substitution = unification substitution g1 g2 in
        unification substitution d1 d2
    | Product (g1, d1), Product (g2, d2) ->
        let substitution = unification substitution g1 g2 in
        unification substitution d1 d2
    | Tvar variable, typ | typ, Tvar variable ->
        if variable_libre_dans variable typ then failwith "types non unifiables"
        else ajouter_substitution substitution variable typ
    | _ -> failwith "types non unifiables"

Le test d'occurrence empêche de fabriquer un type infini.

11. Écrire une première version de w : expression2 -> typ2 pour les expressions sans Let.

Correction

Dans le corrigé complet, cette première version est nommée w_sans_polymorphisme pour laisser w à la version finale.

let w_sans_polymorphisme expression =
  let rec inferer environnement substitution = function
    | Var nom -> (substitution, appliquer substitution (valeur_associee nom environnement))
    | Const _ -> (substitution, Int)
    | Op _ -> (substitution, Arrow (Product (Int, Int), Int))
    | Fun (nom, corps) ->
        let variable = Tvar (nouvelle_variable_type ()) in
        let environnement = inserer nom variable environnement in
        let substitution, typ_corps = inferer environnement substitution corps in
        (substitution, Arrow (appliquer substitution variable, typ_corps))
    | App (fonction, argument) ->
        let substitution, typ_fonction = inferer environnement substitution fonction in
        let substitution, typ_argument = inferer environnement substitution argument in
        let resultat = Tvar (nouvelle_variable_type ()) in
        let substitution = unification substitution typ_fonction (Arrow (typ_argument, resultat)) in
        (substitution, appliquer substitution resultat)
    | Couple (gauche, droite) ->
        let substitution, typ_gauche = inferer environnement substitution gauche in
        let substitution, typ_droite = inferer environnement substitution droite in
        (substitution, Product (appliquer substitution typ_gauche, appliquer substitution typ_droite))
    | Let _ -> failwith "les expressions Let ne sont pas traitées dans cette version"
  in
  reset_compteur_types ();
  let _, typ = inferer (creer_dictionnaire ()) (creer_dictionnaire ()) expression in
  typ

Inférence avec polymorphisme

Pour typer correctement les constructions let, on généralise le type obtenu pour la variable introduite.

Le système de typage utilise des schémas de types de la forme

$$\forall a_1 \dots a_n, t$$

et la généralisation

$$\mathrm{Gen}(t, \Gamma)$$

qui quantifie les variables libres de $t$ qui ne sont pas libres dans l'environnement $\Gamma$.

12. Donner une dérivation du jugement

$$\texttt{let f = fun x -> x in (f 1, f (1, 1))} : int \ast (int \ast int)$$

Correction

On commence par typer fun x -> x avec le type le plus général a -> a. Comme a n'est pas libre dans l'environnement, on généralise en

$$\forall a, a \to a$$

Puis on instancie indépendamment f à chaque occurrence.

• pour f 1, on prend f : int -> int, donc f 1 : int ;
• pour f (1, 1), on prend f : (int \ast int) -> (int \ast int), donc f (1, 1) : int \ast int.

On conclut donc

$$exttt{let f = fun x -> x in (f 1, f (1, 1))} : int \ast (int \ast int)$$

13. Écrire une nouvelle version de w implémentant l'algorithme W polymorphe.

Correction

On introduit d'abord des schémas de types, puis generaliser et instancier.

type schema = Schema of int list * typ2

let generaliser environnement typ =
  let variables = difference (variables_libres_type typ) (variables_libres_env environnement) in
  Schema (variables, typ)

let instancier (Schema (variables, typ)) =
  let substitution =
    List.fold_left
      (fun acc variable -> inserer variable (Tvar (nouvelle_variable_type ())) acc)
      (creer_dictionnaire ()) variables
  in
  appliquer substitution typ

La version finale de w est alors :

let w expression =
  let rec inferer environnement substitution = function
    | Var nom ->
        let schema = valeur_associee nom environnement in
        (substitution, instancier (appliquer_schema substitution schema))
    | Const _ -> (substitution, Int)
    | Op _ -> (substitution, Arrow (Product (Int, Int), Int))
    | Fun (nom, corps) ->
        let variable = Tvar (nouvelle_variable_type ()) in
        let environnement = inserer nom (Schema ([], variable)) environnement in
        let substitution, typ_corps = inferer environnement substitution corps in
        (substitution, Arrow (appliquer substitution variable, typ_corps))
    | App (fonction, argument) ->
        let substitution, typ_fonction = inferer environnement substitution fonction in
        let environnement = appliquer_env substitution environnement in
        let substitution, typ_argument = inferer environnement substitution argument in
        let resultat = Tvar (nouvelle_variable_type ()) in
        let substitution = unification substitution typ_fonction (Arrow (typ_argument, resultat)) in
        (substitution, appliquer substitution resultat)
    | Couple (gauche, droite) ->
        let substitution, typ_gauche = inferer environnement substitution gauche in
        let environnement = appliquer_env substitution environnement in
        let substitution, typ_droite = inferer environnement substitution droite in
        (substitution, Product (appliquer substitution typ_gauche, appliquer substitution typ_droite))
    | Let (nom, valeur, corps) ->
        let substitution, typ_valeur = inferer environnement substitution valeur in
        let environnement = appliquer_env substitution environnement in
        let schema = generaliser environnement (appliquer substitution typ_valeur) in
        inferer (inserer nom schema environnement) substitution corps
  in
  reset_compteur_types ();
  let _, typ = inferer (creer_dictionnaire ()) (creer_dictionnaire ()) expression in
  typ

Résumé du corrigé :

• une implémentation persistante de dictionnaire ;
• le typage avec annotations ;
• l'application d'une substitution et l'unification ;

• une version sans Let ;

• la version polymorphe finale de l'algorithme W.