84

Chapitre 6

D’autres extensions du langage ML et de son système de typage

Dans ce chapitre nous présentons d’autres extensions du language ML et de son système de typage. Dans une première partie, nous considérons des extensions du système de typage qui ne peuvent pas s’effectuer sans ajout de nouvelles primitives. L’extension du langage préserve le noyau ML, dans le sens où l’on retrouve simplement ML en retirant les nouvelles constructions du langage. On pourrait également parler d’extensions “horizontales”. Nous présenterons également des extensions “verticales”, où seul le système de typage est modifié, la syntaxe et la sémantique opérationelle du langage restant celles de ML, voir même du lamda-calcul.

Par exemple, l’ajout des références a nécessité des modifications importantes dans le formalisation de la sémantique, mais le système de typage est inchangé (dans la version basée sur la restriction de la liaison à des valeurs). Inversement, l’ajout d’objets enregistrements a nécessité une extension importante du système de typage, alors que leur sémantique s’écrivait très naturellement dans le formalisme existant. Nous présentons ci-dessous d’autres extensions du langage ML, nous ne les traitons pas avec le même soucis de détail que les précédentes.

6.1 Extensions horizontales

La plupart des extensions que nous avons vues jusqu’à présent rentrent dans cette catégorie. Les plus évidentes sont celles qui peuvent être traitées par simple ajout de constantes.

6.1.1 Types dynamiques

Il n’y a pas une seule bonne raison d’introduire des types dynamiques dans un langage, mais de nombreuses mauvaises raisons. Les types dynamiques sont en quelques sortes un paliatif à de nombreuses déficience du système de typage. Une valeur de type dynamique est la paire d’une valeur avec une représentation de son type ; son type statique est une nouvelle constante Dyn ne portant aucune information. La véritable information de type et la valeur d’origine peuvent être retrouvées à l’éxécution en explorant la représentation du type portée par la valeur dynamique.

La construction de valeurs de type dynamique permet, par exemple, de fabriquer des listes non homogènes, de sauver des données dans un fichier et de les relire de façon sure (puisque les donneées sont enregistrées avec leur type), de passer des arguments polymorphes à des fonctions (au prix de vérifications de types à l’exécution). Bien souvent, ces cas particuliers peuvent trouver des solutions mieux adaptées, mais toutes différentes.

Nous décrivons la forme la plus simple d’ajout de types dynamiques. Le langage est étendu avec deux constructions :

a ::= … | dynamic (a : σ) | typecase a of (x, σ) ⇒ a else a

La première permet de construire des valeurs de type dynamique. La seconde extrait la “vraie” valeur contenue dans une valeur de type dynamique pourvu que son type soit suffisamment général ; elle retourne une valeur par défaut dans le cas contraire.

La sémantique des opérations sur les dynamiques est très proche de celle des types concrets, à la différence qu’elle fait intervenir les types du langage. Les contextes d’évaluation sont étendus à :

E ::= … | dynamic (E, σ) | typecase E of (x, σ) ⇒ a else a (F V (σ) = ∅)

Dans leur formulation la plus simple, le filtrage des valeurs de type dynamique est exact, i.e. les règles de réduction sont

(typecasedynamic (v, σ) of (x, σ) ⇒ a … else a_{0}) ⟶^{ϵ} (fun (x) a) v
(typecasedynamic (v, σ) of (x, σ′) ⇒ a … else a_{0}) ⟶^{ϵ} a_{0}

Les opérations sur les dynamiques ne peuvent pas être typées comme des ajouts de primitives, car elles font intervenir des schémas de types. Les règles de typage sont :

(Dynamic)

\frac{A ⊢ a : τ  ᾱ ∉ F V (A)}{A ⊢ dynamic (a : ∀ ᾱ. τ) : Dyn}

(Typecase)

\frac{A ⊢ a : dynamic  A ⊕ (x : σ) ⊢ a_{1} : τ  A ⊢ a_{2} : τ}{A ⊢ typecase a of (x : σ) ⇒ a_{1} else a_{2} : τ}

Exercice 49 Les propriétés élémentaires du système de type de ML sont-elles conservées ?

Exercice 50 Montrer la correction du typage vis à vis de la sémantique.

En fait on peut permettre une sémantique plus souple, et

     (typecasedynamic (v, σ) of

(x, σ′) ⇒ a else a_{0}) ⟶^{ϵ} \{ \begin{matrix}(fun (x) a) v & if σ ≤ σ′ \\ a_{0} & otherwise \end{matrix}

où σ ≤ σ′ signifie que σ est plus général que σ′.

Il est aussi possible d’écrire dynamic (a) au lieu de dynamic (a : σ) ; cette liberté, utile en pratique est plus délicate à formaliser. D’une part on perd la propriété de type principal. Par exemple le programme fun (x) dynamic (x) a pour types Int → Dyn et Bool → Dyn mais pas α → Dyn car la condition de la règle Dynamic ne serait pas respectée. En pratique, on pourra par exemple échouer lorsque le programme n’admet pas de type principal. D’autre part, le type avec lequel est construite une valeur dynamique doit être fixé statiquement. Il est donc plus commode de voir cette proposition comme une synthèse de programme plutôt que comme une synthèse de types, la sémantique du langage étant définie pour les valeurs dynamiques explicitement typées.

Pour en savoir plus

Il est également possible d’étendre les schémas de types utilisés comme filtres avec des variables de motifs. On pourra consulter [?, ?] à ce sujet.

Enfin, une autre extension de ML intéressante et assez proche consiste à avoir des types dynamiques sans jamais construire de valeurs dynamiques, c’est-à-dire que les types étiquetant les valeurs dynamiques sont remplacés par des arguments supplémentaires transportant des informations de typage et ajoutés au besoin [?].

6.1.2 Types existentiels

Les types dynamiques cachent complètement le type des valeurs ; ils permettent, par exemple, de contruire des listes hétérogènes. Nous proposons ici une autre façon plus systématique qui permet aussi de caché, mais partiellement, le type d’une valeur. Il s’agit des types existentiels. A la différence des types dynamiques, les types existentiels ne permettent pas de retrouver la partie cachée par un test à l’exécution.

Un exemple fréquent consiste à “empaqueter” ensemble dans une même structure une donnée avec des fonctions permettant de manipuler celle-ci. Par exemple, une paire p_{1} ≡ (1, print int) d’un entier et d’une fonction d’impression aura le type int * (int → unit). Dans ce cas le type révèle entièrement la structure et interdit donc de mélanger p_{1} avec une autre paire p_{2} ≡ (true, print bool). Dans l’exemple ci-dessus, on aimerait ne retenir que le fait que la première composante de la paire est une valeur qui peut être passée en argument à la deuxième composante. On exprime cela en disant que ces paires ont le type ∃α.(α → Unit) ∗ α; elles peuvent maintenant être mémorisées dans une structure homogène, par exemple une liste.

Il est facile de représenter le type ∃α.((α → Unit) ∗ α) en ML. Il suffit de définir un nouveau symbol de type, par exemple pair, mais d’arité 0, c’est-à-dire que la variable de type α est implicitement quantifiée et donc cachée. Il est aussi commode d’introduire un constructeur Pair de type (α ∗ Unit) ∗ α → pair. En particulier, la création d’une valeur de type existentielle s’écrit fun (x) Pair (x).

    type pair = Pair of ('a * ('a → unit));;
    let p_{1} = Pair (print int, 1) : pair
    and p_{2} = Pair (print bool, true) : pair;;

Mais que faire de ces objets une fois créés ? Il est possible de les déplacer, de les mémoriser bien sûr, mais comment en extraire les composantes et appliquer le second argument au premier ? Comment aussi empêcher d’appliquer le premier argument de p_{1} au second argument de p_{2} ? On écrira :

    let (Pair (f,x)) = p_{1} in f x;;

Dans le corps f x de l’expression, la paire (f,x) a le type (ω → Unit ∗ ω) où ω est un nouveau constructeur de type ω, différent de tous les autres. Le résultat f x est de type Unit dans lequel u n’apparaît plus. Plus généralement, à l’ouverture d’une valeur de type dynamique ∃α.τ une nouvelle constante de type ω est introduite pour représenter la valeur inconnue de α. La règle de typage sera

\frac{A ⊢ a_{1} : pair (pair = Pair of ∃α.τ) ∈ A A ⊕ (x : τ[ω/α]) ⊢ a_{2} : τ_{2} ω ∉ τ_{2}, A}{let x = Pair a_{1} in a_{2} : τ_{2}}

Nous avons affirmé plus haut les types existentiels n’avaient pas de coût à l’exécution. En effet le constructeur Pair est le seul dans son type, et il est donc superflu, comme le constructeur ( , ) des produits.

Il est aussi possible de se passer de la déclaration des ces constructeurs, en considérant que tous les constructeurs sont prédéclarés : par exemple pair est remplacé par ( : ∃α.α ∗ (α → Unit)). En fait, il faut faire attention à ne considérer que des déclarations de la forme ( : ∃α.τ) pour des α-squelettes τ. Un α-squelette est un squelette de type τ (i.e. un type à trou) tels que α apparaît dans tous les sous-termes (différents de ). Par exemple, α∗( → ) car α n’apparait pas dans ( ∗ ), mais α∗(α → ) en est un. Le symbole pré-défini (∃α.α∗(α → )) d’arité 1 permet d’écrire Unit (∃α.α∗(α → )) au lieu de pair, ce que l’on abbrège évidemment en ∃α.α ∗ (α → Unit) avec la convention usuelle.

Les règles de typage s’écrivent :

(∃-Intro) ; \frac{A ⊢ a_{1} : τ}{A ⊢ (a_{1} : ∃α.τ)} (∃-Elim)

\frac{A ⊢ a_{1} : ∃α.τ A ⊕ (x : τ[ω/α]) ⊢ a_{2} : τ_{2} ω ∉ A, τ_{2}}{let x = (a_{1} : ∃α.τ) in a_{2} : τ_{2}}

Pour en savoir plus

Introduits dans [?], les types existentiels que nous avons décrits ici sont très simples, car ils sont entièrement déclarés. Nous avons utilisé le formalisme des types concrets pour indiquer quand et comment (avec quels types) emballer ou ouvrir une structure de donnée. Ceci permet en particulier de modifier au minimum le système de type de ML (il a quand même fallu introduire la notion de constantes inconnues). Il est difficle, d’aller plus loin dans l’intégration des types existentiels et en faire des types de première classe tout en gardant la synthèse de types. On pourra se reporter à [?] pour suivre une telle tentative, et découvrir ses limites !

Pour une preuve de correction on pourra se reporter à [?]. Dans le chapitre ?? nous verrons une autre façon de réaliser des types abstraits.

6.1.3 Types universels

Nous avons mentionné l’usage des types dynamiques pour passer des valeurs de types polymorphes comme argument des fonctions, comme l’illustre l’exemple ci-dessous.

    let self apply dx =
      typecase dx of (dx : All 'a. 'a → 'a) → x x
      else fail
    in self apply (dynamic (fun y → y : All 'a. 'a → 'a));;

Cette utilisation des valeurs de type dynamique est très inesthétique. En particulier, nous sommes obligés de prévoir un comportement anormal au cas où nous appliquons xxx a une valeur du mauvais type.

De façon analogue au types existentiels, nous écrivons :

    type id = Id of All 'a. 'a → 'a;;
    let self apply ax = let (Id x) = ax in x x
    in self apply (Id (fun x → x));;

Les types universels déclarés sont encore plus simples que les types existentiels déclarés. On pourra se reporter à [?] pour une formalisation plus précise ou [?].

6.2 Extensions verticales

Nous décrivons ici des extensions essentielles du système de typage, en général au prix de perdre la synthèse des types. Nous nous limitons au noyau de ML décrit dans le premier chapitre.

6.2.1 Et si les types étaient récursifs …

On peut étendre l’algèbre des types en remplaçant les termes de types par des expressions rationnelles. Les propriétés essentielles du langage sont conservées, en particulier, les programmes bien typés admettent des types principaux, et les programmes bien typés ne sont jamais bloqués.

Alors que dans le langage sans constante avec types récursifs, tous les termes seraient typables. C’est un peu pour cette raison que le système des types récursifs a été décrié.

Cependant, cela n’est plus vrai si le langage possède des constantes. Par exemple l’entier 1 appliqué à lui même ne peut pas être un programme bien typé car le type des entiers est incompatible avec celui des fonctions.

Le combinateur de point fixe introduit dans la section 2.3, page 27 est définissable dans cette extension de ML, car le programme

let Y F = let G f x = F (f f) x in G G

est bien typé. Donc un système de typage avec types récursifs n’a pas besoin d’une construction de récursion (ou d’un combinateur de point fixe primitif). Autoriser les types récursifs dans le langage invalide évidemment la propriété de terminaison pour les programmes bien typés. D’autres constructions comme les types récursifs déclarés, les exceptions ou bien sûr les structures mutables l’invalidaient déjà.

6.2.2 Types d’ordre supérieur

La règle Gen-Let de ML peut être remplacée par les deux règles suivantes :

(Gen) ; \frac{A ⊢ a : τ α ∉ dom (A)}{A ⊢ a : ∀ α. τ} (Let)

\frac{A ⊢ a_{1} : σ A ⊕ (x : σ) ⊢ a_{2} : τ}{A ⊢ let x = a_{1} in a_{2} : τ}

Il est maintenant possible de dériver des jugements A ⊢ a : σ mais l’ensemble des programmes typables avec chacun des deux systèmes est identique. La règle Gen signifie que si un programme possède le type τ dans un contexte A dans lequel la variable α n’apparaît pas, alors le programme possède le type polymorphe ∀ α. τ, c’est-à-dire intuitivement qu’il possède tous les types τ[τ_{0}/α].

La fonction let f = fun (x) x in f fest typable en ML, en donnant à f le type polymorphe ∀ α. α → α, mais on ne peut pas typer (fun (f) f f) (fun (x) x). La raison est qu’il faudrait donner à l’argument f dans la première expression le type de ∀ α. α → α de f, et donc typer fun (f) f f avec (∀ α. α → α) → α′ → α′. Or en dans les schémas de type de ML les variables quantifiés ne peuvent à apparaître qu’en tête des types. On dit que les types de ML sont quantifiés en tête ou que la quantification est prénexe. Le système F étend le système de typage de ML en permettant des quantificateurs en possition arbitraire.

τ ::= α | τ → τ | ∀ α. τ

Les règles de typage sont

(Fun) ; \frac{A ⊕ (x : τ_{2}) ⊢ a : τ_{1}}{A ⊢ fun (x) a : τ_{2} → τ_{1}}  (App) ; \frac{A ⊢ a_{1} : τ_{2} → τ_{1} A ⊢ a_{2} : τ_{2}}{A ⊢ a_{1} a_{2} : τ_{1}}  (Var) ; \frac{z : τ ∈ A}{A ⊢ z : τ}

(Inst) ; \frac{A ⊢ a : ∀ α. τ}{A ⊢ a : τ[t_{0}/α]}  (Gen) ; \frac{A ⊢ a : τ  α ∉ A}{A ⊢ z : ∀ α. τ}

Exercice 51 (*) Écrire une dérivation de typage de fun (x) x x dans ce système.

Nous ne ferons pas une étude détaillée du système de typage ci-dessus. Dans le système F les typages sont préservés par réduction et les seuls programmes bien typés irréductibles sont les valeurs. Le typage garantit donc la sécurité de l’évaluation. Dans le système sans constantes les programmes bien typés ne peuvent pas être réduits indéfiniment. Par contre, l’inférence de type n’est pas décidable dans le système F.

Pour cette raison, nous pouvons nous intéresser à des sous-ensembles du système F. Nous définissons les types de rangs k de la façon suivante :

\begin{matrix}τ_{0} ::= & α | τ → τ \\ τ_{k+1} ::= & τ_{k} | τ_{k} → τ_{k+1} | ∀ α. τ_{k+1} \end{matrix}

Intuitivement, le rang mesure la profondeur des flèches traversées avant d’y trouver un quantificateur. Un type de τ_{1} peut avoir des quantificateurs en tête seulement (ce sont les schémas de types de ML). Dans un type τ_{2}, un type τ_{1} (c’est-à-dire un schéma de type de ML) peut aussi apparaître à gauche d’une flèche, etc.

La synthèse de type est possible dans le système où les contextes de typages sont de rang 1 et les types sont de rang 2, mais pas au delà.

On pourra également se reporter à [?] où est présenté plus en détail cette restriction décidable.

6.2.3 Types intersection

Dans le système F, une expression qui possède le type polymorphe ∀ α. τ possède aussi, en fait, tous les types τ[τ_{0}/α]. Les types intersection permettent de donner un type, que nous notons τ_{1} ∩ τ_{2}, à une expression qui a à la fois le type τ_{1} et le type τ_{2}. Les types intersection sont de la forme :

τ ::= α | τ → τ | τ ∩ τ

Les règles de typages sont :

(Fun) ; \frac{A ⊕ (x : τ_{2}) ⊢ a : τ_{1}}{A ⊢ fun (x) a : τ_{2} → τ_{1}}  (App) ; \frac{A ⊢ a_{1} : τ_{2} → τ_{1} A ⊢ a_{2} : τ_{2}}{A ⊢ a_{1} a_{2} : τ_{1}}

(Var) ; \frac{z : ∀ ᾱ. τ_{0} ∈ A}{A ⊢ z : τ_{0}[τ̄/ᾱ]}  (∧-Elim-L) ; \frac{A ⊢ a : τ_{1} ∧ τ_{2}}{A ⊢ a : τ_{1}}  (∧-Elim-R) ; \frac{A ⊢ a : τ_{1} ∧ τ_{2}}{A ⊢ a : τ_{2}}  (∧-Intro) ; \frac{A ⊢ a : τ_{1} A ⊢ a : τ_{2}}{A ⊢ z : τ_{1} ∧ τ_{2}}

L’ensemble des programmes typables dans le système des types intersection est exactement l’ensemble des termes fortement normalisables. La synthèse de types pour ce système est donc indécidable, puisque savoir si un terme arbitraire est fortement normalisable est indécidable.

Il existe également des restrictions décidables intéressantes des types intersection. On définit le rang d’un type intersection de façon similaire au rang d’un type quantifié :

\begin{matrix}τ_{0} ::= & α | τ → τ \\ τ_{k+1} ::= & τ_{k} | τ_{k} → τ_{k+1} | ∀ α. τ_{k+1} \end{matrix}

La synthèse de type est décidable dans le système de type de rang 2 où les jugements de typage sont de rang 1 et les types de rang 2. Cette restriction décidable est détaillée dans [?].

On pourra également se reporter à [?] pour un système de type qui comporte à la fois des types quanifiés et des types intersection d’ordre arbitraire.