Précédent Index

2.1   Remarques sur le typage d'Objective Caml

Le typeur de mini-ML ne tenait pas compte des valeurs mutables (physiquement modifiables). Objective Caml est un langage fonctionnel muni d'effets de bord. Or ceci si le mécanisme de généralisation (des types en schémas de types) variables de types

2.1.1   Polymorphisme et valeurs mutables

Le typeur de Objective Caml utilise des variables de types faibles pour rendre sûr la manipulation de valeurs mutables. En effet si les primitives de constructions de valeurs mutables étaient traités comme des valeurs polymorphes classiques le typeur ne détecterait pas les inconsistances de types. Le programme suivant en est un exemple : 
let x = ref (fun x -> x)
in
  x:=(fun x -> x + 1);
  !x true;;
et entraîne une erreur de typage.

Une solution serait de ne construire que des valeurs mutables monomorphes. Comme cette contrainte est trop forte, il est possible de créer des valeurs mutables polymorphes spéciales, en utilisant des variables de types faibles pour celles-ci. L'idée est d'assurer lors de l'instanciation de cette variable de type, dans d'une application, que l'on obtient un type simple ou une variable de type liée au contexte de typage.

Pour cela on différencie les expressions en deux classes : les expressions non expansives incluant principalement les variables, les constructeurs et l'abstraction et les expressions expansives incluant principalement l'application. Seules les expressions expansives peuvent engendrer une exception ou étendre le domaine (incohérence de types).

2.1.2   Expressions non-expansives

Voici le texte de la fonction de reconnaissance d'expression non expansives du compilateur Objective Caml 3.0 : 

let rec is_nonexpansive exp =
  match exp.exp_desc with
    Texp_ident(_,_) -> true
  | Texp_constant _ -> true
  | Texp_let(rec_flag, pat_exp_list, body) ->
      List.for_all (fun (pat, exp) -> is_nonexpansive exp) pat_exp_list &
      is_nonexpansive body
  | Texp_apply(e, None::el) ->
      is_nonexpansive e &&
      List.for_all (function None -> true | Some exp -> is_nonexpansive e) el
  | Texp_function _ -> true
  | Texp_tuple el ->
      List.for_all is_nonexpansive el
  | Texp_construct(_, el) ->
      List.for_all is_nonexpansive el
  | Texp_variant(_, Some e) -> is_nonexpansive e
  | Texp_variant(_, None) -> true
  | Texp_record(lbl_exp_list, opt_init_exp) ->
      List.for_all
        (fun (lbl, exp) -> lbl.lbl_mut = Immutable & is_nonexpansive exp)
        lbl_exp_list &&
      (match opt_init_exp with None -> true | Some e -> is_nonexpansive e)
  | Texp_field(exp, lbl) -> is_nonexpansive exp
  | Texp_array [] -> true
  | Texp_new (_, cl_decl) when Ctype.class_type_arity cl_decl.cty_type > 0 ->
      true
  | _ -> false
;;
Les expressions suivantes sont non-expansives (donc pourront être généralisées :les constantes, les identificateurs, les n-uplet si toutes les sous-expressions le sont, les constructeurs constants, les constructeurs d'arité 1 si ce constructeur n'est pas mutable et si l'expression passée au constructeur est elle aussi non-expansive, les déclarations locales (let et let rec) si l'expression finale et toute les expressions des déclarations locales sont non-expansives, l'abstraction, la récupération d'exceptions si l'expression à calculer et toutes les expressions de partie droite du filtrage le sont, la séquence si le dernier élément de la séquence l'est, la conditionnelle si les branches then et else le sont, les expressions contraintes par un type si la sous-expression l'estm le vecteur vide, les enregistrements si tous ces champs sont non-mutables et si chaque expression associée à un champ l'est, l'accès à un champ d'un enregistrement si l'expression correspondante à l'enregistrement l'est, les filtrages de flots et les gardes si l'expression associée l'est.

Toutes les autres expressions sont expansives.
En Objective Caml on pourra généraliser (c'est-à-dire construire un schéma de type) les variables de type rencontrées dans des expressions non expansives et ne pas généraliser (variable de type faible notée _'a) celles rencontrées dans des expressions expansives.

Ces variables de type faible pourront être instanciées ultérieurement dans le typage d'un module. Il est à noter que ces variables de type faible ne peuvent sortir d'un module (sans le risque de réemplois ultérieurs incompatibles).

2.1.3   Exemples

Voici deux séries d'exemples de typage d'expressions non-expansives et d'expressions expansives :

avec effets de bord
Objective Caml 3.0 commentaires
expression non expansive  
let nref x = ref x;; abstraction
nref : 'a -> 'a ref = <fun> schéma de type
expression expansive  
let x = ref [];; ref est un constructeur mutable
x : '_a list ref = ref [] variable de type faible _a
x:=[3];; affinage du type de x
x;;  
int list ref  

sans effets de bord
Objective Caml 3.0 commentaires
let a x y = x y;; le combinateur A
('a -> 'b) -> 'a -> 'b son schéma de type
let g = a id;; une application partielle
'_a -> '_a son type non généralisé
g 3;; affinage du type de g
int = 3  
g;;  
int -> int  

2.1.4   Exercices

  1. Introduire les références dans mini-ML.
  2. Modifier le typeur de mini-ML pour tenir compte des expressions expansives.

2.1.5   Bibliographie

La thèse de Xavier Leroy [Leroy-these] décrit le typage polymorphe pour les effets de bords, les canaux de communications et les continuations dans un langage algorithmique fonctionnel.

La thèse d'Emmanuel Engel compare différents systèmes de typage polymorphe pour les effets de bords en présence de modules poru le langage Caml.
Précédent Index