Précédent Index Suivant

1.7   Typage des expressions

Le typage des constantes est très simple à l'exception de la liste vide. Ces règles de typage sont toutes considérées comme des axiomes.
(ConstInt)
C |- nombre entier : Int
(ConstFloat)
C |- nombre flottant : Float
(ConstString)
C |- chaine : String
(ConstBool)
C |- booleen : Bool
(ConstUnit)
C |- () : Unit
(ConstListeVide)
C |- [] : "a.a list
Ces règles se traduisent très simplement en Caml : 

# let type_const = function
   Int _ -> Const_type Int_type
 | Float _ -> Const_type Float_type
 | String _ -> Const_type String_type
 | Bool _ ->  Const_type Bool_type
 | Unit ->  Const_type Unit_type
 | Emptylist -> List_type (new_unknown()) ;;
val type_const : ml_const -> ml_type = <fun>


On introduit deux fonctions instance qui retourne une instance de type à partir d'un schéma de types et generalize qui crée un schéma de types à partir d'un type et d'un environnement.

La fonction instance correspond à la fonction O'Caml type_instance. Elle remplace les variables de types quantifiées d'un schéma de type par de nouvelles variables de types. La fonction generalize correspond à la fonction O'Caml suivante : 

# let type_instance st =
   match st with Forall(gv,t)  ->
   let unknowns = List.map (function n -> n,new_unknown()) gv
   in
     let rec instance t  = match t with
         Var_type (vt) as tt ->
           ( match !vt with
               Unknown n ->(try List.assoc n unknowns with Not_found -> tt)
             | Instanciated ti -> instance ti
           )
       | Const_type tc  -> t
       | List_type t1 -> List_type (instance t1)
       | Fun_type (t1,t2) -> Fun_type (instance t1, instance t2)
       | Pair_type (t1,t2) -> Pair_type (instance t1, instance t2)
     in
       instance t
 ;;
val type_instance : quantified_type -> ml_type = <fun>

# let generalize_types gamma l =
   let fvg = free_vars_of_type_env gamma
   in
     List.map (function (s,t) ->
                (s, Forall(free_vars_of_type (fvg,t),t))) l
 ;;
val generalize_types :
  ('a * quantified_type) list ->
  ('b * ml_type) list -> ('b * quantified_type) list = <fun>


Elle crée un schéma de type en quantifiant les variables libres d'un type qui n'appartiennent pas aux variables libres de l'environnement.

Les règles de typages des expressions sont les règles de typage des constantes et les règles suivantes :
(Var)
x:s,C |- x : t         t=instance(s)
(Pair)
C|- e1 : t1         C|- e2 : t2
C|- (e1,e2) : t1 * t2
(List)
C|- e1 : t         C|- e2 : t list
C|- (e1 :: e2) : t list
(If)
C|- e1 : Bool         C|- e2 : t         C|- e3 : t
C|- (if e1 then e2 else e3) : t
(App)
C|- e1 : t' ® t         C|- e2 : t'
C|- (e1 e2) : t
(Abs)
x:t1,C|- e : t2
C|- (function x -> e) : t1 ® t2
(Let)
C|- e1=t1         s = generalize(t1,C)         (x:s),C|- e2:t2
C|- let x = e1 in e2 : t2
(LetRec)
(x:a),C|- e1=t1         aÏV(C)        s = generalize(t1,C)         (x:s),C|- e2:t2
C|- let x = e1 in e2 : t2
Le polymorphisme est introduit dans les règles Let et LetRec. La règle LetRec suppose que la variable définie récursivement (x) est du type a, nouvelle variable de type qui n'apparaît pas libre dans l'environnement. Ce qui ne fait aucune supposition sur le type de x, mais dans la mesure où le type de x n'est pas un schéma de type, les contraintes de type sur x dans e1 seront bien répercutées sur le type final de e1.

La fonction type_expr suivante suit les règles de typage définies ci-dessus. 

# let rec type_expr gamma =
   let rec type_rec expri = 
     match expri with
         Const c -> type_const c
       | Var s -> let t = try List.assoc s gamma
          with Not_found -> raise (Type_error(Unbound_var s))
          in  type_instance t
       | Pair (e1,e2) -> Pair_type (type_rec e1, type_rec e2) 
       | Cons (e1,e2) ->
           let t1 = type_rec e1
           and t2 = type_rec e2 in
             unify_types (List_type t1, t2); t2
       | Cond (e1,e2,e3) ->
           let t1 = unify_types (Const_type Bool_type, type_rec e1)
           and t2 = type_rec e2
           and t3 = type_rec e3 in 
             unify_types (t2,t3); t2
       | App (e1,e2) ->
           let t1 = type_rec e1
           and t2 = type_rec e2 in
             let u = new_unknown() in
               unify_types (t1, Fun_type (t2,u)); u
       | Abs(s,e) ->
           let t = new_unknown() in
             let new_env = (s,Forall ([],t))::gamma in
               Fun_type (t, type_expr new_env e)
       | Letin (s,e1,e2) -> 
           let t1 = type_rec e1 in
             let new_env = generalize_types gamma [ (s,t1) ] in
               type_expr (new_env@gamma) e2
       | Letrecin (s,e1,e2) -> 
           let u = new_unknown () in
             let new_env = (s,Forall([  ],u))::gamma in
               let t1 = type_expr (new_env@gamma) e1 in
                 let final_env = generalize_types gamma [ (s,t1) ] in
                   type_expr (final_env@gamma) e2
   in
     type_rec;;
val type_expr : (string * quantified_type) list -> ml_expr -> ml_type = <fun>


Précédent Index Suivant