58

Chapitre 5

Typage avec contraintes

Dans ce chapitre, nous présentons une extension du système de typage avec des contraintes d’inclusion. Nous introduisons d’abord intuitivement puis formellement la notion de sous-typage qui nous mènera vers les types contraints. Ensuite nous présentons un système de typage avec contraintes d’inclusion et nous montrons qu’il garantit la sécurité du calcul. Nous utilisons comme exemple un langage avec enregistrements flexibles, mais le formalisme est plus général ; il s’applique à des enregistrements extensibles ainsi qu’à l’inclusion sur les types de base, les types des variantes, et bien sûr les types des objets.

La formalisation du typage avec contraintes telle qu’elle est présentée ici est très récente, et de nombreux aspects, notamment la simplification des contraintes, sont encore du domaine de la recherche.

Introduction

Les types enregistrements présentés dans le chapitre précédent ont permis de typer les opérations sur les enregistrements, notamment l’accès, de façon polymorphe. C’est-à-dire que la lecture d’un champ peut être effectuée par une même fonction, indépendemment des autres champs présents. Si l’on oublie l’extension des enregistrements, la seule opération possible sur les enregistrements est la lecture des champs. Un enregistrement peut être utilisé de façon sûr là où un enregistrement avec moins de champ peut l’être. Cela revient à donner à un enregistrement le type d’un enregistrement ayant moins de champs. Cette possibilité est souvent souhaitable, par exemple pour mémoriser dans une structure homogène telle que les listes des enregistrements ayant des domaines différents mais partageant tous une partie commune que l’on doit laisser visible.

Par exemple, l’enregistrement a_{xy} ≡ {x = 1; y = 2} représentant un point dans le plan a pour type τ_{xy} ≡ {x : Pre Int; y : Pre Int; ∅}. Il définit implicitement un point a_{x} ≡ {x = 1} sur le premier axe de coordonnées qui a pour type τ_{x} ≡ {x : PreInt; ∅}. Clairement, il existe une fonction de coercion (ici une projection) qui transforme a_{xy} en a_{x}. Mais il est souvent plus intéressant de considérer que a_{xy} a lui-même le type τ_{x} et peut être utilisé partout où a_{x} le peut. Cela revient à supposer que la fonction de coercion est l’identité, en particulier elle ne change pas la valeur mais simplement le type de son argument. On dira alors que a_{xy} de type τ_{xy} a aussi le type τ_{x} parce que τ_{x} est un sous-type de τ.

La notion de sous-typage la plus simple est celle définie entre des types atomiques, comme par exemple dans le langage C, où le type des caractères est un sous-type du type des entiers, qui est lui même un sous-type du type des nombres réels. Souvent, ce genre de sous-typage n’est utilisé que pour permettre la surcharge des primitives arithmétiques et éviter ainsi à l’utilisateur de préciser complètement les opérations qu’il utilise ; il n’est alors pas essentiel. Dans la suite de ce chapitre, nous ne considérerons que le sous-typage sur les enregistrements. Il est plus utile, notamment pour son application aux objets, mais aussi plus général, et ce choix ne restreint pas l’étude du sous-typage : il sera toujours possible d’appliquer les résultats au sous-typage entre types atomiques, par exemple ceux des nombres.

Il est possible mais plus difficile de paramétrer entièrement la définition du langage par des constantes et des δ-règles comme nous l’avons fait pour ML. Pour rendre l’exposition plus simple, nous limitons notre langage à une extension de ML avec des enregistrements flexibles. Toutefois nous nous efforcerons de traiter le problème de la façon la plus générale possible, afin de pouvoir facilement transférer les résultats à d’autres constructions.

Nous reprenons donc le langage étudié dans le chapitre précédent mais en retirant la primitive d’extension des enregistrements. La syntaxe du langage est :

a ::= x | c | fun (x) a | a a | let x = a in a
c ::= {ℓ_{1} = , … ℓ_{n} = } | .ℓ

Les constantes {ℓ_{i} = ^{i∈1..n}} sont des constructeurs et les constantes ( .ℓ) sont des primitives. Les valeurs sont donc les fonctions et les valeurs enregistrements partiellement appliquées.

v ::= fun (x) a | {ℓ_{i} = v_{i}^{i∈1..n}, ℓ_{j} = ^{J∈1..k}}

La sémantique du langage est bien sûr inchangée. Les contextes d’évaluation sont donc, comme dans le chapitre 2 :

E ::= [] | E a | v E | let x = E in a

(Dans le cas d’ajout de références, la construction Let ne pourrait plus lier que des valeurs et la dernière forme du contexte d’évaluation serait donc supprimée). La relation de réduction est définie par la règle (β) et la famille de δ-règles :

{ℓ_{i} = a_{i}^{i∈1..n}}.ℓ_{j} ⟶^{ϵ} a_{j}  j ∈ 1..n

Nous utiliserons les types enregistrements du chapitre précédent, mais pour simplifier nous retirons les variables de rangée. Ainsi la seule expression de rangée possible est \underline{∅}, et nous pouvons noter \{ℓ_{i} : τ_{i}^{i∈1..n}\} au lieu de \{ℓ_{i} : τ_{i}^{i∈1..n}, \underline{∅}\}. Plus précisément, les expressions de types sont :

τ ::= α | τ → τ | {ℓ : τ^{i∈1..n}} | ∅ | Pre τ

Les types enregistrements sont considérés modulo permutation des champs et modulo la famille d’équations

{ℓ_{i} : τ_{i}^{i∈1..n}} = {ℓ_{i} : τ^{i∈1..n}; ℓ : ∅}  ∀ℓ ∉ {ℓ_{i}^{i∈1..n}}

qui exprime l’extraction de champs.

Dans la section ??, nous étendons le système de type de ML avec une règle de soustypage. En particulier, nous définissons une relation de sous-typage entre les types de ML. Cependant, nous montrons que cette approche pose des problèmes difficiles pour la synthèse de type. Aussi, nous présenterons dans la section 5.3 un système de typage avec contraintes d’inclusion, mieux adapté à la synthèse de type. En fait nous déduirons informellement le système avec contraintes de la relation de sous-typage introduite précédemment. Toutefois les deux formalismes ne sont pas équivalents. Par la suite, nous ne considérons plus que le formalisme des types contraints. Nous montrons dans la section 5.4 que le système de typage avec contraintes est correct vis à vis de l’évaluation.

Le typage avec contraintes est un formalisme très simple et assez général permettant d’étendre la synthèse de type en présence de sous-typage, tout en conservant les aspects essentiels du système de typage de ML. Par certains aspect, le typage avec contraintes est même plus simple que le typage de ML, du moins tant que l’on ne s’intéresse qu’à la sûreté apportée par le typage, en ignorant l’aspect de documentation qui nécessite une simplification des contraintes. Nous discuterons de ces problèmes à la fin de ce chapitre.

5.1 Sous-typage sur les types sans-variables

Pour simplifier nous considérons d’abord le sous-typage pour les expressions de type sans variables.

Pour être suffisemment général (la raison apparaîtra ci-dessous), nous ajoutons aux types deux constantes ⊥ et ⊤ avec l’idée intuitive que tout type est un sous-type de ⊤ et inversemenet ⊥ est un sous-type de tout type.

Définition 1 Nous définissons une relation de sous-typage sur les types sans variables, notée τ <: τ′, comme la plus petite relation réflexive et transitive satisfaisant les règles suivantes :

(<:-Bottom) ; \overline{⊥ <: τ} (<:-Top) ; \overline{τ <: ⊤} (<:-Abs) ; \overline{Pre τ <: ∅} (<:-Pre)

\frac{τ <: τ′}{Pre τ <: Pre τ′}

(<:-Record) ; \frac{τ_{i} <: τ′_{i} ∀i ∈ 1..n}{\{ℓ_{i} : τ_{i}^{i∈1..n}\} <: \{ℓ_{i} : τ′_{i}^{i∈1..n}\}}  (<:-Arrow) ; \frac{τ′_{1} <: τ_{1} τ_{2} <: τ′_{2}}{τ_{1} → τ_{2} <: τ′_{1} → τ′_{2}}

Remarquons d’abord que les règles <:-Abs et <:-Record permettent de déduire que τ_{xy} est un sous type de τ_{x} et plus généralement, {ℓ_{i} : Pre τ_{i}^{i∈1..n+k}} <: {ℓ_{i} : Pre τ_{i}^{i∈1..n}}, en utilisant l’absorption des champs absents. La règle <:-Pre permet également le sous-typage en profondeur ; par exemple, on peut déduire de la relation τ_{xy} <: τ_{x} que {z : Pre τ_{xy}} <: {z : Pre τ_{x}}. Dans la règle <:-Record chaque type doit être écrit avec les mêmes champs explicites, mais par l’équation d’extraction sur les types enregistrements, ce n’est donc pas une véritable restriction. Elle indique (comme la règle <:-Pre d’ailleurs) que le sous-typage se propage au travers de la structure, et ceci de façon covariante, i.e. le sens des inclusions entre deux types de même structure est le même que le sens des inclusions entre les sous-termes immédiats de même position. Ce n’est plus vrai pour les types fonctionnels, puisqu’une fonction de type τ_{1} → τ_{2} peut aussi être considérée comme une fonction de type τ′_{1} → τ′_{2} si τ_{2} <: τ′_{2} mais τ′_{1} <: τ_{1}. On dit que la flèche est covariante à droite et contra-variante à gauche. Cela s’explique par la dissymétrie dans l’application entre les entrées (arguments) et la sortie (le résultat). Nous avons vu par exemple que la fonction d’extraction du champ x exige seulement que son argument soit un enregistrement possédant le champ x. Elle accepte a_{x} de type τ_{x} comme argument, et plus généralement tout enregistrement possédant plus de champs, donc tel que τ_{xy} <: τ_{x}; On a donc bien τ_{x} → τ <: τ_{xy} → τ pour τ_{xy} <: τ_{x}.

Exercice 37 (*) Supposons que l’on ajoute au système de typage la règle suivante (ce que nous ferons ci-dessous) :

(Sub) ; \frac{A ⊢ a : τ τ <: τ′}{A ⊢ a : τ′}

Étant donné quatre types τ_{1}, τ_{2}, τ′_{1} et τ′_{2} tels que τ′_{1} <: τ_{1} et τ_{2} <: τ′_{2}. montrer que l’application égale à la fonction fun (f x) f x possède le type (τ_{1} → τ_{2}) → τ′_{1} → τ′_{2} sans utiliser le sous-typage sur des types flèche. En quoi cela peut-il servir à justifier la relation de sous-typage de la flèche.

La définition ci-dessus peut également s’appliquer aux termes avec variables ; toutefois, les seules relations possibles avec les variables sont ⊥ <: α, α <: α ou α <: ⊤.

Exercice 38 (*) Quels types peut-on donner à la fonction fun (x) {ℓ = x}? Admetelle un type principal (le plus général) ?

Exercice 39 On se pose la même question d’abord avec la fonction fun (f) fun (x) f x puis avec la fonction fun (f) fun (g) fun (x) (f (g x), g (f x)). En quoi le second exemple est pire ?

L’exercice ci-dessus montre que pour typer les fonctions polymorphes, on peut être amené à supposer que les variables de types sont dans une relation de sous-typage.

Les axiomes ci-dessus ne permettent à deux variables d’être dans une relation de sous-typage que si elles sont identiques. Ceci n’est pas suffisant pour typer les fonctions polymorphes. Il est ainsi nécessaire d’abstraire la relation de sous-typage par rapport à des hypothèses sur certaines variables.

5.2 Contraintes avec variables

Nous considérons maintenant des types avec variables. On aimerait définir un jugement de la forme C ⊢ τ_{1} <: τ_{2} où C est un ensemble d’hypothèses, i.e. de paires de types notées également τ_{1} <: τ_{2}. Il faut lire “sous les hypothèses C, τ_{1} est un sous-type de τ_{2}”. Pour cela, nous remplaçons la relation <: par un jugement de typage C ⊢ τ_{1} <: τ_{2}.

Définition 2 Nous définissons le jugement de typage C ⊢ τ_{1} <: τ_{2} comme la plus petite relation satisfaisant les règles suivantes (nous devons maintenant inclure les règles correspondant à la transitivité, car la relation n’est plus binaire) :

(<:-Context) ; \frac{τ_{1} <: τ_{2} ∈ C}{C ⊢ τ_{1} <: τ_{2}}  (<:-Reflex) ; \overline{C ⊢ τ <: τ}  (<:-Trans) ; \frac{C ⊢ τ_{1} <: τ_{2} C ⊢ τ_{2} <: τ_{3}}{C ⊢ τ_{1} <: τ_{3}}  (<:-Top) ; \overline{C ⊢ τ <: ⊤}

(<:-Bottom) ; \overline{C ⊢ ⊥ <: τ} (<:-Abs) ; \overline{C ⊢ Pre τ <: ∅} (<:-Pre)

\frac{C ⊢ τ <: τ′}{C ⊢ Pre τ <: Pre τ′}

(<:-Record) ; \frac{C ⊢ τ_{i} <: τ′_{i} ∀i ∈ 1..n}{C ⊢ \{ℓ_{i} : τ_{i}^{i∈1..n}\} <: \{ℓ_{i} : τ′_{i}^{i∈1..n}\}}  (<:-Arrow) ; \frac{C ⊢ τ′_{1} <: τ_{1} τ_{2} <: τ′_{2}}{C ⊢ τ_{1} → τ_{2} <: τ′_{1} → τ′_{2}}

Nous pouvons en déduire également une relation ⊢ entre ensembles de contraintes, i.e. C_{1} ⊢ C_{2} si pour toute contrainte c de C_{2}, on a C_{1} ⊢ c. Nous notons ⊢ C_{2} lorsque C_{1} est l’ensemble vide. Nous retrouvons en particulier la définition précedente maintenant notée ⊢ τ_{1} <: τ_{2}.

Proposition 11 (Substitutivité) Si C_{1} ⊢ C_{2}, alors θ(C_{1}) ⊢ θ(C_{2}) pour toute substitution θ.

\underline{Preuve} : Il suffit de voir que c’est vrai pour chaque jugement de sous-typage.

Proposition 12 (Transitivité) Si C_{1} ⊢ C_{2} et C_{2} ⊢ C_{3} alors C_{1} ⊢ C_{3}.

\underline{Preuve} : Il suffit de remplacer l’utilisation des hypothèses de c_{2} de C_{2} dans la dérivation de C_{2} ⊢ C_{3} par leur dérivation dans C_{1} ⊢ c_{2}.

Exercice 40 Vérifier que que l’on ne changerait pas le sens de la relation ⊢ en limitant la règle <:-Reflex au cas où τ est un atome, c’est-à-dire une variable ou un des symboles {∅, ⊥, ⊤} (les deux derniers cas étant eux mêmes inutiles.

Solvabilité et cohérence

Se pose immédiatement le problème de la forme des contraintes autorisées dans C. Sontelles seulement des contraintes entre variables ? –cela ne serait pas suffisant. Doiventelles êtres prouvables ? –mais alors elles seraient inutiles…

Certains ensembles de contraintes semblent aberrants parce qu’ils contiennent des contraintes “absurdes” telles que ∅ <: Pre τ. Une telle contrainte n’est évidemment pas valide (i.e. il est faut de dire ∅ ⊢ ∅ <: Pre τ), mais d’autres ensembles de contraintes non valides semblent plus raisonnables ; par exemple, l’ensemble réduit à la contrainte α <: τ si τ n’est pas exactement α n’est pas valide ; cependant, il existe une substitution qui le rend valide, en l’occurrence [τ/α].

Définition 3 (Solvabilité) Nous dirons qu’un ensemble de contraintes C est solvable, et on note ⊧ C, s’il existe une substitution θ de V vers des termes sans variable telle que ⊢ θ(C).

La solvabilité est une définition sémantique. Nous alors par la suite donner une définition syntaxique et nous vérifierons que les deux coïncides exactement.

Remarque S’il existe une substitution θ vers des termes avec variables, telle que ⊢ θ(C), elle peut-être spécialisée en une substitution sans variable, car on n’a pu utilisé d’autre règle sur les variables que la reflexivité, dont on peut instantier les variables par n’importe quel constante, et ainsi C est solvable. Nous avons conservé la restriction parce que le concept de solvabilité est liée à une notion sémantique, et il est usuel de donné la sémantique des termes avec variables par des ensembles de termes sans variables.

Exemple La contrainte ∅ <: Pre τ n’est pas solvable, mais α <: τ l’est.

Exercice 41 Reprenons l’exercice 38 ci-dessus. Nous voulions donner à fun (x) {ℓ = x} le type α → {ℓ : α′} pourvu que α <: α′. Vérifier que la contrainte α <: α′ est solvable. Montrer qu’on peut alors effectuer une dérivation dans le système de l’exercice précédent (première partie).

La solvabilité est une notion sémantique, difficile à manipuler : pour tester la solvabilité, il faudrait, a priori, essayer toutes les substitutions, mais aussi ensuite rechercher pour chaque contrainte une preuve de sa validité sans utiliser d’hypothèse. On cherche donc une notion syntaxique qui lui soit équivalente. C’est la notion de cohérence. On souhaite au mieux que la solvabilité corresponde à la cohérence. Au pire, on se contentera de du fait la cohérence implique la solvabilité.

Dans un premier temps, nous cherchons des propriétés des ensembles de contraintes solvables. Nous regarderons ensuite si ces propriétés sont suffisantes pour caractériser la solvabilité.

La solvabilité d’un ensemble de contrainte implique la solvabilité de chacune des constraintes. La réciproque est fausse bien sûr. Par exemple les contraintes τ → τ → α et α → {} sont solvables indépendemment, mais {τ → τ → α, α → {}} ne l’est pas.

Remarquons que si ⊧ C_{1} et C_{1} ⊢ C_{2}, alors ⊧ C_{2}. En effet si C_{1} est solvable, alors il existe une subsitution θ telle que ⊢ θ(C_{1}). Par subsitutivité, nous avons θ(C_{1}) ⊢ θ(C_{2}), puis par transitivité, nous avons ⊢ θ(C_{2}). Donc ⊧ C_{2}.

Nous pouvons utiliser la contraposée comme une condition nécessaire de solvabilité.

Définition 4 (fermeture) On dit qu’un ensemble C est fermé (par transitivité et propagation) s’il satisfait les conditions suivantes :

τ_{1} <: τ_{2} ∈ C ∧ τ_{2} <: τ_{3} ∈ C ⟹ τ_{1} <: τ_{3} ∈ C  (P-Trans)
Pre τ <: Pre τ′ ∈ C ⟹ τ <: τ′ ∈ C  (P-Pre)
τ_{1} → τ_{2} <: τ′_{1} → τ′_{2} ∈ C ⟹ τ_{2} <: τ′_{2} ∈ C ∧ τ′_{1} <: τ_{1} ∈ C (P-Arrow)
{ℓ_{i} : τ_{i}^{i∈I}} <: {ℓ_{i} : τ′_{i}^{i∈I}} ∈ C ⟹ ∀i ∈ I, τ_{i} <: τ′_{i} ∈ C  (P-Record)

On note C^{∗} la fermeture de C, c’est-à-dire le plus petit ensemble fermé contenant C. Remarquer la fermeture d’un ensemble n’introduit que des relations de sous-typage entre des sous-termes de l’ensemble initiale. Elle comporte au plus n^{2} termes composés de sous-termes. Elle est donc au plus de taille n^{3} (n^{2} avec partage). En fait, elle peut se calculer en temps O(n^{3}) (comme la fermeture transitive simple).

Proposition 13 Si ⊧ C, alors ⊧ C^{∗}.

\underline{Preuve} : Il suffit de vérifier que C^{∗} ⊢ C.

Définition 5 (Incohérence immédiate) Un ensemble de contraintes est immédiatement incohérent s’il contient une contrainte τ_{1} <: τ_{2} tel que l’on, simultanément,

1. τ_{1} et τ_{2} ont des constructeurs de tête différents,

2. τ_{1} ≢ ⊥ et τ_{2} ≢,

3. τ_{1} ≢ Pre τ ou τ_{2} ≢ ∅.

Proposition 14 Un ensemble de contraintes immédiatement incohérent n’est pas solvable.

\underline{Preuve} : Il suffit de le montrer pour une seule contrainte ⊢ τ_{1} <: τ_{2}. Par induction sur une dérivation du jugement précédent. Le jugement précédent n’est filtré par auncune des conclusions des règles que Trans. Mais alors l’une des deux prémisse est nécessairement immédiatement incohérente.

Comme corrolaire, un ensemble fermé immédiatement incohérent n’est pas solvable. La réciproque n’est cependant pas vraie : une ensemble fermé qui n’est pas immédiatement cohérent n’est pas nécessairement solvable.

Une exemple est la contrainte {α → ⊥ <: α, ⊥ <: α → α}. On pourrait montrer que la relation d’équivalence engendrée par la relation de sous-typage est l’égalité. Donc ici, une solution devrait vérifier τ = ⊥ → τ. Cela n’est possible qu’en présence de types récursifs.

Exercice 42 Vérifier que l’ensemble de contraintes {α → ⊥ <: α, α <: ⊥ → α} est cohérence. Montrer qu’il est solvable.

L’ensemble de contraintes {α → ⊥ <: α, α <: α → ⊤} est-il solvable ?

La cohérence n’implique donc pas la solvabilité en l’absence de types récursifs. Par contre, cela devient vrai en présence de types récursifs. En fait nous ne connaissons de critère simple caractérisant la solvabilité sans types récursifs uniquement en l’absence de constructeur de type contravariant. Ce sous-cas n’est pas intéressant.

5.2.1 Types récursifs

Présentation syntaxique On introduit une notation rec α.τ

τ ::= … | rec α.τ

Il faut alors ajouter définir l’égalité par un système d’inférence, qui ajoute au règles structurelles (reflexivité, transitivité, congruence) les règles d’inférence suivantes :

rec α.τ = τ[rec α.τ/α] \frac{τ_{1} = τ_{2}}{rec α.τ_{1} = rec α.τ_{2}}

\frac{τ_{1} = τ[τ_{1}/α] τ_{2} = τ[τ_{2}/α] τ ≠ α}{τ_{1} = τ_{2}}

Arbre infinis rationnels Les types récursifs sont des arbres infinis rationnels, c’està-dire des arbres infinis ne possédant qu’un nombre fini de sous-termes. Un arbre infini est défini par une fonction qui associe à chaque occurence (suite finie d’entiers non nuls) un symbole. Le domaine de cette fonction doit être clos par préfixes. Il doit aussi être bien formé, compte tenu de l’arité des symboles.

Un arbre rationnel peut aussi être défini implicitement par un ensemble d’équations récursives contractives, i.e. de la forme (α_{i} = τ_{i})^{i∈I} où aucun des termes τ_{i} ne n’est une variable.

Nous préférons cette dernière représentation.

Sous-typage sur les types récursifs On peut définir le sous-typage en étendant la présentation syntaxique, avec une nouvelle règle d’inclusion de la forme :

(<:-Rec-Pos) ; \frac{C ⊕ α <: τ ⊕ α <: τ′ ⊢ τ <: τ′}{C ⊕ α <: τ ⊢ τ <: τ′}  (<:-Rec-Neg) ; \frac{C ⊕ τ <: α ⊕ τ′ <: α′ ⊢ τ′ <: τ}{C ⊕ τ <: α ⊢ τ′ <: τ}

Pour les types sans variables, soit deux termes récursifs τ_{1} et τ_{2} définis par le système d’équations contractives C. Alors on défini τ_{1} <: τ_{2} comme C ⊢ τ_{1} <: τ_{2}.

On peut alors montrer que la relation de sous-typage sur les types sans variables est la plus grande relation immédiatement cohérente, transitive et fermée par propagation.

Nous admettrons la propriété suivante :

Proposition 15 Un ensemble de contraintes C fermé et immédiatement cohérent admet une solution avec des types récursifs sans variable.

5.2.2 Implication de contraintes

Nous avons défini une relation de sous-typage sur les types sans variable de façon syntaxique. Nous l’avons étendue à des jugements d’inclusion sous contraintes toujours de façon syntaxique.

D’un autre coté nous avons introduit une notion sémantique, la solvabilité, et nous avons montrée qu’elle coïncidait avec une notion syntaxique de cohérence.

Nous pouvons maintenant définir une notion sémantique d’implication de contrainte, afin de tester la généralité de notre définition syntaxique.

Définition 6 Nous disons qu’un ensemble de contrainte C_{1} implique un ensemble de contrainte C_{2}, et nous notons C_{1} ⊃ C_{2}, si toute solution de C_{1} est également solution de C_{2}.

Attention ! sous forme mathématique C_{1} ⊃ C_{2} signifie ∀θ, θ(C_{1}) ⊃ θ(C_{2}) ce qu’il ne faut pas confondre avec la propriété (⊧ C_{1}) ⟹ (⊧ C_{2}) qui est une conséquence de la précédente. Comme cas particulier, nous avons alors un jugement sémantique d’inclusion C ⊃ τ_{1} <: τ_{2}.

Nous savons, en combinant la subsitutivité et la transitivité que si C_{1} ⊢ C_{2}, alors C_{1} ⊃ C_{2}. Cette propriété est rassurante puisque les relations de sous-typage que l’on peut dériver syntaxiquement sont toujours correctes sémantiquement. La réciproque n’est pas vraie. Nous avons vue que ⊧ C entraîne ⊧ C^{∗}. En fait, la preuve montre que plus précisément, nous avons C ⊃ C^{∗}. Le jugement sémantique inverse C^{∗} ⊃ C est vrai puisque le jugement syntaxique C^{∗} ⊢ C l’est aussi. Mais, inversement, il est faut que C ⊢ C^{∗}. Les ensembles de contraintes C et C^{∗} sont équivalents sémantiquement, mais pas syntaxiquement.

Nous pouvons définir une relation ⊢ plus forte que la notion de déduction ⊃. Nous écrivons C_{1} ⊢ C_{2} if C_{1}^{∗} ⊢ C_{2}. L’idée est que les contraintes de C_{2} sont impliquées par celles de C_{1}, par fermeture ou par déduction. La relation ⊢ est encore une notion syntaxique. Elle approche plus la relation sémantique, et possède de bonne propriété, mais elle n’est toujours pas identique à la notion sémantique. C’est encore un problème ouvert de trouver une caractérisation syntaxique de la relation sémantique.

Exercice 43 Considérons l’ensemble de contraintes C réduit à α <: ⊤ → α et ⊥ → α′ <: α′. Montrer que C ⊧ α <: α′ alors que C ⊬ α <: α′.

Dans la suite nous utiliserons la relation ⊢, mais on peut la remplacer par une autre relation, en particulier ⊃, qui vérifie les propriétés suivantes :

Proposition 16 la relation ⊢ est réflexive et transitive. D’autre part, si C_{1} ⊢ C_{2}, alors

1. C_{1} ⊢ C_{2}^{∗},

2. (⊧ C_{1}) ⟹ (⊧ C_{2})

3. ∀C, C_{1} ∪ C ⊢ C_{2} ∪ C. (En particulier, ∀ θ, θ(C_{1}) ⊢ θ(C_{2}). )

\underline{Preuve} : La réflexitivé et la transitivité découlent facilement de la définition et de la transitivité de ⊢. Supposons C_{1} ⊃ C_{2}, c’est-à-dire C_{1}^{∗} ⊢ C_{2}.

Cas 1 : C’est-à-dire C_{1}^{∗} ⊢ C_{2}^{∗}. On le montre par récurrence sur la construction de C_{2}^{∗}.

Cas 2 : C’est-à-dire que si C_{1}^{∗} est immédiatement cohérent. alors C_{2}^{∗} l’est aussi. C’est une conséquence immédaite de C_{1}^{∗} ⊢ C_{2}^{∗} (première propriété).

Cas 3 : Il faut montrer (C_{1} ∪ C)^{∗} ⊢ C_{2} ∪ C. Comme C_{1}^{∗} est inclus dans (C_{1} ∪ C)^{∗} et C_{1}^{∗} ⊢ C_{2}, on a (C_{1} ∪ C)^{∗} ⊃ C_{2}. De même C est inclus dans (C_{1} ∪ C)^{∗}, donc (C_{1} ∪ C)^{∗} ⊢ C.

5.3 Un système de typage avec contraintes

Nous avons mentionné la nécessité de considérer des jugements de sous-typage sous des hypothèses d’inclusion. Dans l’exercice 38, page 61, nous avons également proposé d’associer à la fonction fun (x) {ℓ = x} le type α → {ℓ : Pre α′; ∅} pourvu que α <: α′.

Nous devons naturellement incorporer les hypothèses d’inclusion dans les jugements de typage. Nous écrirons des jugements de typage de la forme C, A ⊢ a : τ où C est un ensemble de contraintes cohérentes. Les contraintes C portent sur tout le jugement, donc sur A autant que sur τ.

Pour pouvoir écrire que fun (x) {ℓ = x} a le type α → {ℓ : Pre α′} pourvu que α <: α′, et pouvoir lier cette expression, nous sommes aussi amenés à étendre les schémas de types pouvant apparaître dans un environnement de typage à des schémas de types contraints de la forme ∀ ᾱ | C. τ où C est un ensemble de contraintes cohérentes. La notation ∀ α. τ peut être vue comme une abréviation pour ∀ α | ∅. τ. Par exemple, le type de la fonction ci-dessus sera ∀ α, α′ | α <: α′. α → {ℓ : Pre α′}

Les constantes du langage ont pour schémas de types :

{ℓ_{i} : ^{i∈1..n}} : ∀ α_{1}, … α_{n}. α_{1} → … α_{n} → {ℓ_{i} : Pre α_{i}^{i∈1..n}}
( .ℓ) : ∀ α. {ℓ : Pre α} → α

Remarquons que le type de l’extraction est plus faible que le type que nous lui avions donné dans le chapitre précédent, puisque pour simplifier nous avons retiré les variables de rangée. En ML, ce type ne serait pas assez général car nous ne pourrions pas appliquer cette fonction à des enregistrements possédant d’autres champs que ℓ. Le mécanisme de sous-typage permet quand même de typer de telles applications.

Les règles de typage sont les suivantes :

(Var-Inst) ; \frac{z : ∀ ᾱ | C_{0}. τ_{0} ∈ A C ⊢ C_{0}[τ̄/ᾱ]}{C, A ⊢ z : τ_{0}[τ̄/ᾱ]}  (Fun) ; \frac{C, A ⊕ (x : τ_{2}) ⊢ a : τ_{1}}{C, A ⊢ fun (x) a : τ_{2} → τ_{1}}

(Gen-Let)

\frac{C, A ⊢ a_{1} : τ_{1} C, A ⊕ (x : ∀ ᾱ | C_{0}. τ_{1}) ⊢ a_{2} : τ_{2} ᾱ ∉ F V (A) ∪ F V (C \ C_{0})}{C, A ⊢ let x = a_{1} in a_{2} : τ_{2}}

(App) ; \frac{C, A ⊢ a_{1} : τ_{0} → τ  C, A ⊢ a_{2} : τ_{0}}{C, A ⊢ a_{1} a_{2} : τ}  (Sub) ; \frac{C, A ⊢ a ⊢ τ  C ⊢ τ <: τ′}{C, A ⊢ a : τ′}

L’abstraction et l’application sont typées comme en ML et les contraintes sont propagées des prémisses aux conclusions. Une variable dont le schéma de type est ∀ ᾱ. τ est typée en substituant les variables génériques par des types pourvu que cette même substitution appliquée à C_{0} soit un ensemble de contraintes impliquées par les contraintes du jugement. Le typage d’une liaison let x = a_{1} in a_{2} est aussi similaire à celui d’une liaison en ML, mais il faut généraliser les contraintes du typage de a_{1} en même temps que le type τ_{1} de a_{1}. En fait seule les contraintes possédant des variables génériques ont besoin d’être incluses dans le schéma de type. Il est important de laissé une copie des contraintes non généralisées dans C, car si la variable x n’est pas utilisé dans a_{2}, c’est la seule façon d’assurer la cohérence de C_{0} (dont une instance est incluse dans C).

Enfin, la règle de sous-typage nous dit que si une expression a a un type τ dans un environnement A et sous les contraintes C, et si les contraintes (cohérentes par définition) impliquent que τ est un sous-type de τ′, alors a a aussi le type τ. Sans la condition de cohérence des contraintes dans les jugements de typage, tous les programmes seraient typables.

Exercice 44 En supposant que les constantes incluent les entiers, montrer que le non respect de la condition ci-dessus permettrait de typer le programme 1 (fun (x) x) dans l’environnement vide avec le type Int pourvu qu’un certain ensemble de contraintes soit satisfaites. Montrer que ce programme n’est plus typable (en respectant la condition de cohérence)

Propriétés du système de typage

Par combinaison des règles Sub et App, la règle suivante est dérivable :

(App’) ; \frac{C, A ⊢ a_{1} : τ_{1} → τ C, A ⊢ a_{2} : τ_{2} C ⊢ τ_{2} <: τ_{1}}{C, A ⊢ a_{1} a_{2} : τ}

Une dérivation dans le système obtenu en remplaçant la règle App par la règle App’ et où la règle Sub n’est éventuellement utilisée qu’en ultime position est dite canonique. On peut alors montrer le lemme suivant qui permettra de simplifier toutes les preuves en ne regardant que des dérivations canoniques.

Lemme 17 (Dérivation canoniques) Tout jugement prouvable possède une dérivation canonique.

\underline{Preuve} : La démonstration est simple. Elle consiste à montrer que la règle Sub commute vers le bas avec toutes les autres règles (sauf App qui a été remplacée par App’), i.e. Var-Inst, Fun, App’ et Let. Les seuls cas intéressants sont ceux de la règle App’ et Fun, car ils utilisent les propriétés de propagation et de cohérence associées au symbole flèche.

Cas App’ : Nous avons une dérivation de la forme

\begin{aligned}C, A ⊢ a_{1} : τ_{1}  C ⊢ τ_{1} <: τ_{2} → τ (1) \\ & (Sub) \\ C, A ⊢ a_{1} : τ_{2} → τ \end{aligned}  C, A ⊢ a_{2} : τ_{2} (App’)
C, A ⊢ a_{1} : τ′_{2} → τ  \begin{aligned}C, A ⊢ a_{2} : τ_{2}  (2) \\ & (Sub) \\ C, A ⊢ a_{2} : τ′_{2} \end{aligned} (App’)

C, A ⊢ a_{1} a_{2} : τ (3) (Sub)

C, A ⊢ a_{1} a_{2} : τ La cohérence de C et (1) entraînent que τ_{1} doit être de la forme τ′_{2} → τ′ et la règle de propagation implique C ⊢ τ′_{2} <: τ_{2} (2) et C ⊢ τ <: τ′ (3). On peut donc effectuer la dérivation suivante :

C, A ⊢ a_{1} a_{2} : τ′

Cas Fun : Nous avons une dérivation de la forme

C, A ⊕ x : τ ⊢ a : τ_{1} C ⊢ τ_{1} <: τ_{2} (Sub)

C, A ⊕ x : τ ⊢ a : τ_{2} (Fun)

C, A ⊢ fun (x) a : τ → τ_{2}

De C ⊢ τ_{1} <: τ_{2} nous pouvons déduire C ⊢ τ → τ_{1} <: τ → τ_{2}. Ainsi, nous avons la dérivation suivante :

\begin{aligned}C, A ⊕ x : τ ⊢ a : τ_{1} \\ & (Fun) \\ C, A ⊢ fun (x) a : τ → τ_{1} \end{aligned} C ⊢ τ → τ_{1} <: τ → τ_{2} (Sub)

C, A ⊢ fun (x) a : τ → τ_{1}

Cas Let : Il y a deux cas possibles, selon que la règle Sub peut être appliquée à la prémisse droite ou à la prémisse gauche. Dans le premier cas, la commutation est immédiate. Dans le second cas, nous avons une dérivation de la forme :

\begin{aligned}C, A ⊢ a_{1} : τ_{1}  C ⊢ τ_{1} <: τ_{2} (1) \\ & (Sub) \\ C, A ⊢ a_{1} : t_{2} \end{aligned}  C, A ⊕ (x : ∀ ᾱ | C_{0}. τ_{2}) ⊢ a_{2} : τ (Let)
C, A ⊢ let x = a_{1} in a_{2} : τ

Il est alors facile de montrer, par récurrence sur la taille de la dérivation, que l’on peut dériver C, A ⊕ (x : ∀ ᾱ | C_{0}. τ_{2}) ⊢ a_{2} : τ en ajoutant dans la dérivation ci-dessus une règle Sub à toutes les occurrences de la règle Var-Inst appliquées à la variable x.

Cas Var-Inst : Comme c’est un axiome, cette règle ne peut pas être précédée d’une règle Sub.

Nous pouvons également montrer un lemme de substitution. Une différence par rapport à ML est qu’un jugement de typage n’est préservé par substitution, que si la substitution préserve la cohérence de ses contraintes.

Lemme 18 (Substitutivité) Si C, A ⊢ a : τ et θ est une substitution telle que θ(C) est cohérent, alors θ(C), θ(A) ⊢ a : θ(τ)

Les propriétés de généralisation et d’extension de contexte sont conservées : On dit que ∀ ᾱ | C. τ est plus général ∀ ᾱ′ | C′. τ′ s’il existe une substitution θ de domaine ᾱ telle que θ(τ) = τ′ et θ(C) ⊢ C′.

Proposition 19 (Extension de l’environnement de typage) Si les affectations de types A et B sont identiques partout sauf peut-être sur les variables qui ne sont pas libres dans a, alors C, A ⊢ a : τ est dérivable si et seulement si C, B ⊢ a : τ l’est.

Proposition 20 (Généralisation du contexte) Si C, A ⊢ a : τ et si A et B ont même domaine, et que pour tout z de ce domaine, B(z) est plus général que A(z), alors C, B ⊢ a : τ.

On montre également le lemme suivant qui correspond au renforcement d’hypothèses :

Proposition 21 (Renforcement des contraintes) Si C, A ⊢ a : τ et si C′ ⊢ C et C′ est cohérent, alors C′, A ⊢ a : τ.

\underline{Preuve} : Il suffit de remplacer chaque utilisation de C ⊢ τ <: τ′ dans une dérivation de la prémisse par C′ ⊢ τ <: τ′ qui découle de la transitivité de ⊢.

5.4 Sûreté du typage

Nous montrons maintenant la correction du typage pour la sémantique à petits pas.

Comme pour le langage ML, la correction du typage s’exprime par deux résultats complémentaires. Le théorème 5 (d’auto-réduction) affirme que les typages sont préservés par réduction. Le théorème 6 (des termes irréductibles) certifie que les programmes bien typés irréductibles sont des valeurs. La combinaison des deux théorèmes permet donc d’affirmer que la réduction des programmes bien typés ne peut s’arrêter que sur des valeurs.

Un typage pour une expression a est un triplet (A, τ, C) tel que C, A ⊢ a : τ. L’inclusion des typages induit une relation ⊂ sur les termes. Noues écrivons a_{1} ⊂ a_{2} pour signifier que tous les typages de a_{1} sont aussi des typages de a_{2}. Le théorème d’auto-réduction s’écrit alors comme la préservation des typages pendant la réduction.

Théorème 5 (auto-réduction) La réduction est une sous-relation de ⊂ (avec des symboles, si a_{1} ⟶ a_{2}, alors a_{1} ⊂ a_{2}),

La preuve est simplifiée par les lemmes suivants :

Lemme 22 La relation ⊂ est croissante, c’est-à-dire si a_{1} ⊂ a_{2}, alors E[a_{1}] ⊂ E[a_{2}].

\underline{Preuve} : Par récurrence structurelle sur E (voir le chapitre 2)

Lemme 23 (Remplacement dans un terme) Si C, A ⊢ v : τ_{0} (1) et C, A ⊕ (x : ∀ α_{0} | C_{0}. τ_{0}) ⊢ a : τ (2), et si les variables ᾱ_{0} ne sont pas libres dans A et C_{0} est un sous-ensemble de C contenant au moins toutes les coercions de C où apparaissent des variables de ᾱ_{0}, alors C, A ⊢ a[v/x] : τ.

\underline{Preuve} : La preuve est une récurrence structurelle sur l’expression a. Nous notons A_{0} pour A ⊕ (x : ∀ α_{0} | C_{0}. τ_{0}).

Dans chaque cas, nous considérons d’abord une dérivation canonique de (1) qui ne se termine pas par une règle Sub, et nous montrons qu’il est possible de construire une dérivation de (2). Si une preuve canonique de (1) se termine pas une règle Sub, alors il existe une dérivation C, A_{0} ⊢ a : τ′ qui ne se termine pas par une règle Sub, et d’autre part C ⊢ τ′ <: τ. Par hypothèse de récurrence, il existe une dérivation de C, A ⊢ a[v/x] : τ′, et l’on conclut par la règle Sub.

En fait, pour chaque cas le raisonnement est identique à celui du chapitre 1 en remplaçant les types par des types contraints.

5.4. SÛRETÉ DU TYPAGE 73

Cas a est x: Les termes a[v/x] et v sont égaux. De la dérivation de (2), il découle que τ est de la forme θ(τ_{0}) où dom (θ) est égal à ᾱ_{0}, et C ⊢ θ(C_{0}) (3).

Nous pouvons appliquer le lemme de substitution 18 à (1). En effet, il découle de (3) et du fait que C est cohérent que θ(C_{0}) l’est aussi. On obtient donc θ(C), A ⊢ v : τ. D’autre part C contient θ(C) et est cohérent. Par le lemme de renforcement des contraintes 21, C, A ⊢ v : τ.

Cas a est z et z ≠ x: Les termes a[v/x] et a sont égaux et x n’est pas libre dans a. Donc A(z) est identique à A_{0}(z) et on peut conclure avec la même règle Var que celle utilisée pour typer a.

Cas a est let y = a_{1} in a_{2} : La dérivation canonique de (2) se termine par :

(3) C, A_{0} ⊢ a_{1} : τ_{1} (4) C, A_{0} ⊕ (y : σ1) ⊢ a_{2} : τ (Let)

A_{0} ⊢ let y = a_{1} in a_{2} : τ

où σ_{1} est ∀ ᾱ_{1} | C_{1}. En utilisant le lemme de généralisation de contexte, nous pouvons supposé que ᾱ_{1} include all variables that are not free in A. Ainsi l’ajout de y : σ_{1} au contexte A ne modifie pas les variables libres du contexte. Par l’hypothèse de récurrence appliquée à (3), nous savons que A ⊢ a_{1}[v/x] : τ_{1} (5). Par le lemme de généralisation de En réarrangeant les contextes par la propriété 21, page 70 on obtient C, A⊕(y : σ_{1})⊕(x : ∀ ᾱ_{0} | C_{0}. τ_{0}) ⊢ a_{2} : τ (6). Comme y n’est pas libre dans v, nous avons aussi C, A⊕(y : σ_{1}) ⊢ v : τ_{0} (7), puis en appliquant l’hypothèse de récurrence à (7) et (6) :

C, A ⊕ (y : σ_{1}) ⊢ a_{2}[v/x] : τ (8)

Nous concluons par l’application de la règle Let à (5) et (8).

Cas a est fun (y) a_{1} : La dérivation canonique de (1) doit se terminer par :

\frac{C, A_{0} ⊕ (y : τ_{2}) ⊢ a_{1} : τ_{1} (4)}{C, A_{0} ⊢ fun (y) a_{1} : τ_{2} → τ_{1}}

où τ est τ_{2} → τ_{1}. En réarrangeant le contexte (4), nous obtenons C, A ⊕ (y : τ_{2}) ⊕ (x : τ_{0}) ⊢ a_{1} : τ_{1} (5). En étendant le contexte (2), nous avons C_{0}, A⊕(y : τ_{2}) ⊢ v : τ_{0} (6). Par application de l’hypothèse de récurrence à (5) et (6), nous obtenons C, A ⊕ (y : τ_{2}) ⊢ a_{1}[v/x] : τ_{1}. Nous concluons en appliquant la règle Fun.

Cas a est a_{1} a_{2} : La dérivation canonique de (1) doit se terminer par une règle App’ et donc en particulier (en remplaçant la règle App’ par sa définition) une règle App :

\frac{C, A_{0} ⊢ a_{1} : τ_{2} → τ (1) C, A_{0} ⊢ a_{2} : τ_{2} (2)}{C, A_{0} ⊢ a_{1} a_{2} : τ}

En appliquant l’hypothèse de récurrence à chaque prémisse (qui sont toutes deux canoniques), nous obtenons C, A ⊢ a_{1}[v/x] : τ_{0} → τ (4) et C, A ⊢ a_{2}[v/x] : τ_{2} (5). Puis la conclusion par une règle App.

\underline{Preuve} : [de l’auto-réduction] En utilisant le lemme 22, il est suffisant de montrer l’autoréduction pour chaque radical. De plus, nous pouvons montrer chaque cas indépendamment. Le lemme peut d’abord être montré pour des typages dont une dérivation canonique ne se termine pas par une règle de sous-typage. Le cas général en découle ensuite par application d’une règle de sous-typage.

74 CHAPITRE 5. TYPAGE AVEC CONTRAINTES

Cas a_{1} est let x = v in a: La dérivation canonique se termine par :

C, A ⊢ v : τ_{1} (3) C, A ⊕ (x : ∀ ᾱ | C′. τ_{1}) ⊢ a : τ (1) (Let)

C, A ⊢ let x = v in a : τ

où, ᾱ est inclus dans F V (A) et F V (C \ C′). En particulier, les conditions du lemme 23 sont remplies, ce qui nous permet de conclure.

Cas a_{1} est (fun (x) a) v: La dérivation canonique se termine par :

\begin{aligned}C, A ⊕ (x : τ_{1}) ⊢ a : τ (1) \\ & (Fun) \\ C, A ⊢ fun (x) a : τ_{1} → τ \end{aligned}  \frac{C, A ⊢ v : τ_{2} (2)  C ⊢ τ_{2} <: τ_{0}}{C, A ⊢ v : τ_{1} (3)}

(App)

C, A ⊢ (fun (x) a) v : τ

Nous pouvons donc conclure par application du lemme 23.

Cas a est {ℓ_{i} = a_{i}^{i∈1..n}}.ℓ_{j} pour j dans 1..n: La dérivation canonique doit se terminer comme suit :

C, A ⊢ v_{i} : τ_{i} ∀i ∈ 1..n (1) (Record)

C, A ⊢ {ℓ_{i} = v_{i}^{i∈1..n}} : {ℓ_{i} : Pre τ_{i}^{i∈1..n}}

· ; · ; · ; · ; · ; · ; · ; · ; ·

C, A ⊢ (ℓ_{j}. ) : {ℓ_{j} : Pre τ_{0}} → τ_{0}

C ⊢ {ℓ : Pre τ_{0}} → τ_{0} <: {ℓ_{i} : Pre τ_{i}^{i∈1..n}} → τ (2) \overline{(Sub)}

C, A ⊢ (ℓ_{j}. ) : {ℓ_{i} : Pre τ_{i}^{i∈1..n}} → τ (App)

C, A ⊢ {ℓ_{i} = v_{i}^{i∈1..n}}.ℓ_{j} : τ

La relation (2) ne peut être satisfaite que si C ⊢ τ_{j} <: τ_{0} et C ⊢ τ_{0} <: τ et donc en particulier C ⊢ τ_{j} <: τ (3). La conclusion s’obtient en appliquant la règle Sub à (1) et (3).

Théorème 6 (Termes irréductibles) Les termes bien typés irréductibles sont des valeurs.

\underline{Preuve} : La difficulté est de montrer que la forme des valeurs correspond à la forme de leur type. Ceci repose évidemment sur la cohérence des contraintes. Nous montrons d’abord que pour toute dérivation canonique du jugement C, ⊢ v : τ qui ne se termine pas par une règle Sub,

• Si v est une fonction alors τ est τ_{1} → τ_{2},
• Si v est de la forme {ℓ_{i} = v_{i}^{i∈1..n}}, alors τ est de la forme {ℓ_{i} : Pre τ_{i}^{i∈1..n}},

Les structures de ces types sont deux à deux disjointes ; nous avons considéré tous les cas de valeurs ; nous pouvons donc inverser les implications :

• Si τ est τ_{1} → τ_{2} alors v est une fonction,
• Si τ est {ℓ_{i} : Pre τ_{i}^{i∈1..n}} alors v est un enregistrement de la forme {ℓ_{i} = v_{i}^{i∈1..n}},

Si la dérivation canonique de C, ⊢ v : τ se termine par une règle Sub, alors il y a une dérivation C, ⊢ v : τ′ qui ne se termine pas par une règle Sub et telle que C ⊢ τ <: τ′. Puisque τ′ ne peut pas être une variable, nous pouvons déduire de la relation de cohérence :

5.5. DISCUSSION 75

• Si τ est τ_{1} → τ_{2} alors τ′ est de la forme τ′_{1} → τ′_{2} ; ainsi v est une fonction.

• Si τ est {ℓ_{i} : Pre τ_{i}^{i∈1..n}} alors τ′ est de la forme {ℓ_{i} : Pre τ′_{i}^{i∈1..n+p}}, ainsi v est un enregistrement {ℓ_{i} = v_{i}^{i∈1..n+p}}.

Nous pouvons maintenant prouver le fait que les termes bien typés irréductibles sont des valeurs, par récurrence structurelle sur un tel terme a. Considérons une dérivation canonique d’un typage de a. Après avoir retiré la dernière règle de la dérivation si c’est une règle Sub, nous avons une dérivation du jugement C, ⊢ a : τ (1) qui ne se termine pas par une règle Sub.

Cas a est x: n’est pas possible puisque a est une expression fermée.

Cas a est fun (x) a_{1} : alors a est une valeur.

Cas a est une application a_{1} a_{2} : La dérivation de (1) se termine par :

\frac{⊢ C, a_{1} : τ_{2} → τ_{1} C, ⊢ a_{2} : τ_{2}}{⊢ C, a_{1} a_{2} : τ_{1}}

Par hypothèse de récurrence, a_{1} est une valeur. Puisque a_{1} a un type fonctionnel, ou bien c’est une fonction et a peut se réduire ou bien une application de primitive :

Sous-cas a est {ℓ_{i} = a_{i}^{i∈1..n}}: La dérivation canonique de (1) se termine par :

C, A ⊢ a_{i} : τ_{i} ∀i ∈ 1..n … (App)

C, A ⊢ a : {ℓ_{i} : Pre τ_{i}^{i∈1..n}}

Par hypothèse de récurrence, tous les a_{i} doivent être des valeurs donc a est également une valeur.

Sous-cas a est a_{1}.ℓ: La dérivation canonique de (1) se termine par :

C, A ⊢ a_{1} : {ℓ_{i} : Pre τ_{i}^{i∈1..n}} … (App)

C, A ⊢ a_{1}.ℓ_{i} : τ

Par hypothèse de récurrence, a_{1} doit être une valeur, donc il est de la forme {ℓ_{i} : v_{i}^{i∈1..n}} et a peut se réduire.

5.5 Discussion

Synthèse de types

Il est facile de déduire du formalisme de la section 5.3 un algorithme de synthèse de types avec contraintes. L’existence de dérivations canoniques conduit à un système de typage dirigé par la syntaxe. La seule flexibilité restante est dans l’ensemble des variables généralisables. On pourra choisir ∀ ᾱ | C_{0}. τ pour Gen(τ, A, C) tel que ᾱ soit le plus petit ensemble contenant toutes les variables libres de τ qui ne sont pas dans A, et toutes les variables libre de C qui ne sont pas dans A et atteignable à partir d’autres variables de α. On choisi alors pour C′ le plus petit ensemble satisfaisant la condition. L’ajout ultérieur de contraintes à C′ ne modifie pas ce choix.

Étant donné un programme a on cherche a trouver un type τ et un ensemble de contraintes C telles que C, A_{0} ⊢ a : τ. L’ensemble de contraintes C devra être le même dans chaque sous jugement de typage. Il suffit donc de parcourir récursivement l’expression a en construisant le type τ et en collectionnant les contraintes C. Nous vérifions a posteriori la cohérence de C, ce qui nous permettra de garantir que chacune des étapes précédentes était correcte. Si C n’est pas cohérent, alors il n’existe pas de dérivation possible.

Pour la synthèse des types, on préferera en général effectuer des simplifications en cours de calcul comme évoqué ci-dessous. La présentation avec la règle App” décrite ci-dessous est également mieux adaptée au sous-typage.

Exercice 45 Réaliser une maquette de la synthèse de type pour le langage de ce chapitre. Utiliser des structures de donnée simples sans trop se préoccuper de l’efficacité. L’algorithme devrait fonctionner en un temps très raisonnable sur des exemples de quelques lignes. Essayer les exemples de ce chapitre et quelques fonctions très simples.

Il pourra être intéressant d’ajouter les variantes (voir l’exercice 46).

Le nombre de contraintes obtenues pour une expression a sera au moins égal au nombre de nœuds d’application (c’est exactement ce nombre pour un programme sans liaison). Cet ensemble est donc au moins de la taille du programme. Il faut ensuite en vérifier la cohérence. La fermeture de l’ensemble des contraintes peut en rendre la taille proportionnelle au carré de la taille du programme. Cela pose un double problème. D’une part, les contraintes seront probablement illisibles par l’utilisateur. D’autre part, les calculs peuvent devenir très chers.

5.5.1 Simplification des contraintes

Pour cette raison, il est essentiel de pouvoir simplifier les contraintes. Il y a de nombreuses possibilités de simplification. On pourra d’abord utiliser le lemme de renforcement des contraintes21, voir même en faire une règle dérivée

(Sub-Context)

\frac{C, A ⊢ a : τ C′ ⊢ C}{C′, A ⊢ a : τ}

Le lemme de renforcement des contraintes montre que l’ajout de cette règle ne change pas l’ensemble des jugements dérivables. Par contre, elle augmente le nombre de dérivation d’un jugement, permettant de de simplifier les contraintes a posteriori.

On pourra aussi combiner cette règle avec la règle App’

(App”) ; \frac{C_{1}, A ⊢ a_{1} : τ_{1} C_{2}, A ⊢ a_{2} : τ_{2}}{C_{1} ∪ C_{2} ∪ \{τ_{1} <: τ_{2} → α\}, A ⊢ a_{1} a_{2} : α}

La règle App” permet de Cette règle est encore plus économique, permet d’ajouter les contraintes à la demande (au nœuds d’application) ; elle réduit la taille des dérivations, mais pas la taille des jugements finaux.

Pour réduire vraiment la taille des contraintes, il va falloir introduire plus de jugements de typage. On peut en fait enrichir la relation d’implication entre ensembles de contraintes, en se raprochant de la relation ⊃.

Une autre approche est de permettre de simplifier les schémas de type. On peut définir une relation sémantique

C ⊃ ∀ ᾱ | C_{0}. τ_{0} <: ∀ ᾱ′ | C′_{0}. τ′_{0}

si pour toute substitution θ de ᾱ telle que ⊧ θ(C), pour toute substitution θ_{0} de ᾱ telle que ⊢ (θ_{0} ∘ θ)(C_{0}), il existe une substitution θ′_{0} de ᾱ′ telle que ⊢ (θ′_{0} ∘ θ)(C′_{0}) et ⊢ (θ_{0} ∘θ)(τ_{0}) <: (θ′_{0} ∘θ)(τ′_{0}). Malheureusemnt, cette relation est au moins aussi difficile que l’implication de contraintes C ⊃ C′ qui n’est pas encore bien comprise.

Toutefois, on pourrait utiliser un version syntaxique plus faible

C ⊢ ∀ ᾱ | C_{0}. τ_{0} <: ∀ ᾱ′ | C′_{0}. τ′_{0}

Cette relation sur les schémas, entraîne naturellement un relation entre les jugements de typage, donc une forme plus générale de Sub :

(Sub) ; \frac{C, A ⊢ a : ∀ α | C_{0}. τ_{0} C ⊢ ∀ α | C_{0}. τ_{0} <: ∀ α′_{0} | C′_{0}. τ′_{0}}{C, A ⊢ a : ∀ α′ | C. τ′_{0}}

à condition de réintroduire les règles

(Gen) ; \frac{C, A ⊢ a : τ_{0}  ᾱ ∉ F V (A)}{C, A ⊢ a : ∀ α | C. τ_{0}}  (Inst) ; \frac{C, A ⊢ a : ∀ α | C_{0}. τ_{0} C ⊢ C_{0}[τ̄/ᾱ]}{C, A ⊢ a : τ_{0}[τ̄/ᾱ]}

La simplification des contraintes est encore du domaine de la recherche, et nous ne la détaillerons pas plus ici.

Généralité de l’approche

Notre cas d’étude est un langage avec enregistrements, mais bien sûr, la méthode est générale. Elle s’applique au sous-typage sur les types de base mais aussi (et surtout) au typage des objets. Elle permet également d’améliorer le typage des variantes que nous avons traité dans le chapitre précédent.

Exercice 46 (**) On reprend les variantes traitées dans le chapitre précédent par ajout de constantes. On fera la même simplification sur les types de variantes en retirant les variables de rangée. Quelle relation de sous-typage doit-on définir pour les types variantes (écrire les règles de propagation et de cohérence correspondantes) ? Quels schémas de type faut-il donner aux primitives de construction et destruction des variantes ? Montrer la correction du typage vis à vis de la sémantique.

Enfin nous avons présenté les enregistrements et les opérations associées comme des constantes de façon à montrer comment les preuves pourraient s’étendre à d’autres constantes. Il y a clairement un lien analogue à celui du chapitre 2 entre les δ-règles associées à ces constantes et leur typage (incluant les règles de propagation et les règles de cohérence), mais il est plus difficile de formaliser ce lien dans le cas général.

Nous avons considéré des enregistrements flexibles, non extensibles afin de simplifier le langage des types. Il est possible de revenir à des types enregistrements plus riches avec des variables de rangées comme dans le chapitre précédent. Le système de typage obtenu est plus expressif. Par exemple, il permet de typer l’extension des enregistrements, opération qui n’est pas typable de façon suffisamment polymorphe dans le système présenté dans ce chapitre.

Le sous-typage ne se substitue donc pas aux types enregistrements, mais il les complète de façon orthogonale, et l’on gagne à conserver les variables de rangées en présence de sous-typage.

Exercice 47 (**) Donner un exemple de programme montrant que le sous-typage sans variable de rangée (comme dans ce chapitre) n’est pas aussi expressif que les types enregistrements polymorphes avec variables de rangées (comme dans le chapitre précédent). Donner un exemple inverse. On peut donc ré-introduire les variables de rangée dans les types d’enregistrements en présence de sous-typage. Quelles modifications faut-il apporter au formalisme de ce chapitre ? Vérifier que toutes les propriétés sont conservées.

Raffinement de la relation de sous-typage

Pour des raisons d’exposition, nous avons présenté ici la relation de sous-typage la plus simple entre enregistrements. Il est possible d’enrichir cette relation. Par exemple, il peut-être important de pouvoir connaître par le typage le domaine exact d’un objet enregistrement. Cela ne fonctionne pas avec la relation de sous-typage que nous avons présentée parce qu’il est toujours possible d’oublier la présence des champs dans un type-enregistrement (∅ ⊢ Pre τ <: ∅). Une solution simple consiste à rejeter cette inclusion (i.e. la règle <:-Abs) et à la remplacer par les règles suivantes :

(<:-Abs)

                 \overline{C ⊢ ∅ <: Either}

(<:-Pre)

                                   C ⊢ Pre τ <: Either

où Either est une nouvelle constante de type. Le diagramme suivant schématise la relation de sous-typage.

τ ::= … | Either

                                             Either

[figure]

                                         ∅  Pre τ

On pourra alors typer l’enregistrement x =^{def} {x = 1} avec {x : Pre Int; ∅}, mais l’expression if x then {x = 1} else {x = 2; y = 3} ne pourra être typée qu’avec {x : Pre Int; y : Either; ∅}, se souvenant ainsi que le champ y puisse exister bien qu’innaccessible.

Exercice 48 (**) On reprend l’exercice 46 sur les variantes. En fait on peut ajouter un cas d’évaluation par défaut dans l’analyse par cas. Pour cela on fournit une autre collection de primitives fun ℓ(x) ⇒ a_{1} … | ℓ_{n}(y) ⇒ a_{n} else a_{0}. Pour typer cette fonction il faut revenir à des types variantes plus explicites en faisant apparaître le terme de rangée ∅ et aussi autoriser des termes de rangée Either.

\begin{matrix}τ ::= & … [ℓ_{i} : τ_{i}^{i∈1..i}, \underline{τ}] \\ \underline{τ} ::= & \underline{∅} | \underline{Either} \end{matrix}

Les équations d’extraction sont, bien sûr :

ℓ_{i} : τ_{i}^{i∈1..n}, \underline{∅} = [ℓ_{i} : τ_{i}^{i∈1..n}, ℓ : ∅, \underline{∅}] [ℓ_{i} : τ_{i}^{i∈1..n}, \underline{Either}] = [ℓ_{i} : τ_{i}^{i∈1..n}, ℓ : Either, \underline{Either}]

Préciser les nouvelles relations de sous-typage, les schémas de types pour les nouvelles primitives. Montrer la correction de cette extension vis à vis de l’évaluation.

Une relation encore plus fine permet de préciser exactement sur quels champs l’inclusion a dû être utilisée :

τ ::= … | Maybe τ | Pre^{+} τ

                                               Either

[figure]

                                                      Pre^{+} τ

[figure: ^{·····}; ·····]

                                       Maybe τ  Pre^{+} τ′

\begin{matrix} \\ | \\ | \end{matrix}
[figure: |]

                                  ∅  Pre τ  Pre τ′

On pourra remarquer que dans l’exemple ci-dessus le constructeur Pre est invariant.

De tels raffinement permettent de typer les programmes plus précisément, mais parfois aussi de typer plus de programmes, notemment dans les langages à objets.

Conclusion

Dans ce chapitre, nous avons introduit une relation d’inclusion sur les types. Nous avons d’abord montré comment elle permet de mieux typer les enregistrement. Mais une application essentielle de la relation d’inclusion est de pouvoir coercer implicitement les objets qui sont dans une relation de sous-typage, comme nous le verrons brièvement dans le chapitre ??.

Nous avons introduit le formalisme des types contraints qui permet d’ajouter naturellement une relation de sous-typage au système de typage de ML, tout en préservant la correction du typage vis à vis du calcul.

Comme nous l’avons déjà plusieurs fois rappelé, le formalisme des types contraints est récent et de nombreux aspects sont encore du domaine de la recherche. La simplification des contraintes est un de ces aspects, et dans la messue où des algorithmes efficaces de simplification des contraintes existent, le système de typage avec contraintes pourrait peut-être remplacer avantageusement le système de typage de ML.

Pour en savoir plus

Le formalisme des types contraints que nous utilisons ici a été introduit par Pavel Curtis [?], puis repris par A. Aiken [?] dans un cadre plus général. Une présentation plus récente, et plus proche du formalisme présenté ici a été réintroduite dans [?, ?] pour y être appliquée à des langages à objets. Pour une étude de la simplification des contraintes, on pourra aussi lire [?].

Solutions des exercices

Exercice 37, page 62

Une dérivation du jugement est

(f : τ_{1} → τ_{2}, x : τ′_{1}) ⊢ f : τ_{1} → τ_{2} (f : τ_{1} → τ_{2}, x : τ′_{1}) ⊢ x : τ′_{1} τ′_{1} <: τ_{1} ; \overline{(Sub)} ; (f : τ_{1} → τ_{2}, x : τ′_{1}) ⊢ x : τ_{1} ; \overline{(App)} ; (f : τ_{1} → τ_{2}, x : τ′_{1}) ⊢ f x : τ_{2} ; ·· τ_{2} <: τ′_{2} (Sub)

(f : τ_{1} → τ_{2}, x : τ′_{1}) ⊢ f x : τ′_{2} (Fun)

⊢ apply: (τ_{1} → τ_{2}) → τ′_{1} → τ′_{2}

La fonction apply se comporte comme l’identité : elle ne calcul rien, et se contente de changer le type de ses arguments. On dit que c’est une fonction de retypage. On peut utiliser une telle fonction pour effectuer des coercions de types explicites. Le typage de apply justifie la relation de sous-typage de la flèche, car il montre qu’on peut remplacer les occurrences de la règle Sub sur les flèches par coercions explicites (en ajoutant des applications de la constante apply).

Exercice 38, page 62

Le type α → {ℓ : Pre α; ∅} donné par ML (sans utilisation de la règle de sous-typage) est bien sûr un type correct. Nous pouvons en déduire d’autres en appliquant la règle de sous-typage seulement à la fin. En propageant l’inclusion par la règle structurelle pour les types fonctionnels, cette fonction a donc aussi le type τ → τ′ pourvu que τ <: α et {ℓ : Pre α; ∅} <: τ′. Par exemple, on peut prendre τ′ égal à {∅} et τ quelconque. Mais on peut aussi prendre τ′ égal à {ℓ : Pre τ; ∅} et τ quelconque. Toutes ces solutions sont incompatibles. Donc il n’y a pas de type principal.

Nous pouvons aussi prendre des instances du type ML, par exemple, en remplaçant α par {x : Pre I; ∅}. Il est alors possible de choisir {x : Pre I; y : Pre I; ∅} pour τ et le type enregistrement vide pour τ′. Enfin, il faut aussi envisager d’appliquer également la relation de sous-typage à l’intérieur de la dérivation (mais pour cet exemple, nous n’obtiendrions pas plus de typages).

Nous aimerions dire que la fonction a le type principal α → {ℓ : Pre (α′); ∅} tel que α <: α′. Mais cette expression n’est pas un type.

Exercice 39, page 62

Dans le premier exemple, on peut considérer que (α → α) → α → α est un type principal. En effet tous les autres types possibles de la fonctions, qui sont (τ_{1} → τ′_{1}) → τ_{2} → τ′_{2} tels que τ_{2} <: τ_{1} et τ′_{1} <: τ′_{2}, peuvent se déduire du premier par instantiation et par l’application de la règle Sub.

Ce n’est plus le cas pour le second exemple. Les types possibles sont de la forme (τ_{1} → τ′_{1}) → (τ_{2} → t′_{2}) → τ → (τ′_{1} × τ′_{2}) tels que

τ <: τ_{1}  τ <: τ_{2}  τ′_{1} <: τ  τ′_{2} <: τ

Ils ne peuvent pas se déduire des types ML (τ → τ) → (τ → τ) → τ → τ → (τ × τ) simplement par application d’une relation de sous-typage.

Exercice 40, page 64

C’est une simple induction sur la structure de τ qui repose sur le fait que deux termes de même structure sont dans une relation de sous-typage si leurs sous-termes immédiats sont aussi dans une relation de sous-typage (directe ou inverse pour les positions contravariantes).

Exercice 41, page 64

Par exemple, on peut prendre la substitution α ↦ α′. En appliquant cette substitution, partout dans la dérivation nous conservons une dérivation valide et dans laquelle les relations de sous-typage sont sans hypothèses. D’autres substitutions sont bien entendu possibles, mais le raisonnement restant le même ; elles correspondent à d’autres dérivations sans hypothèses de sous-typage.

Exercice 42, page 66

Dans le premier cas, il suffit de voir que l’ensemble est fermé et immédiatement cohérence. Une solution est ⊥ → ⊥ for α.

Dans le second cas, ni ⊥ ni ⊤ ne sont solutions. Une solution est donc une flèche. Cependant en remplaçant α par α_{1} → α_{2}, on obtient après fermeture les contraintes {α_{1} → α_{2} <: α_{1}} et α_{1} <: α_{1} → α_{2} qui ne sont pas simulatément solvables.

Exercice 43, page 68

Une instance de α satisfaisant C est ⊥ ou bien de la forme ⊤ → τ′ telle que τ′ est une instance de α′ satisfaisant C. Par symmétrie, une instance de α′ satisfaisant C est ⊤ ou bien de la forme ⊤ → τ telle que τ est une instance de α′ satisfaisant C. On en déduit la forme générale des instances τ et τ′ de α et α′ satisfaisant C.

\begin{matrix}τ_{n} ::= & ⊥ | ⊤ → τ_{n−1} | rec α.(⊤ → α) \\ τ′_{n} ::= & ⊤ | ⊥ → τ′_{n−1} | rec α.(⊥ → α) \end{matrix}

De plus, les τ_{i} forment une suite croissante de limite rec α.(⊤ → α). Inversement, les τ′_{i} formeent une suite décroissante de limite rec α.(⊥ → α). De plus rec α.⊤ → α <: rec α.⊥ → α. Donc on a bien τ <: τ′ pour toute solutions α ↦ τ, α′ ↦ τ′) de C.

Montrons C ⊢ α <: α′ n’est pas possible. Une dérivation de la forme C ⊢ α <: τ′′ ne peut se terminer que par une règle Context ou un règle Trans. Cependant dans le dernier cas, une premisse doit se terminer par une règle Context dérivant un jugement de la même forme. Or étant donné la forme de C, il n’est pas possible de dériver un jugement de la forme C ⊢ α <: τ′′.

Exercice 44, page 70

Il suffit d’appliquer les règles de typage de l’application et des fonctions. La seule contrainte Int <: (τ → τ) → Int suffit.

Par analyse des dérivations possibles, on peut montrer que l’ensemble de contraintes comportera au moins la contrainte Int <: τ → τ′ et ne peut donc pas être cohérent (règle C-Arrow).

Exercice 47, page 78

L’extension polymorphe des enregistrements n’est pas typable de façon aussi polymorphe. Le programme suivant n’est pas typable avec le sous-typage sans variables de rangées.

    let extend r x = r || {a = x} in extend (extend {b = 2} 1) true;;

Inversement, sans le sous typage, on en peut oublier la présence des champs. Le programme suivant n’est pas typable sans inclusion.

    if true then {a = 1} else {a = 1; b =2};;

Il faut modifier la règle <:-Record en

(<:-Record) ; \frac{C ⊢ τ_{i} <: τ′_{i} ∀i ∈ 0..n}{C ⊢ \{ℓ_{i} : τ_{i}^{i∈1..n}; τ_{0}\} <: \{ℓ_{i} : τ′_{i}^{i∈1..n}; τ_{0}\}}

Cela nous aménera aussi à modifier les règles de propagation et de cohérence : Il faut modifier la règle de propagation :

{ℓ_{i} : τ_{i}^{i∈1..n}; τ_{0}} <:_{C} {ℓ_{i} : τ′_{i}^{i∈1..n}; τ′_{0}} ⟹ τ_{i} <:_{C} τ′_{i}, ∀i ∈ 0..n (P-Record)

Le reste du formalisme est inchangé. Toutes les propriétés restent vraies (mais il faut le vérifier).