Précédent Remonter Suivant

3.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 Remonter Suivant