44

Chapitre 4

Les enregistrements polymorphes

Dans ce chapitre nous nous intéressons à l’extension du langage ML avec des enregistrements. Les enregistrements sont des produits à champs nommés. Après avoir expliquer brièvement comment ajouter des enregistrements déclarés à ML, puis justifié la nécessité d’ajouter des opérations plus puissantes sur les enregistrements, nous découvrons le principe du typage des enregistrements extensibles, que nous formaliserons ensuite complètement.

4.1 Des enregistrements déclarés aux enregistrements extensibles

Les enregistrements déclarés sont des produits à champs nommés. Comme pour les types concrets, nous pouvons les formaliser de deux façons différentes. Nous pouvons les considérer comme une extension du formalisme, ou bien comme une application du cas général pour un choix particulier des constantes du langage.

Exercice 28 Formaliser l’ajout d’un seul enregistrement pré-défini et correspondant à la déclaration de type suivante (en Caml) :

    type ('a, 'b) pair = {fst : 'a; snd : 'b}

Dans la définition de type de l’exercice ci-dessus, nous disons que les identificateurs fst et snd sont les étiquettes de l’enregistrement. Outre le caractère obligatoire des déclarations de types un inconvénient majeur est qu’une étiquette ne peut pas être utilisée dans plusieurs enregistrements à la fois. Pour que la fonction f égale à fun

(x) x.ℓ soit définie, il est nécessaire qu’un type enregistrement ait été préalablement défini avec l’étiquette ℓ. La fonction f est typable, mais ne peut s’appliquer qu’aux enregistrements de ce type. L’extraction de champ est donc une opération monomorphe.

Une première extension consiste à rendre primitives les constructions d’enregistrements de façon à se passer des déclarations de types. On se donne un ensemble dénombrable d’étiquettes L que nous désignerons par la lettre ℓ. Nous ajoutons au langage les expressions suivantes :

a ::= … | {ℓ_{1} = a_{1}; … ℓ_{n} = a_{n}} | a.ℓ

Mais, les enregistrements ne sont dits polymorphes ou flexibles que s’il est possible également de définir une fonction d’accès polymorphe fun (x) x.ℓ. Par exemple, les enregistrements de Sml-nj [?] bien que non déclarés ne sont pas polymorphes.

Dans la plupart des langages, les enregistrements ne peuvent être construits qu’en une seule étape. C’est-à-dire qu’il n’est pas possible d’étendre un enregistrement déjà construit avec une nouvelle étiquette. On dit que les enregistrements sont extensibles lorsqu’il est possible de définir une fonction fun (r v) r @ {ℓ = v} permettant d’étendre un enregistrement arbitraire r sur le champ ℓ avec une valeur v. Il est alors possible de construire les enregistrements à partir de l’enregistrement vide par ajout successifs de champs.

Nous étudions maintenant un langage avec enregistrements polymorphes et extensibles. La solution la plus simple est toujours d’essayer de considérer les enregistrements extensibles comme un cas particulier du cas général. Nous essayons donc de ne pas ajouter d’expressions au langage mais simplement des familles de constantes :

• un constructeur {ℓ_{1} = , … ℓ_{n} = } d’arité n pour tous les tuples d’étiquettes deux à deux disjointes ;

• une primitive ( .ℓ) d’arité 1 pour chaque étiquette ℓ dans L;

• une primitive ( @ {ℓ = }) d’arité 2 pour chaque étiquette ℓ dans L.

Nous ajoutons les règles de réduction suivantes :

\begin{matrix}\{ℓ_{i} = v_{i}^{i∈I}\}.ℓ_{j} & ⟶^{ϵ} v_{j} & (j ∈ I) \\ \{ℓ_{i} = v_{i}^{i∈I}\} @ \{ℓ_{j} = v_{j}\} & ⟶^{ϵ} \{l_{i} = v_{i}^{i∈I∪\{j\}}\} & (j ∉ I) \\ \{ℓ_{i} = v_{i}^{i∈1..n}\} @ \{ℓ_{j} = w_{j}\} & ⟶^{ϵ} \{ℓ_{j} = w_{j}, l_{i} = v_{i}^{j∈I\\{j\}}\} & (j ∈ I) \end{matrix}

L’ajout d’un champ à un enregistrement peut se faire même si ce champ était déjà présent : on dit que l’extension est libre. Si l’on retire la dernière règle, cela n’est plus possible, et on dit que l’extension des enregistrements est stricte.

Exercice 29 (***) Plutôt que d’ajouter des valeurs enregistrements, on aurait pu se contenter d’un enregistrement vide {} et considérer les expressions v_{1} @ {ℓ = v_{2}} comme des valeurs, c’est-à-dire ( @ {ℓ = }) comme un constructeur. Suivre cette approche, et définir les règles de réduction. Les deux approches sont elles équivalentes (on n’en fera pas la preuve formelle, mais on essayera d’indiquer précisément en quel sens, et éventuellement les étapes de la preuve) ?

Nous pourrions considérer les valeurs enregistrements égales par permutation de champs, mais cela nous ferait sortir du formalisme des constantes. Ou bien, ayant fixé un ordre sur les étiquettes, nous pourrions nous restreindre à des primitives {ℓ_{1} = , … ℓ_{k} : }.

4.2 Principe du typage des enregistrements extensibles

Par opposition avec le typage des objets mutables, la difficulté n’est pas sémantique, mais purement syntaxique : comment étendre le système de typage pour assurer le polymorphisme désiré ? La première difficulté provient de la fonction d’accès fun (r) r.ℓ que l’on veut polymorphe, c’est-à-dire que l’on veut pouvoir l’appliquer à des enregistrements ayant au moins le champ ℓ mais pouvant également définir un ensemble arbitraire d’autres champs.

Pour simplifier, considérons le cas où les enregistrements sont construits à partir de deux étiquettes ℓ_{1} et ℓ_{2}. Nous pouvons alors décrire un enregistrement en décrivant chaque champ séparément. Par exemple, soit x et y les valeurs {ℓ_{1} = 1} et {ℓ_{1} = true; ℓ_{2} = 2}. Nous pouvons dire que l’enregistrement x est défini sur le champ ℓ_{1} avec une valeur entière et indéfini sur le champ ℓ_{2}, et que y est défini sur le champ ℓ_{1} avec une valeur booléenne et défini sur le champ ℓ_{2} avec une valeur entière. Nous pouvons décrire cette information explicitement par le type suivante :

x : {ℓ_{1} : Pre (Int); ℓ_{2} : ∅} y : {ℓ_{1} : Pre (Bool); ℓ_{2} : Pre (Int)}

La fonction d’extraction f égale à fun (r) r.ℓ prend en argument un enregistrement dont le champ ℓ_{1} est défini avec une valeur de type τ retournée en résultat et dont le champ ℓ_{2} est soit défini, soit indéfini ; ainsi, nous pouvons dire que son type est une instance de {ℓ_{1} : Pre α_{1}; ℓ_{2} : α_{2}} → α_{1}, puisque α_{2} peut alors être remplacé soit par Pre τ, soit par ∅. S’il y avait trois étiquettes, les types des valeurs précédentes seraient :

x : {ℓ_{1} : Pre (Int); ℓ_{2} : ∅; ℓ_{3} : ∅}
y : {ℓ_{1} : Pre (Bool); ℓ_{2} : Pre (Int); ℓ_{3} : ∅}
f : {ℓ_{1} : Pre (α_{1}); ℓ_{2} : α_{2}; ℓ_{3} : α_{3}} → α_{1}

Il est immédiat d’imaginer ce que deviendrait les types ci-dessus s’il y avait une quatrième étiquette : puisque les étiquettes ℓ_{3} et ℓ_{4} n’apparaissent pas dans le programme, elles se comportent de la même façon, leurs types doivent donc être isomorphes. Le problème est en fait que nous ne connaissons pas par avance l’ensemble des étiquettes qui seront utilisées dans le reste du programme. En utilisant la remarque précédente, il nous suffit de donner un modèle pour les champs qui ne sont pas explicitement cités, de façon à pouvoir en prendre des instances au besoin. Le type des valeurs ci-dessus deviendra :

x : \{ℓ_{1} : Pre (Int); ℓ_{2} : ∅; \underline{∅}\}
y : \{ℓ_{1} : Pre (Bool); ℓ_{2} : Pre (Int); \underline{∅}\}
f : \{ℓ_{1} : Pre (α_{1}); ℓ_{2} : α_{2}; \underline{α}\} → α_{1}

Les expressions soulignées ne sont pas attachées à des étiquettes particulières, mais elles décrivent, pour l’enregistrement dans lequel elles apparaissent, les types possibles pour les champs qui ne figurent pas explicitement à leur gauche. Ce sont, en quelque sorte, des modèles pour les champs implicites et les types de ces champs sont des instances du modèle. En fait, il faut lire \{ℓ_{1} : τ_{1}; ℓ_{2} : τ_{2}; \underline{τ_{3}}\} comme \{ℓ_{1} : τ_{1}; (ℓ_{2} : τ_{2}; \underline{τ_{3}})\}. À partir du type \{ℓ_{1} : Pre (Int); (ℓ_{2} : ∅; \underline{∅})\}, nous devons pouvoir obtenir le type \{ℓ_{1} : Pre (Int); (ℓ_{2} : ∅; (ℓ_{3} : ∅; \underline{∅}))\}. Pour cela, il suffit de considérer les enregistrements modulo la famille d’équations

\underline{∅} = (ℓ : ∅; \underline{∅})  ∀ℓ ∈ L

Le type \{ℓ_{1} : Pre (α_{1}); (ℓ_{2} : α_{2}; (ℓ_{3}; α_{3}; \underline{α′}))\} → α_{1} doit aussi pouvoir être considéré comme un type de f. Celui-ci est simplement obtenu par substitution de la variable \underline{α} dans le type de f par (ℓ_{3} : α_{3}; \underline{α′}). La variable \underline{α} est aussi appelée une variable de rangée. Enfin, il faut ajouter la famille d’équations

(ℓ_{1} : α_{1}; (ℓ_{2}; α_{2}; \underline{α})) = (ℓ_{2} : α_{2}; (ℓ_{1} : α_{1}; \underline{α}))  ∀ℓ_{1}, ℓ_{2} ∈ L

pour exprimer que l’ordre dans lequel apparaissent les champs dans un type enregistrement n’a pas d’importance.

Jusqu’à présent, nous avons ignoré le fait que les expressions Pre et ∅ ne désignent pas des types, mais des modèles de types. Certaines expressions, par exemple, Pre→ ∅(τ) ou \{\underline{\{∅\}}\} n’ont pas de sens, pas plus que \{l_{1} : τ_{1}; ℓ_{1} : τ_{2}; \underline{∅}\} ou encore \{ℓ : \underline{α}; \underline{α}\}. Pour éliminer ces types indésirables, nous utilisons des sortes. Les sortes sont aux types ce que les types sont aux termes de ML : ils permettent, par un mécanisme similaire au typage, d’éliminer parmi tous les types certains types considérés comme mal formés. Cette élimination se fait en deux étapes.

Premièrement, nous considérons deux sortes Type et Field, et nous imposons la signature (Σ_{1}) aux symboles de type :

                     ( → ) :: Type ⊗ Type ⇒ Type
                        { } :: Field ⇒ Type
                     Pre ( ) :: Type ⇒ Field
                          ∅ :: Field
                     (ℓ : ; ) :: Field ⊗ Field ⇒ Field

Les types Pre→ ∅(τ) et {∅} ne peuvent plus être écrits, car ils ne respectent pas les contraintes de sortes. Les types de tous les exemples qui précèdent sont heureusement bien formés pour Σ_{1}. Mais, il est encore possible d’écrire {ℓ_{1} : τ_{1}; ℓ_{1} : τ_{2}; ∅}.

Exercice 30 Parmi les quatre exemples décrit une quinzaine de lignes ci-dessus, quels sont ceux que l’on ne peut plus écrire ? Comment éliminer les autres ?

Puis, nous filtrons à nouveau les expressions de types par une seconde signature. Nous considérons les sortes Type et la collection de sortes Row (L) où L varie dans l’ensemble des parties finies de l’ensemble des étiquettes. Cette fois-ci, l’idée est de séparer une expression de type ordinaire, de la sorte Type, d’une expression de rangée, de la sorte Row (L), l’ensemble L décrivant les étiquettes ne devant pas être redéfinies.

La signature des symboles de types est (Σ_{2}) :

             ( → ) :: Type ⊗ Type ⇒ Type

{ } :: Row (∅) ⇒ Type

             Pre ( ) :: Type ⇒ Type

∅ :: κ
(ℓ : ; ) :: Type ⊗ Row ({ℓ} ∪ L) ⇒ Row (L) (ℓ ∉ L)

La variable κ est une variable de sorte. Cela signifie que ∅ a toutes les sortes. Les symboles ∅ et (ℓ : ; ) ont donc plusieurs sortes. En fait, il est possible de les indicer par leur sorte de façon à se ramener à des symboles mono-sortés. Dans le formalisme, il est plus simple de considérer les termes mono-sortés, mais en pratique, nous n’écrirons pas les indices des symboles. Étant donné la sorte d’un terme, il existe au plus une façon de l’annoter (c’est-à-dire d’indicer ses symboles de types par des sortes) de telle façon que le terme soit bien formé et de cette sorte. Il existe un algorithme qui décide si un terme est bien formé, et le cas échéant annote ses sous-termes par les sortes.

Les expressions de types bien formées sont celles qui respectent à la fois la signature Σ_{1} et la signature Σ_{2}. Il est essentiel de vérifier que les deux familles d’équations sont bien sortées, c’est-à-dire que les membres gauches et droits de chacune des équations admettent simultanément les même sortes.

Exercice 31 (***) Écrire un algorithme de synthèse de sortes. Indications : on pourra ajouter des variables de sortes au langage des sortes, puis s’inspirer de l’algorithme d’unification donné ci-dessous. Dans un premier temps on pourra chercher un semialgorithme qui termine sur toutes les expressions de type bien formées, puis obtenir un algorithme par une petite modification simple permettant de détecter les cas de non terminaison du semi-algorithme.

Exercice 32 (**) Pour chaque expression de type τ possiblement mal formée pour Σ_{2} on définit un type τ̄ obtenu en remplaçant successivement :

1. toute variable de rangée α par un préfixe de la forme {ℓ_{1} : α_{1}, … ℓ_{k} : α_{k}; α_{0}} où les ℓ_{i} sont toutes les étiquettes figurant sur un chemin quelconque dans τ menant à α et les α_{i} sont des variables fraiches et disctinctes deux à deux.

2. tout terme ℓ : τ; τ′ par τ′ pour chaque orrurence de ℓ : τ; τ′ au bout d’un chemin contenant ℓ.

Vérifier que τ̄ est égal à τ si τ est bien formé pour Σ_{2}. À partir de la synthèse de sortes, en déduire un algorithme qui accepte une expression de type τ possiblement mal formée pour Σ_{2} et retourne τ̄ si τ̄ est bien formée, ou signale une erreur sinon.

Par exemple, l’expression de type associée à {ℓ_{1} : τ_{1}; ℓ_{1} : τ_{2}; ∅} est {ℓ_{1} : τ_{1}; ∅}. Celle associée à {τ} → {ℓ : τ_{0}; τ} est {ℓ : α_{1}; τ} → {ℓ : τ_{0}; τ}. Par contre, il n’y a pas d’expression de type associée à τ → {ℓ : τ_{0}; τ}, car τ ne peut pas être à la fois de la sorte Type et Row (L).

Les règles de typage des enregistrements peuvent être traitées comme l’ajout de constantes avec l’environnement initial suivant :

{(ℓ_{i} = )^{i∈1..n}} :  α_{1} → … α_{n} → {(ℓ_{i} = Pre α_{i})^{i∈1..n}; ∅}  (Record)
( .ℓ) :  {ℓ : Pre α; α′}) → α  (Dot)
( @ {ℓ = } :  {ℓ : α_{1}; α} → α_{2} → {ℓ : Pre α_{2}; α}  (With)

Il est quand même nécessaire de refaire l’étude des propriétés du typage car en considérant les types modulo une théorie équationnelle, nous avons changé l’algèbre des types. La formalisation des types enregistrements par des algèbres d’enregistrements permet de ramener le typage des enregistrements au typage dans ML, modulo une théorie équationnelle simple. Il suffira alors de généraliser les preuves faites pour le noyau ML au cas où les types sont considérés modulo une théorie équationnelle.

4.3 Algèbres d’enregistrements

Pour avoir une présentation plus générale et plus complète des types enregistrements, on pourra se reporter à [?, ?]. Il y est montré que les types enregistrements sont les termes d’une algèbre avec sortes engendrées par des théories équationnelles particulières, que ces théories équationnelles sont syntaxiques, et que le problème de l’unification y est décidable.

L’algèbre des types enregistrements est syntaxique ; cela signifie que l’unification de deux termes peut toujours se ramener à un problème d’unification entre leurs sous-termes en n’examinant les arguments que jusqu’à une profondeur bornée. Concrètement, les théories équationnelles syntaxiques sont celles pour lesquels l’agorithme d’unification peut s’écrire comme une extension naturelle de l’agorithme dans le cas non équationnel. Nous donnons ci-dessous un algorithme d’unification des types enregistrements :

    let rec unify =
      fun α τ →
         if α ∈ V(τ) then fail else [τ/α]

| g(τ_{i})_{i∈1..n} g(τ′_{i})_{i∈1..n} →

         let φ_{0} = unify τ_{0} τ′_{0} in

let φ_{1} = unify φ_{0}(τ_{1}) φ_{0}(τ′_{1}) in

         ...

let φ_{n} = unify φ_{n−1}(τ_{n}) φ_{n−1}(τ′_{n}) in φ_{n}

| (ℓ_{1} : τ_{1}; τ′_{1}) (ℓ_{2} : τ_{2}; τ′_{2}) →

         let α = new var() in

let φ_{0} = unify τ′_{1} (ℓ_{2} : τ_{2}; α) in

let φ_{1} = unify φ_{0}(τ′_{2}) φ_{0}(ℓ_{1} : τ_{1}; α) in

φ_{1}

| ∅ (ℓ : τ_{1}; τ_{2}) →

         let φ_{0} = unify ∅ τ_{1} in
         let φ_{1} = unify ∅ φ_{0}(τ_{2}) in

φ_{1}

| (ℓ : τ_{1}; τ_{2}) ∅ →

unify ∅ (ℓ : τ_{1}; τ_{2})

| τ α →

         unify α τ

        | → fail

4.4 Synthèse de type

Le problème de la synthèse de types avec enregistrements extensibles se ramène alors à celui plus général de la synthèse de types lorsque les types sont considérés modulo une théorie équationelle pour laquelle le problème d’unification est décidable et unitaire. Les propriétés de la synthèse de types pour ML sont conservées sous certaines conditions très simples : il suffit que la théorie équationnnelle soit régulière, c’est-à-dire que les termes égaux aient toujours le même ensemble de variables libres ; que l’unification y soit décidable, et unitaire (c’est-à-dire qu’il existe un unificateur principal pour les problèmes d’unifications solvables). L’algorithme de synthèse de types est alors obtenu en remplaçant l’algorithme d’unification de ML par celui de la théorie équationelle considérée.

4.5 Correction de la sémantique

L’approche la plus naturelle consiste à reprendre tout le formalisme des chapitres 1 et 2, et l’étendre au cas où les types sont condidérés modulo une théorie équationnelle régulière, pour laquelle le problème d’unification est décidable et unitaire. En particulier, les propriétés 1, 2 et 3, page 13 sont conservées, ainsi que les résultats du chapitre 2.

Le cas des enregistrements peut ensuite être traité comme ajouts de primitives. Nous devons alors vérifier que les règles de réduction et les schémas de type des primitives donnés ci-dessus sont compatibles, dans le sens où les hypothèses H1 et H2 du chapitre 2 sont satisfaites.

\underline{Preuve} : [de H1] Nous devons considérer les cas suivants :

52 CHAPITRE 4. LES ENREGISTREMENTS POLYMORPHES

Cas a est {ℓ_{i} : v_{i}^{i∈1..n}}.ℓ_{j} : où j est dans 1..n. Alors une preuve du typage A ⊢ a : τ impose que A ⊢ v_{i} : τ_{i} pour i dans 1..n d’une part, et que τ soit égal à τ_{j} d’autre part. On a donc en particulier A ⊢ v_{j} : τ.

Cas a est {ℓ_{i} : v_{i}^{i∈1..n}}||{ℓ_{j} = v′_{j}}: . Alors une preuve du typage A ⊢ a : τ impose que A ⊢ v_{i} : τ_{i} pour i dans 1..n d’une part, et que A ⊢ v′_{j} : τ′_{j} d’autre part. Nous distinguons deux cas : si j est dans 1..n, alors le réduit a′ de a est {ℓ_{i} : v_{i}^{i≠j∈1..n}; l_{j} = v′_{j}} et a pour type {ℓ_{i} : Pre τ_{i}^{i≠j∈1..n}; l_{j} = τ′_{j}}. Sinon, le réduit de a est {ℓ_{i} : v_{i}^{i∈1..n}; l_{j} = v′_{j}} et a pour type {ℓ_{i} : Pre τ_{i}^{i∈1..n}; l_{j} = τ′_{j}}. Dans les deux cas a′ possède le type τ dans l’environnement A.

\underline{Preuve} : [de H2] Nous raisonnons de la façon habituelle. Considérons un jugement A ⊢ v : τ. Alors :

• Si v est une fonction ou bien une constante fonctionnelle partiellement appliquée, alors τ est un type fonctionnel,

• Si v est un enregistrement, alors τ est un type enregistrement. De plus si v possède le champ ℓ, alors τ associe le type Pre τ′ sur le champ ℓ.

L’égalité conserve toujours le constructeur de tête sur les types de la sorte Type, et préserve également la présence des champs. Les types engendrés par les différents cas ne peuvent donc pas se superposer. Les cas ci-dessus traitent tous les cas de valeurs. Nous pouvons donc inverser la propriété :

• Si τ est un type fonctionnel, alors v est une fonction ou bien une constante fonctionnelle partiellement appliquée,

• Si τ est un type enregistrement, alors v est un enregistrement. De plus si τ associe le type Pre τ′ au champ ℓ, alors v possède le champ ℓ.

Nous pouvons maintenant montrer la seconde propriété en considérant les cas suivants de programmes irréductibles :

Cas a est v.ℓ: Une preuve du typage A ⊢ a : τ impose que A ⊢ v : {ℓ : pre τ′; τ′′}. Donc v est un enregistrement possédant le champ ℓ, et a peut se réduire.

Cas a est v @ ℓ = v′: Une preuve du typage A ⊢ a : τ impose que A ⊢ v : {ℓ : τ′; τ′′}. Donc v est un enregistrement, et a peut se réduire.

4.6 Les variantes

Les types concrets sont des sommes déclarées. Les sommes polymorphes, encore appelées variantes sont donc aux types concrets ce que sont les enregistrements polymorphes aux enregistrementgs déclarés. Ainsi, l’idée est de pouvoir définir ou filtrer des objets construits sans devoir déclarer leur structure au préalable. Par exemple, on voudrait écrire :

    let x = Cons (1, Nil) and let hd Cons (h,t) = h in hd x;;

Les variantes peuvent être formalisées par ajout de constantes : la primitive inject_{ℓ}, d’arité 1, crée une variante avec l’étiquette ℓ; la primitive (fun ℓ_{1} ⇒ | … ℓ_{n} ⇒ ) d’arité n, filtre des variantes selon l’étiquette ℓ_{i} avec laquelle elle a été construite. Par exemple, le programme ci-dessus pourra s’écrire :

    let x = inject Cons (1, inject Nil())
    and let hd = fun Cons (h,t) → h in hd x;;

La sémantique opérationelle est définie par la famille de δ-règles suivantes :

(fun ℓ_{i} ⇒ v_{i}^{i∈I}) (inject ℓ_{j} v) ⟶^{ϵ} v_{i} v  (j ∈ I)

(On écrit aussi fun ℓ_{i} x_{i} ⇒ a_{i}^{i∈1..i}n lorsque les v_{i} sont des fonctions fun (x_{i}) a_{i}).

Les variantes sont parfois considérées comme duales des enregistrements. En effet, on peut définir une traduction [[ ]] des programmes avec variantes vers les programmes avec enregistrements de la façon suivante : la primitive inject_{ℓ} est traduite par fun (x y) y.ℓ x. Le filtrage (fun ℓ_{i} ⇒ a_{i}^{i∈1..n}) est traduit par fun (x) x {ℓ_{i} = a_{i}}. Les autres constructions sont traduites de façon homomorphe.

Exercice 33 Montrer que si a_{1} ⟶ a_{2}, alors [[a_{1}]] ⟶^{∗} [[a_{2}]].

Cette vision est souvent fructueuse, mais elle est aussi trompeuse. En particulier, l’usage des variantes est très différent de celui des enregistrements. Par exemple, il est naturel d’étendre les variantes avec une action par défaut qui sera appliquée lorsque la variante filtrée est construite avec une étiquette non explicite dans le filtre. La contrepartie de cette construction dans les enregistrements extensibles serait la possibilité de définir des enregistrements avec une valeur par défaut, qui sera retournée comme la projection de l’enregistrement sur un champ qui n’a pas été explicitement défini.

Nous pourrions typer les variantes en “remontant” le typage de leur traduction en objets enregistrements.

Exercice 34 Essayer cette méthode. Pourquoi n’est-elle pas satisfaisante ?

Nous utilisons plutôt une méthode directe, tout en nous inspirant du typage des enregistrements. Nous notons [τ] le type des variantes décrites par un type de rangé τ (donc de la sorte Row (∅). Nous affectons aux primitives les schémas de type suivants :

inject_{ℓ}: α → [ℓ : Pre α; α′]
fun ℓ_{1} ⇒ | … ℓ_{n} ⇒ : (α_{1} → α) → … (α_{n} → α) →
[ℓ_{1} : Pre (α_{1}); … ℓ_{n} : Pre (α_{n}); ∅] → α

Dans les types de variantes, les expressions de type Pre τ et ∅ prennent un sens opposé à celui qu’elles ont dans les types d’enregistrements. Le type [ℓ_{1} : Pre τ_{1}; ℓ_{2} : Pre τ_{2}; α] est celui d’une variante qui est peut-être construite sur l’étiquette ℓ_{1} avec une valeur de type τ_{1} ou sur l’étiquette ℓ_{2} avec une valeur de type τ_{2}. Un objet construit par (inject_{ℓ_{1}} v) a donc un type de la forme [ℓ_{1} : Pre τ_{1}; α] où τ est le type de v. En particulier, il est possible de substituer la variable α, par exemple par (ℓ_{2} : Pre τ_{2}; α′) et retrouver un type comme celui ci-dessus ; cela est nécessaire lorsque une variante peut provenir, par exemple de deux branches différences d’une conditionelle, et a donc pu être construit soit avec ℓ_{1} soit avec ℓ_{2}, sans qu’il soit possible de le déterminer statiquement. Inversement, si le type ∅ est associé à une étiquette ℓ dans un type de variante τ, alors on sait qu’une variante de type τ n’a pas pu être construite avec l’étiquette ℓ. Par exemple, la construction de filtrage des variantes exige que l’objet filtré ait un type variante fermé, c’est-à-dire que les champs non explicitement mentionnés aient le type ∅, ce qui garantit la réussite du filtrage.

Exercice 35 Montrer la correction du typage vis à vis de la sémantique pour les objets variantes.

Exercice 36 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}. Donner les nouvelles règles de réduction. Quels schémas de type faut-il associer aux primitives. Montrer la correction du typage.

Conclusion

Dans ce chapitre nous avons montré comment étendre le langage ML avec des types enregistrements extensibles. Nous avons introduit les algèbres d’enregistrements, un formalisme général qui permet de traiter uniformément plusieurs variantes d’enregistrements. Nous n’avons pas décrit l’opération de concaténation sur les types enregistrements. Cette construction pose encore des problèmes de typage. Toutefois, dans de nombreux cas pratiques on peut ramener le problème de la concaténation à celui de l’extension [?]. Les variantes peuvent également être ajoutées à ML, de façon duale. Toutefois, elles sont d’un usage moins fréquent, sans doute parce leur aspect “ouvert”, c’est-à-dire la possibilité d’être mélangées entre elles de façon arbitraire, n’est pas très satisfaisante.

Pour en savoir plus

Il existe d’autres approches au typage des enregistrements. Celle utilisant des types étiquettés [?] est très similaire. Une autre apporche intéressante, traitant le cas des enregistrements flexibles, mais pas celui des enregistrements extensibles repose sur l’utilisation de sortes sur les variables de type ordinaire [Oho90]. Enfin, nous verrons dans le chapitre suivant comment l’ajout de sous-typage permet également et de façon plus élégante de traiter le cas des enregistrements flexibles. Dans un cadre de typage explicite, on peut trouver plusieurs solutions utilisant également une relation de soustypage. Par exemple, on pourra regarder [?, ?].

Appendix : Simulation des enregistrements extensibles

Cette annexe décrit comment simuler les enregistrements extensibles en ML. Cela suppose que l’on connaisse à l’avance toutes les étiquettes utilisées dans tout le programme. Nous l’illustrons sur un exemple en considérant trois champs a, b et c. Les enregistrements extensibles seront simplement représentés par un enregistrement rigides à trois champs, certains étant marqués “absents”.

    type ('a, 'b, 'c) abc = {a:'a; b:'b; c:'c};;

Nous voulons garantir par le typage que l’accès à un champ autorisé réussit toujours. Nous utilisons deux types incompatibles pour représenter les champs présents et les champs absents :

    type 'a pre = Pre of 'a;;
    type abs = Abs;;

L’enregistrement vide est simplement

    let nul = {a = Abs; b = Abs; c = Abs};;

Tous les autres enregistrements peuvent être construits par modification de champs à partir de l’enregistrement vide ; il suffit de définir trois fonctions :

    let extend a r x = {a = Pre x; b = r.b;   c = r.c };;
    let extend b r x = {a = r.a;   b = Pre x; c = r.c };;
    let extend c r x = {a = r.a;   b = r.b;   c = Pre x};;

Par exemple, l’enregistrement {a = 1; b = 2} s’écrit :

    let deux = extend b (extend a nul 1) 2;;
    let trois = extend b (extend c deux 3) 4;;

De façon similaire, nous définissons trois fonctions d’accès à un enregistrement :

    let extract a r = let (Pre v) = r.a in v;;
    let extract b r = let (Pre v) = r.b in v;;
    let extract c r = let (Pre v) = r.c in v;;

On vérifie que extact a ab et extract b abc sont typables, mais que extract c ab ne l’est pas.

Le codage ci-dessus est tout à fait utilisable en pratique, soit pour une application particulière qui requiert des enregistrements extensibles alors qu’ils ne seraient pas fourni dans le langage, soit pour reprendre simplement l’idée du codage de la présence, sans les étiquettes, ou encore pour faire des exercices sur les enregistrements extensibles. Pour cela, il sera plus convivial de pré-définir un certain nombre d’étiquettes :

    type 'a label = Label of 'a;;

    let a = Label (extract a, extend a);;
    let b = Label (extract b, extend b);;
    let c = Label (extract c, extend c);;

Enfin, on peut utiliser des identificateurs cours et infixés pour retrouver une syntaxe plus habituelle, bien que cet exercice soit accrobatique :

    let ( // ) r f = f r;;
    let ( = ) (Label ( , extend)) x r = extend r x;;
    let ( $ ) r (Label (extract,  )) = extract r;;

Les exemples ci-dessus s’écrivent alors très naturellement :

    let deux = nul // (a = 1) // (b = 2) ;;
    let trois = deux // (c = 3) // (b = 4);;
    trois$b;;

Pour plus de sûreté, on pourra aussi contraindre les types des abréviations ci-dessus.

Solutions des exercices

Exercice 29, page 46

Les règles d’évaluation sont alors

\begin{matrix}(v @ \{ℓ_{0} = v_{0}\}).ℓ_{0} & ⟶^{ϵ} v & (δ_{1}) \\ (v @ \{ℓ_{0} = v_{0}\}).ℓ & ⟶^{ϵ} v.ℓ & (δ_{2}) \end{matrix}

Les deux approches sont équivalentes dans un langage purement fonctionnel (i.e. sans effets de bords). Cependant avec la nouvelle approche les enregistrements sont partagés, et une extension naturelle avec des champs mutables ne fournirait pas la sémantique attendue.

On distingue l’ancienne présentation (1) et la nouvelle présentation (2). La réduction dans (2) peut être abrégée en regroupant toutes les règles δ_{2} suivies d’une règle δ_{1} (qui ne peuvent jamais être en nombre infini). Les enregistrements de (1) peuvent être traduits en valeurs enregistrements de (2) de façon évidente et non ambigüe. On peut alors montrer qu’une étape de réduction dans (1) commute avec zéro ou une étape de réduction (regroupée) dans (2), modulo la traduction des enregistrements.

La terminaison dans (1) ou (2) sont équivalentes, et lorsque les programmes terminent, les valeurs obtenues se correspondent modulo la traduction des valeurs d’enregistrements.

Exercice 30, page 48

On ne peut plus écrire Pre → ∅(τ) ni \{\underline{\{∅\}}\}. On peut encore écrire \{l_{1} : τ_{1}; ℓ_{1} : τ_{2}; \underline{∅}\} ainsi que \{ℓ : \underline{α}; \underline{α}\}. La résponse à la deuxième question est décrite dans la section suivant l’énoncé de l’exercice.

Exercice 31, page 49

Comme suggéré, on ajoute des variables de sortes. On se donne des variables de sortes ϵ, et l’on construit les expressions sortes avec les constructeurs de sortes Type and ∅ d’arité 0, et (Row ) et (ℓ. ) d’arité 1. La signature Σ_{1} permet de restreindre les termes par la grammaire suivante :

\begin{matrix}κ ::= & ϵ | Type | Row (κ_{1}) \\ κ_{1} ::= & ϵ | ∅ | ℓ · κ_{1} \end{matrix}

La signature Σ_{2} élimine les termes dont de la forme ℓ_{1} · . . . ℓ_{k} · κ_{1} où au moins deux des étiquettes du préfixe sont identiques. Les sortes sont égales modulo la seule équation de commutativité gauche :

ℓ_{1} · ℓ_{2} · ϵ = ℓ_{2} · ℓ_{1} · ϵ

Il est facile de montrer que l’algèbre des sortes est une algèbre d’enregistrements particulière.

On en déduit un algorithme d’unification sur les sortes... pourvu que les sortes soient elles-même bien formées. Cet agorithme termine et est correct pour les expressions de sorte bien formées. En fait, commes les expressions de sorte initiales sont toujours localement bien formées, le seul cas d’expressions de sorte mal formées qui peuvent apparaître en cours de calcul sont des expressions cycliques. Dans ce cas l’agorithme de vérification des sortes boucle, en fabriquant des sortes de plus en plus grandes. Comme ces sortes sont construites à partir des étiquettes figurant dans le programme source, donc en nombre connu, il est facile de détecter ce cas et l’expression de type testée est donc mal formée.

Exercice 33, page 53

On le vérifie d’abord pour la δ-règle des variantes donnée ci-dessus, puis indépendamment, pour la β-règle. On le montre ensuite pour une réduction ayant lieu dans un contexte d’évaluation E quelconque par induction structurelle sur E.

Exercice 34, page 53

Le typage des enregistrements fournit :

[[inject_{ℓ}]] : α_{1} → ℓ : Pre (α_{1} → α_{2}); α_{3} → α_{2}

Il y a deux problèmes, cependant. D’une part, ce type est compliqué et donc peu lisible. D’autre part, appliquée à une valeur monomorphe, c’est-à-dire une fois α_{1} remplacé par un type τ_{1}, on s’attend à avoir un type monomorphe, alors que les variables α_{2} et α_{3} sont libre et donc universellement quantifiées en tête.