Remarques sur le typage de Caml-light 0.7

Polymorphisme et valeurs mutables
Expressions non-expansives
Exemples
Exercices
Bibliographie

3.14 Remarques sur le typage de Caml-light 0.7

Le typeur de mini-ML ne tenait pas compte des valeurs mutables (physiquement modifiables). Caml-light 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

3.14.1 Polymorphisme et valeurs mutables

Le typeur de Caml-light 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).

3.14.2 Expressions non-expansives

Voici le texte de la fonction de reconnaissance d'expression non expansives du compilateur caml-light 0.7 :

let rec is_nonexpansive expr =
  match expr.e_desc with
    Zident id -> true
  | Zconstant sc -> true
  | Ztuple el -> for_all is_nonexpansive el
  | Zconstruct0 cstr -> true
  | Zconstruct1(cstr, e) -> cstr.info.cs_mut == Notmutable 
                            & is_nonexpansive e
  | Zlet(rec_flag, bindings, body) ->
      for_all (fun (pat, expr) -> is_nonexpansive expr) bindings &
      is_nonexpansive body
  | Zfunction pat_expr_list -> true
  | Ztrywith(body, pat_expr_list) ->
      is_nonexpansive body &
      for_all (fun (pat, expr) -> is_nonexpansive expr) pat_expr_list
  | Zsequence(e1, e2) -> is_nonexpansive e2
  | Zcondition(cond, ifso, ifnot) ->
      is_nonexpansive ifso & is_nonexpansive ifnot
  | Zconstraint(e, ty) -> is_nonexpansive e
  | Zvector [] -> true
  | Zrecord lbl_expr_list ->
      for_all (fun (lbl, expr) ->
                  lbl.info.lbl_mut == Notmutable & is_nonexpansive expr)
              lbl_expr_list
  | Zrecord_access(e, lbl) -> is_nonexpansive e
  | Zparser pat_expr_list -> true
  | Zwhen(cond, act) -> is_nonexpansive act
  | _ -> 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 Caml Light 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).

3.14.3 Exemples

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

avec effets de bord

Camllight 0.7	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

Camllight 0.7	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`

3.14.4 Exercices

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

3.14.5 Bibliographie

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