Précédent Index 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())
* ;;
* 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 Caml-light 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 Caml-light suivante : let generalize_types gamma l =
* let fvg = free_vars_of_type_env gamma
* in
* map (function (s,t) ® (s, Forall(free_vars_of_type (fvg,t),t))) l
* ;;
* 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 = function
* Const c ® type_const c
* Var s ® let t = try 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
* ;;
* type_expr : (string * quantified_type) list ® ml_expr ® ml_type = áfunñ

Précédent Index Suivant