Typage et évaluation en Mini-ML
Typage et évaluation en Mini-ML
“Typage et programmation”
Xavier Leroy
[Link]@[Link]
3 Inférence de types 27
3.1 Introduction à l’inférence de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.2 Inférence de types pour mini-ML avec typage monomorphe . . . . . . . . . . . . . . 28
3.2.1 Construction du système d’équations . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.2 Lien entre typages et solutions des équations . . . . . . . . . . . . . . . . . . 30
3.2.3 Résolution des équations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.4 L’algorithme d’inférence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.3 Inférence de types pour mini-ML avec typage polymorphe . . . . . . . . . . . . . . . 32
1
3.3.1 L’algorithme W de Damas-Milner-Tofte . . . . . . . . . . . . . . . . . . . . . 33
3.3.2 Propriétés de l’algorithme W . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3.3 Typage polymorphe de ML par expansion des let . . . . . . . . . . . . . . . 38
3.3.4 Complexité du typage polymorphe de ML . . . . . . . . . . . . . . . . . . . . 40
5 La programmation impérative 47
5.1 Les références . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
5.2 Sémantique à réduction pour les références . . . . . . . . . . . . . . . . . . . . . . . . 48
5.3 Typage des références . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.4 Restreindre la généralisation aux expressions non expansives . . . . . . . . . . . . . . 52
5.5 Preuve de sûreté du typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.6 Autres approches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.6.1 Les références monomorphes . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.6.2 Les variables faibles de Standard ML . . . . . . . . . . . . . . . . . . . . . . . 58
5.6.3 Systèmes d’effets et de régions . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.6.4 Variables dangereuses et typage des fermetures . . . . . . . . . . . . . . . . . 59
5.7 Les exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.8 Continuations et opérateurs de contrôle . . . . . . . . . . . . . . . . . . . . . . . . . 61
2
7.1.4 Règles de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.1.5 Sûreté du typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.1.6 Inférence de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.2 Sous-typage et subsomption explicite . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
7.3 Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
7.3.1 Évaluation des classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
7.3.2 Typage des classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
7.4 Les types récursifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
7.4.1 Présentations des types récursifs . . . . . . . . . . . . . . . . . . . . . . . . . 84
7.4.2 Sous-typage et types récursifs . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
7.4.3 Inférence en présence de types récursifs . . . . . . . . . . . . . . . . . . . . . 86
7.5 Inférence par contraintes de sous-typage . . . . . . . . . . . . . . . . . . . . . . . . . 86
7.5.1 Règles de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
7.5.2 Construction du système de contraintes . . . . . . . . . . . . . . . . . . . . . 87
7.5.3 Lien entre typages et solutions des équations . . . . . . . . . . . . . . . . . . 88
7.5.4 Cohérence d’un système de contraintes . . . . . . . . . . . . . . . . . . . . . . 88
7.5.5 Algorithme d’inférence de types . . . . . . . . . . . . . . . . . . . . . . . . . . 90
8 Systèmes de modules 94
8.1 Un calcul de modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
8.2 Évaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
8.2.1 Sémantique par traduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
8.2.2 Sémantique à réduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
8.3 Règles de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
8.3.1 Équivalence entre types de base . . . . . . . . . . . . . . . . . . . . . . . . . . 97
8.3.2 Typage du langage de base . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
8.3.3 Sous-typage entre types de modules . . . . . . . . . . . . . . . . . . . . . . . 99
8.3.4 Typage du langage de modules . . . . . . . . . . . . . . . . . . . . . . . . . . 101
3
Chapter 1
Nous omettons les détails de la syntaxe concrète (forme des identificateurs, parenthèses, priorités
des opérations, . . . ).
La classe c contient des constantes comme par exemple des constantes entières 0, 1, 2, −1, . . . ,
les booléens true, false, ou des chaı̂nes littérales "foo", . . . . La classe op contient des symboles
d’opérations primitives, comme l’addition entière +, les projections fst et snd pour accéder aux
composantes d’une paire, etc.
Exemples d’expressions:
+ (3, 2)
le calcul de 3 plus 2
3 + 2
le même, avec notation infixe pour le +
fun x → + (x, 1)
la fonction ‘‘successeur’’
fun f → fun g → fun x → f(g x)
la composition de fonctions
let double = fun f → fun x → f(f x) in
let fois2 = fun x → + (x, x) in
4
let fois4 = double fois2 in
double fois4
la fonction ‘‘fois 16’’
Exercice 1.1 (*) Pour définir des fonctions récursives en ML, on dispose de la construction
spéciale let rec f x = a1 in a2 . Traduire cette expression en mini-ML en terme de let et fix.
Exercice 1.2 (**) Même question pour la récursion mutuelle de ML: let rec f x = a1 and g y =
a2 in a3 .
5
Valeurs: v ::= fun x → a valeurs fonctionnelles
|c valeurs constantes
| op primitives non appliquées
| (v1 , v2 ) paire de deux valeurs
(Remarquons qu’ici les valeurs sont un sous-ensemble des expressions; ce n’est pas toujours le cas
dans ce style de sémantique.)
P1 P2 ... Pn
P
qui se lisent “si P1 , . . . , Pn sont vraies, alors P est vraie”. Une autre lecture de la règle d’inférence
ci-dessus est comme l’implication P1 ∧ . . . ∧ Pn ⇒ P .
Les règles d’inférence et les axiomes peuvent contenir des variables libres, qui sont implicitement
quantifiées universellement en tête de la règle. Par exemple, l’axiome A(x) signifie ∀x.A(x); la règle
P1 (x) P2 (y)
P (x, y)
Impair(n) Pair(n)
Pair(0)
Pair(n + 1) Impair(n + 1)
Il faut les lire comme les conditions suivantes portant sur les prédicats Pair et Impair:
Pair(0)
∀n. Impair(n) ⇒ Pair(n + 1)
∀n. Pair(n) ⇒ Impair(n + 1)
Il y a de nombreux prédicats sur les entiers qui satisfont ces conditions, par exemple Pair(n) et
Impair(n) vrais pour tout n. Cependant, les plus petits prédicats (les prédicats vrais les moins
souvent) vérifiant ces conditions sont Pair(n) = (n mod 2 = 0) et Impair(n) = (n mod 2 = 1). Les
règles d’inférence définissent donc Pair et Impair comme étant ces deux prédicats.
Exercice 1.3 (**) Montrer que pour tout ensemble de règles d’inférence sur un prédicat, il existe
toujours un plus petit prédicat satisfaisant ces règles. Pour être plus précis, on considèrera un
ensemble d’axiomes et de règles sur un seul prédicat P à un paramètre:
6
P (b1j (x)) ... P (bnj (x))
P (ai (x))
P (cj (x))
(Indication: montrer que si on a une famille de prédicats (Pk )k∈K qui satisfont les règles, alors
V
leur conjonction k∈K Pk les satisfait aussi.)
Une dérivation (encore appelée arbre de preuve) dans un système de règles d’inférence est
un arbre portant aux feuilles des instances des axiomes et aux noeuds des conclusions de règles
d’inférence dont les hypothèses sont justifiées par les fils du noeud dans l’arbre. La conclusion de
la dérivation est le noeud racine de l’arbre. On représente généralement les dérivations par des
“empilements” d’instances de règles d’inférence, avec la conclusion de la dérivation en bas. Par
exemple, voici une dérivation qui conclut Impair(3) dans le système de règles ci-dessus:
Pair(0)
Impair(1)
Pair(2)
Impair(3)
Les dérivations caractérisent exactement les plus petits prédicats vérifiant un ensemble de règles
d’inférences. Par exemple, Pairmin (n) est vrai (où Pairmin est le plus petit prédicat satisfaisant
les règles d’inférence) si et seulement si il existe une dérivation qui conclut l’énoncé Pair(n).
Exercice 1.4 (**) En se plaçant dans le même cadre que l’exercice 1.3, montrer que le prédicat
défini par “il existe une dérivation de l’énoncé P (x) dans le système de règles” est le plus petit
prédicat satisfaisant le système de règles.
On a noté a[x ← v] l’expression obtenue en substituant chaque occurrence de x libre dans a par
v. Ainsi, (+ (x, 1))[x ← 2] est +(2, 1), mais (fun x → x)[x ← 2] est (fun x → x).
Les règles 1, 2, 3 expriment que les constantes, les opérateurs et les fonctions sont déjà
entièrement évalués: il n’y a rien à faire lors de l’évaluation. La règle 4 exprime que pour évaluer
une application a1 a2 , il faut évaluer a1 et a2 . Si la valeur de a1 est une fonction fun x → a
7
(règle 4), le résultat de l’application est la valeur de a après substitution du paramètre formel x par
l’argument effectif v2 (la valeur de a2 ). Enfin, pour une construction let x = a1 in a2 , la règle 6
exprime qu’il faut d’abord évaluer a1 , puis substituer x par sa valeur dans a2 et poursuivre avec
l’évaluation de a2 .
Pour être complet, il faut ajouter des règles pour chaque opérateur op qui nous intéresse,
décrivant l’évaluation des applications de cet opérateur. Par exemple, pour +, fst et snd, nous
avons les règles
v v
a1 → + a2 → (n1 , n2 ) n1 , n2 constantes entières et n = n1 + n2
(7)
v
a1 a2 → n
v v v v
a1 → fst a2 → (v1 , v2 ) a1 → snd a2 → (v1 , v2 )
(8) (9)
v v
a1 a2 → v1 a1 a2 → v2
v
Exemple: nous avons (fun x → +(x, 1)) 2 → 3, car la dérivation suivante est valide:
v v
2→2 1→1
v v
+→+ (2, 1) → (2, 1)
v v v
(fun x → +(x, 1)) → (fun x → +(x, 1)) 2→2 +(2, 1) → 3
v
(fun x → +(x, 1)) 2 → 3
v
Exercice 1.5 (*) On considère l’expression a = 1 2. Existe-t’il une valeur v telle que a → v?
Même question avec l’expression a0 = (fun f → (f f )) (fun f → (f f )). Quelle différence voyez-
vous entre ces deux exemples?
Exercice de programmation 1.1 (*) Implémenter un évaluateur pour le langage mini-ML qui
suive les règles ci-dessus. Essayez-le sur les exemples d’expressions donnés dans ce chapitre. Com-
ment votre évaluateur se comporte-t’il sur les expressions de l’exercice 1.5?
8
Cas a est un opérateur op ou une abstraction fun x → a. Comme le cas précédent.
Cas a est une paire (a1 , a2 ). Une seule règle d’évaluation peut s’appliquer à a: la règle 5. Donc, la
dérivation D est nécessairement de la forme
(D1 ) (D2 )
.. ..
. .
v v
a1 → v1 a2 → v2
v
(a1 , a2 ) → (v1 , v2 )
9
(D1 ) (D2 ) (D3 )
.. .. ..
. . .
v v v
a1 → fun x → a a2 → v2 a[x ← v2 ] → v
v
a1 a2 → v
(D10 ) (D20 ) (D30 )
.. .. ..
. . .
v v v
a1 → fun x → a a2 → v2 a[x ← v2 ] → v 0
v
a1 a2 → v 0
Appliquant une dernière fois l’hypothèse de récurrence aux dérivations D3 et D30 , il vient v = v 0
comme attendu.
Si v1 est un opérateur +, fst, ou snd, nous concluons directement v = v 0 par examen des règles,
sans avoir besoin d’invoquer l’hypothèse de récurrence une troisième fois.
Cas a est let x = a1 in a2 . Le résultat découle de l’hypothèse de récurrence par un raisonnement
analogue au cas de l’application. 2
Exercice 1.6 (*) Rédiger complètement le dernier cas de la preuve ci-dessus.
Un corollaire de la proposition 1.1 est que l’évaluation de mini-ML est réellement une fonction
partielle eval des expressions dans les valeurs: eval (a), si défini, est l’unique valeur v telle que
v
a → v.
Nous avons cependant gardé une présentation relationnelle, car elle s’étend plus facilement avec
des primitives non-déterministes. Par exemple, donnons-nous une primitive random(n) qui renvoie
un nombre réellement aléatoire entre 0 et n. Sa règle d’évaluation est:
v v
a1 → random a2 → n n entier et 0 ≤ m ≤ n
v
a1 (a2 ) → m
v v
Avec cette règle, on a random(1) → 0 et random(1) → 1, exprimant que 0 et 1 sont deux valeurs
correctes pour cette expression.
10
Types: τ ::= T type de base (int, bool, etc)
|α variable de type
| τ1 → τ2 type des fonctions de τ1 dans τ2
| τ1 × τ2 type des paires de τ1 et τ2
Pour les règles (const) et (op), on se donne une fonction T C qui associe un type à chaque
constructeur et opérateur; par exemple, T C(0) = T C(1) = int et T C(+) = int × int → int.
Dans la règle (var), E(x) est le type qui est associé à x dans l’environnement E. Dans les règles
(fun) et (let), E + {x : τ } est l’environnement qui associe τ à x et qui est identique à E sur toute
variable autre que x.
11
Exemples de typages que l’on ne peut pas dériver:
Exemples d’expressions que l’on ne peut pas typer (il n’existe pas de E et de τ tels que E ` a : τ ):
12
fun f → f f
let f = fun x → x in (f 1, f true)
Exercice 1.7 (*) Expliquer pourquoi ces trois dernières expressions ne sont pas typables.
Lorsque l’ensemble des variables quantifiées est vide, on note simplement τ au lieu de ∀. τ .
Ainsi, les types peuvent être vus comme des schémas triviaux.
Les variables liées par ∀ peuvent être librement renommées (opération d’alpha-conversion), et
les schémas de types sont considérés égaux modulo alpha-conversion:
L’ensemble L(τ ), L(σ), L(E) des variables libres d’un type τ , d’un schéma de types σ ou d’un
environnement E est formellement défini comme suit:
L(T ) = ∅
L(α) = {α}
L(τ1 → τ2 ) = L(τ1 ) ∪ L(τ2 )
L(τ1 × τ2 ) = L(τ1 ) ∪ L(τ2 )
L(∀α1 , . . . , αn . τ ) = L(τ ) \ {α1 , . . . , αn }
[
L(E) = L(E(x))
x∈Dom(E)
Avec ces notations, l’égalité de deux schémas modulo alpha-conversion se définit formellement
comme suit:
12
Exercice 1.8 (*)/(**) Montrer que L(τ [α1 ← β1 , . . . , αn ← βn ]) = L(τ )[α1 ← β1 , . . . , αn ← βn ].
En déduire que la définition de L(σ) passe bien au quotient par alpha-conversion.
Un schéma de types peut être vu comme l’ensemble des types obtenus en instanciant
(spécialisant) ses variables quantifiées par des types particuliers. Ainsi, ∀α. α → α peut être vu
comme l’ensemble des types {τ → τ | τ type}. Pour formaliser cette intuition, on définit la relation
τ ≤ σ (lire: le type τ est une instance du schéma de types σ) de la manière suivante:
Exemples: int → int est une instance de ∀α. α → α, ainsi que bool → bool, mais pas int → bool.
Remarque: si σ est le schéma trivial ∀.τ 0 , alors τ ≤ σ est équivalent à τ = τ 0 .
• de même, T C associe des schémas de types aux constantes et aux opérateurs, par exemple
• la règle de typage des identificateurs effectue une étape d’instanciation sur le schéma de type
de l’identificateur;
• enfin, la règle du let généralise le type de l’expression liée avant de typer le corps du let.
Autrement dit, Gen(τ1 , E) est τ1 dans lequel on a généralisé toutes les variables qui ne sont pas
libres dans l’environnement E.
13
Exemple:
α≤α int → int ≤ ∀α. α → α
{x : α} ` x : α {f : ∀α. α → α} ` f : int → int {f : ∀α. α → α} ` 1 : int
∅ ` fun x → x : α → α {f : ∀α. α → α} ` f 1 : int
∅ ` let f = fun x → x in f 1 : int
Exercice 1.9 (*) Peut-on typer les expressions ci-dessous en mini-ML? Avec quels types?
let f = fun x → x in f f
fun f → f f
Exercice 1.10 (**) Une définition plus simple de Gen serait Gen(τ1 , E) = ∀α1 , . . . , αn . τ1 où
{α1 , . . . , αn } = L(τ1 ). (Autrement dit, on généralise toutes les variables de τ1 , même celles qui
sont libres dans E.) Montrer sur un exemple que cela conduit à des typages incorrects (c.à.d. qui
attribuent des types sémantiquement trop généraux à certaines expressions).
La seconde propriété est que les typages ne changent pas si dans l’environnement de typage on
ajoute ou supprime des hypothèses de typage portant sur des variables non libres dans l’expression.
Par exemple, si la seule variable libre dans a est x, alors on peut dériver
{x : σx ; y : int} ` a : τ
si et seulement si on peut dériver
{x : σx ; z : bool} ` a : τ
14
Proposition 1.3 (Indifférence du typage vis-à-vis des hypothèses inutiles) Supposons
E1 (x) = E2 (x) pour tout identificateur x libre dans l’expression a. Alors E1 ` a : τ si et seulement
si E2 ` a : τ .
La troisième propriété est que tous les typages que l’on peut dériver sous certaines hypothèses
peuvent être dérivés sous des hypothèses “plus fortes”. Pour formaliser cette notion de “plus fort”,
on dit qu’un schéma de type σ 0 est plus général qu’un autre schéma σ, et on note σ 0 ≥ σ, si toute
instance de σ est aussi instance de σ 0 . On montre facilement que σ 0 ≥ ∀α1 . . . αn . τ (où les αi sont
choisies non libres dans σ 0 ) si et seulement si τ ≤ σ 0 .
La preuve des propositions 1.2, 1.3 et 1.4 est facile dans le cas du système de types monomorphe
de la section 1.3.2 (par récurrence sur les dérivations de typage), mais beaucoup plus difficile dans
le système de types de ML (les récurrences “passent” difficilement sur le cas de la règle (let-gen)).
Exercice 1.11 (***) Prouver la proposition 1.2. (On commencera par définir précisément l’image
ϕ(σ) d’un schéma de types σ par une substitution ϕ.)
15
Chapter 2
Le but du typage statique est d’éliminer toute une classe de programmes absurdes, comme par
exemple 1 2 ou 1 + (fun x → x). Dans ce cours, nous allons prouver que c’est le cas pour les
systèmes de types introduits au chapitre 1. Cette propriété que tout programme bien typé s’évalue
“sans problèmes” est appelée sûreté du typage vis-à-vis de l’évaluation.
16
Le problème de cette approche est qu’il y a une autre classe d’expressions qui ne s’évalue pas en
une valeur, mais pourtant ne déclenche pas d’erreurs à l’exécution: les expressions qui ne terminent
pas. (Leur calcul “boucle” sans jamais effectuer d’opération incorrecte.)
Certains systèmes de types ne laissent passer que des programmes qui terminent toujours. On
dit que ce sont des systèmes de types fortement normalisants. (C’est le cas des systèmes de types
du chapitre 1 tant qu’on n’y ajoute pas un opérateur de point fixe.) Ces systèmes de types sont très
importants dans le monde de la logique constructive, mais pas très intéressants pour les langages
de programmation. En général, on souhaite qu’un langage de programmation soit Turing-complet,
c’est-à-dire qu’il puisse exprimer toutes les fonctions calculables; étant donné l’indécidabilité du
problème de l’arrêt, cela veut dire que leur système de types ne peut pas laisser passer tous les
programmes qui terminent et rejeter tous ceux qui ne terminent pas.
Pour cette raison, nous allons considérer des systèmes de types qui ne garantissent pas que
les programmes bien typés terminent. Un exemple simple est le système de types de mini-ML du
chapitre 1 muni de l’opérateur de point fixe fix. Pour un langage tel que mini-ML + fix, la
propriété
v
Si a est bien typée, alors il existe une valeur v telle que a → v.
est fausse. Par exemple,
let fact = fix(fun fact → fun n → if n = 0 then 1 else n * fact(n-1))
in fact (-1)
est bien typée (vérifiez-le!), mais ne termine pas, et donc ne s’évalue en aucune valeur v. Il faut
donc trouver une autre caractérisation des programmes erronés.
17
Il faut aussi ajouter des règles pour propager err vers le haut: si l’évaluation d’une sous-expression
produit une erreur, l’évaluation de l’expression tout entière la produit aussi.
v v v v
a1 → err a1 → v1 a2 → err a1 → err
(15) (16) (17)
v v v
a1 a2 → err a1 a2 → err (a1 , a2 ) → err
v v v v v
a1 → v1 a2 → err a1 → err a1 → v1 a2 → err
(18) (19) (20)
v v v
(a1 , a2 ) → err let x = a1 in a2 → err let x = a1 in a2 → err
La propriété de sûreté du typage s’énonce alors ainsi:
v
Si a est bien typée et a → r, alors r 6= err.
v
Autrement dit, une expression a bien typée peut s’évaluer en une valeur (a → v) ou bien ne pas
v v
terminer (a →6 r pour tout r), mais ne peut pas provoquer une erreur d’exécution (a → err).
Cette propriété de sûreté est vraie, et se prouve par récurrence structurelle sur la dérivation
v
de a → r. Cependant, cette approche n’est pas entièrement satisfaisante, pour plusieurs raisons.
Tout d’abord, il faut ajouter beaucoup de règles, et cela rend peu lisible la sémantique du langage.
De plus, il y a un gros risque d’oublier d’ajouter certaines règles d’erreur. Par exemple, si nous
oublions la règle 12, la propriété de sûreté ci-dessus reste vraie (puisqu’il y a moins de programmes
a qui vont s’évaluer en err), mais elle ne nous garantit plus qu’il est inutile de vérifier à l’exécution
que les deux arguments de + sont des entiers. Rien ne nous prouve formellement que nous avons
mis toutes les bonnes règles d’erreur et que donc les vérifications à l’exécution sont inutiles.
Pour ces raisons, nous allons abandonner la sémantique opérationnelle structurelle et introduire
un nouveau style de sémantique, la sémantique à réductions, qui nous permettra de prouver un
résultat plus fort de sûreté du typage.
a → a1 → a2 → . . . → v
18
On se donne aussi des axiomes pour les opérateurs complètement appliqués. Ces axiomes s’appellent
aussi des δ-règles et dépendent bien sûr des opérateurs considérés. Voici les δ-règles pour +, fst,
snd, ifthenelse, et fix:
ε
+ (n1 , n2 ) → n si n1 , n2 entiers et n = n1 + n2 (δ+ )
ε
fst (v1 , v2 ) → v1 (δf st )
ε
snd (v1 , v2 ) → v2 (δsnd )
ε
fix (fun x → a) → a{x ← fix (fun x → a)} (δf ix )
ε
ifthenelse(true, (a1 , a2 )) → a1 (δif )
ε
ifthenelse(false, (a1 , a2 )) → a2 (δif 0 )
Bien sûr, on ne réduit pas toujours en tête de l’expression. Considérons par exemple
Aucun des axiomes ci-dessus ne s’applique à a. Pour évaluer a, il est clair qu’il faut commencer
par réduire “en profondeur” la sous-expression +(1, 2). Cette notion de réduction en profondeur
est exprimée par la règle d’inférence suivante:
ε
a → a0
(contexte)
Γ(a) → Γ(a0 )
Dans cette règle, Γ est un contexte d’évaluation. Les contextes d’évaluation sont définis par la
syntaxe abstraite suivante:
Contextes d’évaluation:
Γ ::= [ ] évaluation en tête
|Γa évaluation à gauche d’une application
|v Γ évaluation à droite d’une application
| let x = Γ in a évaluation à gauche d’un let
| (Γ, a) évaluation à gauche d’une paire
| (v, Γ) évaluation à droite d’une paire
Rappels sur les contextes: Un contexte est une expression avec un “trou”, noté [ ]. Par
exemple, +([ ], 2). L’opération de base sur un contexte C est l’application C(a) à une expression
a. C(a) est l’expression dénotée par C dans laquelle le “trou” [ ] est remplacé par a. Par exemple,
+([ ], 2) appliqué à 1 est l’expression +(1, 2).
Les contextes d’évaluation Γ ne sont pas n’importe quelle expression avec un trou. Par exemple,
(+(1, 2), [ ]) n’est pas un contexte d’évaluation, car le membre gauche de la paire n’est pas une
valeur. L’idée est de forcer un certain ordre d’évaluation en restreignant les contextes. La syntaxe
des contextes ci-dessus force une évaluation en appel par valeur et de gauche à droite (on évalue la
sous-expression gauche d’une application, d’une paire ou d’un let avant la sous-expression droite).
19
Exemple Considérons l’expression a = (+(1, 2), +(3, 4)). Il n’y a qu’une manière de l’écrire
sous la forme a = Γ1 (a1 ) afin d’appliquer la règle (contexte): il faut prendre Γ1 = ([ ], +(3, 4)) et
ε
a1 = +(1, 2). Comme a1 → 3, on obtient a → Γ1 (3) = (3, +(3, 4)). Cette dernière expression peut
alors s’écrire sous la forme Γ2 (a2 ) avec Γ2 = (3, [ ]) et a2 = +(3, 4). Appliquant la règle (contexte),
on obtient le résultat Γ2 (7) = (3, 7). On a donc obtenu la séquence de réductions suivante:
qui nous emmène de a vers la valeur (3, 7) en évaluant toujours la sous-expression gauche en
premier. Si nous voulons commencer par évaluer la sous-expression droite +(3, 4), il faudrait écrire
a = Γ3 (a3 ) avec Γ3 (+(1, 2), [ ]) et a3 = +(3, 4), mais cela n’est pas possible car Γ3 n’est pas un
contexte d’évaluation.
∗
Réduction multiple et formes normales On définit la relation → (lire: “se réduit en zéro,
∗
une ou plusieurs étapes”) comme la fermeture réflexive et transitive de →. C’est-à-dire, a → a0 ssi
0 0
a = a ou il existe a1 , . . . , an tels que a → a1 → . . . → an → a .
On dit que a est en forme normale si a 6→, c’est-à-dire s’il n’existe pas d’expression a0 telle que
a → a0 . Remarquons que les valeurs v sont en forme normale. Il y a aussi d’autres expressions
qui sont en forme normale et qui ne sont pas des valeurs, comme [Link]. 1 2. Par la suite, nous
caractériserons les expressions erronées comme les formes normales qui ne sont pas des valeurs.
Exercice 2.1 (*) Modifier la syntaxe abstraite des contextes Γ pour forcer une évaluation de droite
à gauche. Même question si l’on ne veut pas spécifier l’ordre d’évaluation des sous-expressions.
Exercice 2.2 (**) Montrer que la sémantique par réduction de mini-ML est équivalente à la
v ∗
sémantique opérationnelle structurelle du chapitre 1: a → v si et seulement si a → v. (Indica-
v
tion: l’implication ⇒ est une récurrence facile sur la dérivation de a → v. Pour l’implication ⇐,
v
on montrera et on utilisera les deux lemmes suivants: (1) v → v pour toute valeur v; (2) si a → a0
v v
et a0 → v, alors a → v.)
20
1. a se réduit en un nombre fini d’étapes vers une valeur v:
a → a1 → . . . → an → v
Cela correspond à un calcul qui termine et ne rencontre pas d’erreurs pendant l’évaluation.
2. a se réduit à l’infini
a → a1 → . . . → an → . . .
C’est un calcul qui ne termine pas, mais ne rencontre pas d’erreurs pendant l’évaluation.
a → a1 → . . . → an 6→
Dans ce cas, an est une expression absurde (du genre de 1 2). Ici, le calcul “plante” car il
provoque une erreur d’exécution.
Nous allons prouver que si l’expression a est bien typée, le cas (3) ne peut pas se produire: ou
bien a se réduit en une valeur (cas (1)), ou bien a ne termine pas (cas (2)), mais dans tous les cas
aucune erreur d’exécution ne se produit. Ceci est un corollaire des deux propriétés suivantes:
• Les formes normales bien typées sont des valeurs: si a est en forme normale vis-à-vis de →
et si ∅ ` a : τ , alors a est une valeur.
∗
Théorème 2.1 (Sûreté du typage) Si ∅ ` a : τ et a → a0 et a0 est une forme normale, alors a0
est une valeur.
Nous allons maintenant prouver les deux propriétés utilisées dans la preuve ci-dessus.
Autrement dit, tous les types possibles pour a1 doivent être des types possibles pour a2 .
21
Démonstration: Soient E et τ tels que E ` Γ(a1 ) : τ (1). Nous montrons que E ` Γ(a2 ) : τ par
récurrence structurelle sur le contexte Γ.
Cas de base Γ = [ ]. Immédiat.
Cas Γ = Γ0 a. Une dérivation de (1) se termine par
E ` Γ0 (a1 ) : τ 0 → τ E`a:τ
E ` Γ0 (a1 ) a : τ
E ` a0 : τ 0
E + {x : ∀α1 . . . αn .τ 0 } ` a : τ
avec α1 , . . . , αn non libres dans E, et aucune des variables x liées dans a n’est libre dans a0 . Alors,
E ` a[x ← a0 ] : τ
22
Démonstration: par récurrence sur la structure de l’expression a. On écrit Ex pour
E + {x : ∀α1 . . . αn .τ1 }.
Cas a est x. Nous avons alors a[x ← a0 ] = a0 . Par hypothèse, Ex ` x : τ , et donc τ ≤ ∀α0 . . . αn .τ 0 .
C’est-à-dire que τ = ϕ(τ 0 ) pour une certaine substitution ϕ sur les αi . Appliquant la propriété de
stabilité du typage par substitution du chapitre 1 (proposition 1.2) à l’énoncé E ` a0 : τ 0 et à la
substitution ϕ, il vient ϕ(E) ` a0 : ϕ(τ 0 ), c’est-à-dire E ` a0 : ϕ(τ 0 ) puisque les αi ne sont pas libres
dans E. Nous avons donc montré E ` a0 : τ ; c’est le résultat attendu.
Cas x n’est pas libre dans a. Ceci recouvre les cas suivants: a est une variable y 6= x; a est une
constante c ou un opérateur op; et a = fun x → a1 . Alors, a[x ← a0 ] = a. De plus, Ex ` a : τ
implique E ` a : τ par la proposition 1.3 (indifférence du typage vis-à-vis des hypothèses inutiles).
CQFD.
Cas a = fun y → a1 avec y 6= x. Si les αi apparaissent dans τ , nous pouvons les renommer en
des variables βi non libres dans E et distinctes des αi par la substitution θ = [αi ← βi ]. Si les αi
n’apparaissent pas dans τ , nous prenons θ égale à l’identité. Par la proposition 1.2, nous avons
Ex ` a : θ(τ ) dans les deux cas.
Comme Ex ` a : θ(τ ), nous avons θ(τ ) = τ2 → τ1 et
Ex + {y : τ2 } ` a1 : τ1
Ex ` fun y → a1 : τ2 → τ1
Ex ` a1 : τ2 → τ Ex ` a2 : τ2
Ex ` a1 a2 : τ
E ` a1 [x ← a0 ] : τ2 → τ E ` a2 [x ← a0 ] : τ2
E ` a1 [x ← a0 ] a2 [x ← a0 ] : τ
23
typage par renforcement des hypothèses (proposition 1.4), E + {x : Gen(τ1 , Ex )} ` a2 : τ implique
E + {x : Gen(τ1 , E)} ` a2 : τ . D’où la dérivation du résultat attendu:
E ` a1 [x ← a0 ] : τ1 E + {x : Gen(τ1 , E)} ` a2 : τ
Ex ` let x = a1 [x ← a0 ] in a2 : τ
E ` a1 [x ← a0 ] : τ1 E + {y : Gen(τ1 , E)} ` a2 [x ← a0 ] : τ
Ex ` let y = a1 [x ← a0 ] in a2 [x ← a0 ] : τ
E + {x : τ 0 } ` a1 : τ
E ` (fun x → a1 ) : τ 0 → τ E ` v : τ0
E ` (fun x → a1 ) v : τ
Nous appliquons le lemme de substitution (proposition 2.2) aux deux prémisses. Il vient E `
a1 [x ← v] : τ , c’est-à-dire E ` a0 : τ . D’où le résultat attendu a v a0 . 2
24
Proposition 2.4 (Préservation du typage par réduction) Si a → a0 , alors a v a0 .
Démonstration: Si c’est une réduction de tête, le résultat s’ensuit par la proposition 2.3. Sinon,
c’est une application de la règle (contexte):
ε
a1 → a01
Γ(a1 ) → Γ(a01 )
Par la proposition 2.3, a1 v a01 . Par croissance de v (proposition 2.1), Γ(a1 ) v Γ(a01 ). C’est le
résultat attendu. 2
Démonstration: par examen des règles de typage qui peuvent s’appliquer suivant la forme de τ .
Seules les règles (const-inst), (op-inst), (fun) et (paire) sont à considérer, car les autres règles
s’appliquent à des expressions qui ne sont pas des valeurs. Notons que par hypothèse H0, (const-
inst) ne s’applique que si τ est un type de base, et (op-inst) que si τ est un type flèche. 2
En conséquence, un terme bien typé ou bien est une valeur, ou bien peut se réduire.
25
Si a1 et a2 sont des valeurs, par la proposition 2.5, a1 est ou bien une fonction fun x → a3 ou
bien un opérateur op. Dans le premier cas, a1 a2 se réduit par la règle βf un . Dans le deuxième cas,
l’hypothèse H2 dit que a1 a2 peut aussi se réduire.
Cas a = let x = a1 in a2 . On a
∅ ` a1 : τ1 ∅ + {x : Gen(τ1 , ∅)} ` a2 : τ2
∅ ` (let x = a1 in a2 ) : τ2
Si a1 n’est pas une valeur, l’hypothèse de récurrence montre qu’elle peut se réduire, et donc a peut
aussi se réduire par la règle (contexte). Si a1 est une valeur, la règle βlet s’applique à a.
Cas a = (a1 , a2 ). On a
∅ ` a1 : τ1 ∅ ` a2 : τ2
∅ ` (a1 , a2 ) : τ1 × τ2
Si a1 n’est pas une valeur, par hypothèse de récurrence, elle peut se réduire, et donc a peut aussi
se réduire par la règle (contexte). Même raisonnement si a1 est une valeur mais pas a2 . Si a1 et a2
sont toutes deux des valeurs, a est aussi une valeur. CQFD. 2
Proposition 2.7 (Les formes normales bien typées sont des valeurs) Si ∅ ` a : τ et a est
en forme normale vis-à-vis de →, alors a est une valeur
Exercice 2.3 (*) Vérifier H0, H1 et H2 pour les constantes entières et les opérateurs +, fst, snd,
et fix.
26
Chapter 3
Inférence de types
Vérification pure: Dans le source, toutes les sous-expressions du programme, ainsi que tous les
identificateurs, sont annotés par leur type.
fun (x:int) →
(let (y:int) = (+:int×int→int)((x:int),(1:int):int×int) in (y:int) : int)
Le typeur est alors très simple, puisque le programme source contient déjà autant d’informations
de typage que la dérivation de typage correspondante. La patience du programmeur est mise à
rude épreuve par la quantité d’annotations de types à fournir. Aucun langage réaliste ne suit cette
approche.
27
Le typeur infère le type int → int pour cette expression. Cette approche est suivie par la plupart
des langages impératifs: Pascal, C, Java, . . . (En fait, ces langages exigent un peu plus d’annotations
de types; par exemple, il faut aussi déclarer le type du résultat des fonctions.)
Déclaration des types des paramètres de fonction et propagation des types: La seule
différence par-rapport à l’approche précédente est que les variables locales ([Link]. les identificateurs
liés par let) ne sont pas annotées par leur type, ce dernier étant déterminé par le type de l’expression
liée à la variable. Exemple:
Ayant déterminé que +(x,1) est de type int, le typeur déduit que y est de type int dans le reste
de la fonction.
Inférence complète de types: Le programme source ne contient aucune déclaration de type sur
les paramètres de fonctions ni sur les variables locales. Le typeur détermine le type des paramètres
de fonctions d’après l’utilisation qui en est faite dans le reste du programme. Exemple:
Puisque l’addition + n’opère que sur des paires d’entiers, x est forcément de type int. C’est
l’approche suivie dans les langages de la famille ML.
Dans ce cours, nous allons nous concentrer sur la dernière approche (inférence complète), car les
autres sont techniquement très simples. On pourra faire l’exercice suivant pour se familiariser avec
l’avant-dernière approche.
Exercice de programmation 3.1 Écrire un typeur pour mini-ML avec typage monomorphe (sec-
tion 1.3.2) et dans lequel les paramètres de fonctions sont annotés dans le programme source par
leur type:
Expressions: a ::= . . . | fun (x : τ ) → a
Il s’agit donc de la troisième approche dans la liste ci-dessus. On écrira le typeur sous la forme
d’une fonction prenant une expression a et un environnement de typage E en arguments, et ren-
voyant un type τ pour a dans E s’il existe, ou bien échoue (en levant une exception) si a n’est pas
typable dans E.
Quels problèmes se posent si l’on veut étendre ce typeur à mini-ML avec typage polymorphe (en
gardant les paramètres de fonctions annotés par leurs types)?
1. À partir du programme source, on construit un système d’équations entre types qui caractérise
tous les typages possibles pour ce programme.
28
2. On résout ensuite ce système d’équations. S’il n’y a pas de solution, le programme est mal
typé. Sinon, on détermine une solution principale au système d’équation; cela nous donne le
type principal du programme.
En combinant ces deux phases, on obtient un algorithme de typage qui détermine si un programme
est bien typé et si oui, calcule son type principal.
On a:
?
C(a) = { αb = αe → αa ;
?
αb = αx → αc ;
?
αc = αy → αd ;
?
αd = int;
?
αe = bool}
Exercice de programmation 3.2 Écrire une fonction qui prend une expression a en entrée et
construit son ensemble d’équations C(a). Pour associer les variables αb , αx aux sous-expressions
b et aux identificateurs x, on pourra ou bien utiliser une table d’association globale (table de
hachage ou autre), ou bien écrire une première passe sur a qui annote les identificateurs et les
sous-expressions par des variables de types.
29
3.2.2 Lien entre typages et solutions des équations
Une solution de l’ensemble d’équations C(a) est une substitution ϕ telle que pour toute équation
?
τ1 = τ2 dans C(a), on ait ϕ(τ1 ) = ϕ(τ2 ). Autrement dit, une solution est un unificateur de
l’ensemble d’équations C(a).
Les deux propositions suivantes montrent que les solutions de C(a) caractérisent exactement
les typages possibles pour a.
Proposition 3.1 (Correction des solutions vis-à-vis du typage) Si ϕ est une solution de
C(a), alors E ` a : ϕ(αa ) où E est l’environnement de typage {x : ϕ(αx ) | x libre dans a}.
Proposition 3.2 (Complétude des solutions vis-à-vis du typage) Soit a une expression.
S’il existe un environnement E et un type τ tels que E ` a : τ , alors le système d’équations
C(a) admet une solution.
E + {x : τ1 } ` b : τ2
E ` fun x → b : τ1 → τ2
30
On a donc a = fun x → b et τ = τ1 → τ2 . Par application de l’hypothèse de récurrence, il existe
une solution ϕ0 de C(b) vérifiant de plus (1), (2) et (3). On prend ϕ = ϕ0 + [αa ← τ ]. Il est facile
?
de voir que ϕ est une solution de C(a) = C(b) ∪ {αa = αx → αb }. En effet,
et d’autre part ϕ est solution de C(b) puisque ϕ prolonge ϕ0 . Enfin, les propriétés (1), (2) et (3)
sont vérifiées pour ϕ.
Cas la dérivation se termine par la règle (app).
E ` b : τ0 → τ E ` c : τ0
E`bc:τ
On a donc a = b c. En appliquant deux fois l’hypothèse de récurrence à b et c, il vient des
solutions ϕ1 et ϕ2 de C(b) et C(c) qui satisfont les propriétés (1)–(3). Par la propriété (2), il vient
ϕ1 (αx ) = ϕ2 (αx ) pour tout x ∈ Dom(E). On peut donc prendre ϕ = ϕ1 + ϕ2 + [αa ← τ ]. C’est
une substitution qui prolonge ϕ1 et ϕ2 . Donc, ϕ est solution de C(b) et C(c). Enfin,
mgu(∅) = id
?
mgu({α = α} ∪ C) = mgu(C)
?
mgu({α = τ } ∪ C) = mgu(C[α ← τ ]) ◦ [α ← τ ] si α n’est pas libre dans τ
?
mgu({τ = α} ∪ C) = mgu(C[α ← τ ]) ◦ [α ← τ ] si α n’est pas libre dans τ
? ? ?
mgu({τ1 → τ2 = τ10 → τ20 } ∪ C) = mgu({τ1 = τ10 ; τ2 = τ20 } ∪ C)
? ? ?
mgu({τ1 × τ2 = τ10 × τ20 } ∪ C) = mgu({τ1 = τ10 ; τ2 = τ20 } ∪ C)
Dans tous les autres cas, mgu(C) échoue et C n’a pas de solutions.
31
Exemple: on considère le jeu d’équations obtenus dans l’exemple de la section 3.2.1. La solution
principale est
αx ← bool αe ← bool
αa ← αy → int αc ← αy → int
αd ← int
Les autres solutions s’en déduisent en remplaçant αy par un type quelconque.
3. Principalité du type inféré: s’il existe un type τ 0 tel que ∅ ` a : τ 0 , alors I(a) n’est pas err;
au contraire, c’est un type τ , et de plus il existe une substitution θ telle que τ 0 = θ(τ ).
32
Remarquons que les αx sont maintenant des schémas et non plus des types simples.
La résolution des contraintes C(a) est maintenant beaucoup plus difficile qu’un problème
d’unification du premier ordre. En particulier, on ne peut plus résoudre les contraintes d’unification
et les contraintes de généralisation dans n’importe quel ordre.
Exemple: on considère
a = let x = fun y → y in x 1
|{z}
c
| {z }
b
αx = Gen(αb , ∅)
αb = αy → αc
αc = αy
Si l’on résout la première immédiatement, on obtient αx = ∀αb .αb , ce qui n’est clairement pas cor-
rect puisque b a forcément un type fonctionnel. Il faut donc avoir résolu au préalable les contraintes
sur αb et αc avant de calculer αx .
Pour résoudre ce problème, nous allons voir un algorithme qui entremêle construction de con-
traintes et résolution de ces contraintes par unification, en une seule passe sur le programme
d’entrée.
33
• Si a est fun x → a1 :
soit α une nouvelle variable prise dans V
soit (τ1 , ϕ1 , V1 ) = W (E + {x : α}, a1 , V \ {α})
prendre τ = ϕ1 (α) → τ1 et ϕ = ϕ1 et V 0 = V1 .
• Si a est let x = b in c:
soit (τ1 , ϕ1 , V1 ) = W (E, a1 , V )
soit (τ2 , ϕ2 , V2 ) = W (ϕ1 (E) + {x : Gen(τ1 , ϕ1 (E))}, a2 , V1 )
prendre τ = τ2 et ϕ = ϕ2 ◦ ϕ1 et V 0 = V2 .
• Dans tous les cas non couverts par les cas ci-dessus, et en particulier si l’un des appels à
mgu échoue, ou si V est vide lorsqu’on veut prendre une nouvelle variable dedans, on prend
W (E, a, V ) = err.
Exercice de programmation 3.5 Implémenter l’algorithme W et le faire tourner sur des exem-
ples. (On pourra se dispenser du paramètre V et du résultat V 0 , et à la place générer des variables
“nouvelles” en utilisant un compteur.)
34
Proposition 3.4 (Commutation entre Gen et substitution) On dit qu’une variable α est
hors de portée d’une substitution ϕ si ϕ(α) = α et pour tout β 6= α, α n’est pas libre dans ϕ(β).
Soit alors un environnement E, un type τ et une substitution ϕ tels que les variables généralisables
L(τ ) \ L(E) sont toutes hors de portée de ϕ. Alors, Gen(ϕ(τ ), ϕ(E)) = ϕ(Gen(τ, E)).
Démonstration: on remarque qu’une variable α hors de portée de ϕ est libre dans un type ϕ(τ )
si et seulement si elle est libre dans le type d’origine τ . Il s’ensuit L(ϕ(τ )) \ L(ϕ(E)) = L(τ ) \ L(E),
puis le résultat annoncé. 2
Démonstration: (du théorème 3.1) par récurrence structurelle sur a. La preuve utilise de manière
essentielle la stabilité du typage par substitution (proposition 1.2). On donne un cas de base, et
deux cas qui utilisent l’hypothèse de récurrence; les autres cas sont similaires. On reprend les
notations de l’algorithme.
Cas a = x avec x ∈ Dom(E). On a (τ, V 0 ) = Inst(E(x), V ) et ϕ = id . Par définition de Inst, on
a τ ≤ E(x). On peut donc bien dériver E ` x : τ par la règle (inst-var).
Cas a = a1 a2 . Appliquant l’hypothèse de récurrence aux deux appels récursifs de W, on obtient
des dérivations de
ϕ1 (E) ` a1 : τ1 et ϕ2 (ϕ1 (E)) ` a2 : τ2 .
On applique la substitution µ ◦ ϕ2 à la dérivation de gauche, et µ à celle de droite. Par la proposi-
tion 1.2, il vient:
ϕ(E) ` a1 : µ(ϕ2 (τ1 )) et ϕ(E) ` a2 : µ(τ2 ).
?
Comme µ est un unificateur de {ϕ2 (τ1 ) = τ2 → α}, on a µ(ϕ2 (τ1 )) = µ(τ2 ) → µ(α). On peut donc
dériver par la règle (app)
ϕ(E) ` a1 a2 : µ(α)
C’est le résultat attendu.
Cas a = let x = a1 in a2 . On applique l’hypothèse de récurrence aux deux appels récursifs de
W . Il vient des preuves de
Si nécessaire, on renomme dans la dérivation de gauche les variables généralisées pour qu’elles soient
hors de portée de ϕ2 . On a alors par le lemme 3.4
ϕ(E) ` let x = a1 in a2 : τ2 .
35
Définition: étant données deux substitutions ϕ et ψ et un ensemble de variables V , on dit que
ϕ = ψ hors de V si ϕ(α) = ψ(α) pour toute variable α ∈ / V . On voit facilement que si L(τ ) ∩ V = ∅
et si ϕ = ψ hors de V , alors ϕ(τ ) = ψ(τ ).
Théorème 3.2 (Complétude et principalité de l’algorithme W ) Soit V un ensemble de
variables infini et tel que V ∩ L(E) = ∅. S’il existe un type τ 0 et une substitution ϕ0 tels que
ϕ0 (E) ` a : τ 0 , alors W (E, a, V ) n’est pas err; au contraire, il existe τ, ϕ, V 0 et une substitution θ
tels que
W (E, a, V ) = (τ, ϕ, V 0 ) et τ 0 = θ(τ ) et ϕ0 = θ ◦ ϕ hors de V .
Démonstration: on commence par remarquer que, avec les hypothèses de la proposition, si
(τ, ϕ, V 0 ) = W (a, E, V ) est défini, alors V 0 ⊆ V , V 0 est infini, et les variables de V 0 ne sont
pas libres dans τ et sont hors de portée de ϕ. En conséquence, V 0 ∩ L(ϕ(E)) = ∅.
La preuve du théorème 3.2 est par récurrence structurelle sur a. On donne un cas de base et
trois cas de récurrence; les autres cas sont similaires.
Cas a = x. Puisque ϕ(E) ` x : τ , on a x ∈ Dom(ϕ(E)) et τ ≤ ϕ(E)(x). Ceci entraı̂ne x ∈ Dom(E).
Écrivons E(x) = ∀α1 . . . αn . τx , avec les αi choisies dans V 0 et hors de portée de ϕ0 . Nous avons
donc que W (E, x, V ) est défini et renvoie
τ = τx [α1 ← β1 , . . . , αn ← βn ] et ϕ = id et V 0 = V \ {β1 . . . βn }
pour certaines variables β1 . . . βn ∈ V . Par choix des αi , nous avons ϕ0 (E(x)) = ∀α1 . . . αn . ϕ0 (τx ).
On note ρ la substitution sur les αi telle que τ 0 = ρ(ϕ0 (τx )). On prend
ψ = ρ ◦ ϕ0 ◦ [β1 ← α1 , . . . , βn ← αn ].
On a ψ(τ ) = ρ(ϕ0 (τx )) = τ 0 . D’autre part, toute variable α ∈
/ V n’est ni une des αi , ni une des βi ,
0 0
d’où ψ(α) = ρ(ϕ (α)) = ϕ (α). C’est le résultat annoncé, puisque ϕ = id ici.
Cas a = fun x → a1 . La dérivation initiale se termine par
ϕ0 (E) + {x ← τ20 } ` a1 : τ10
ϕ0 (E) ` fun x → a1 : τ20 → τ10
Prenons α dans V , comme dans l’algorithme. On définit l’environnement E1 et la substitution ϕ01
par
E1 = E + {x ← α} et ϕ01 = ϕ0 + {α ← τ20 }.
On a ϕ01 (E1 ) = ϕ0 (E) + {x ← τ20 }. On applique l’hypothèse de récurrence à a1 , E1 , V \ {α}, ϕ01 et
τ20 . Il vient
(τ1 , ϕ1 , V1 ) = W (a1 , E1 , V \ {α}) et τ10 = ψ1 (τ1 ) et ϕ01 = ψ1 ◦ ϕ1 hors de V \ {α}.
Il s’ensuit que W (E, a, V ) est bien défini. On prend alors ψ = ψ1 . Montrons que cette substitution
ψ convient. On a:
ψ(τ ) = ψ(ϕ1 (α) → τ1 ) par définition de τ dans l’algorithme
= ψ1 (ϕ1 (α) → τ1 ) par définition de ψ
= ϕ01 (α) → ψ1 (τ1 ) parce que α ∈ / V \ {α}
= τ20 → ψ1 (τ1 ) par construction de ϕ01
= τ20 → τ10 par construction de ψ1
36
D’autre part, pour toute variable γ hors de V ,
ϕ0 (E) ` a1 : τ 00 → τ 0 ϕ0 (E) ` a2 : τ 00
ϕ0 (E) ` a1 (a2 ) : τ 0
On a L(τ1 ) ∩ V1 = ∅, d’où ψ1 (τ1 ) = ψ2 (ϕ2 (τ1 )). Posons ψ3 = ψ2 + {α ← τ 0 }. (La variable α, choisie
dans V2 , est hors de portée de ψ2 , et donc ψ3 prolonge ψ2 .) On a:
37
On applique l’hypothèse de récurrence à a1 , E, V , τ 0 et ϕ0 . Il vient
(τ1 , ϕ1 , V1 ) = W (a1 , E, V ) et τ 0 = ψ1 (τ1 ) et ϕ0 = ψ1 ◦ ϕ1 hors de V.
En particulier, ϕ0 (E) = ψ1 (ϕ1 (E)). On vérifie facilement que ψ1 (Gen(τ1 , ϕ1 (E))) est plus général
que Gen(ψ1 (τ1 ), ψ1 (ϕ1 (E))), c’est-à-dire que Gen(τ 0 , ϕ0 (E)). Puisqu’on peut prouver
ϕ0 (E) + {x ← Gen(τ 0 , ϕ0 (E))} ` a2 : τ 00 ,
le lemme 1.4 dit qu’on peut a fortiori prouver
ϕ0 (E) + {x ← ψ1 (Gen(τ1 , ϕ1 (E)))} ` a2 : τ 00 ,
c’est-à-dire
ψ1 (ϕ1 (E) + {x ← Gen(τ1 , ϕ1 (E))}) ` a2 : τ 00 .
On applique l’hypothèse de récurrence à a2 , dans l’environnement ϕ1 (E) + {x ← Gen(τ1 , ϕ1 (E))},
avec les variables V1 , le type τ 00 et la substitution ψ1 . Il vient
(τ2 , ϕ2 , V2 ) = W (a2 , ϕ1 (E) + {x ← Gen(τ1 , ϕ1 (E))}, V1 )
et τ 00 = ψ2 (τ2 ) et ψ1 = ψ2 ◦ ϕ2 hors de V1 . L’algorithme prend τ = τ2 et ϕ = ϕ2 ◦ ϕ1 et V 0 = V2 .
Montrons que ψ = ψ2 convient. On a bien ψ(τ ) = τ 00 . Et si α ∈ / V , a fortiori α ∈
/ V1 , et donc:
ψ(ϕ(α)) = ψ2 (ϕ2 (ϕ1 (α)))) par définition de ϕ
= ψ1 (ϕ1 (α)) parce que ϕ1 (α) ∈ / V1 , puisque α hors de portée de ϕ1
0
= ϕ (α) parce que α ∈ / V.
D’où ϕ0 = ψ ◦ ϕ hors de V , comme annoncé. 2
38
Exemple: avec la règle (let-subst), on a
parce que ∅ ` fun x → x : string → string (ou tout autre type à la place de string), d’une part,
et de l’autre ∅ ` ((fun x → x) 1, (fun x → x) true) : int × bool.
Une fois (let-gen) remplacée par (let-subst), l’environnement de typage E ne contient plus que
les identificateurs liés par fun (ceux liés par let ne sont jamais ajoutés à E). Donc, nous n’avons
plus besoin de schémas de types: il suffit de dire que E fait correspondre des types simples τ aux
identificateurs x, comme dans le système de types monomorphe. De même, la règle (var-inst) n’est
plus nécessaire, et nous pouvons la remplacer par l’axiome (var) du système monomorphe:
E ` x : E(x) (var)
Nous sommes donc ramenés à un système de types essentiellement monomorphe (le système de la
section 1.3.2 plus la règle (let-subst)), auquel nous pouvons appliquer les techniques de la section 3.2:
génération d’équations entre types simples et résolution par unification. En particulier, les équations
à générer pour une construction let sont les suivantes:
?
si a = let x = b in c, C(a) = C(b) ∪ C(c[x ← b]) ∪ {αa = αc[x←b] }
(Remarque: ceci n’est pas tout à fait exact, car nous avions supposé pour définir C(a) que tous
les identificateurs liés dans a avaient des noms différents, et ce n’est certainement pas le cas pour
a = c[x ← b]. Par exemple, si b = fun y → y et c = x x, nous avons a = (fun y → y) (fun y → y),
dans laquelle y est liée deux fois. Pour être tout à fait correct, il faut considérer les expressions
de mini-ML à α-conversion près, en s’autorisant à renommer les identificateurs liés par let et
fun comme dans le λ-calcul. Puis il faut interpréter c[x ← b] dans la formule ci-dessus comme
“l’expression c dans laquelle chaque occurrence de x est remplacée par une copie de b dans laquelle
on a renommé tous les identificateurs liés par de nouveaux identificateurs”. Dans l’exemple, cela
donnerait c[x ← b] = (fun y 0 → y 0 ) (fun y 00 → y 00 ).)
Pour justifier complètement l’approche décrite ci-dessus, il faut encore montrer que le système
de type ML monomorphe + la règle (let-subst) type exactement les mêmes programmes que ML
polymorphe (tout programme bien typé dans l’un des systèmes est bien typé avec le même type
dans l’autre). C’est une conséquence du théorème suivant:
Démonstration: (esquissée). La partie “seulement si” est une conséquence du lemme 2.2. Pour
la partie “si”, on montre à l’aide du théorème de principalité de W (théorème 3.2) qu’il existe un
type τ0 qui est principal pour a1 dans E: c’est-à-dire, E ` a : τ0 , et de plus pour tout type τ 0 tel
que E ` a : τ 0 , il existe une substitution ψ telle que τ 0 = ψ(τ0 ) et Dom(ψ) ⊆ L(τ ) \ L(E). On prend
alors σ = Gen(τ0 , E), et on montre par récurrence structurelle sur a que si E + E 0 ` a2 [x ← a1 ] : τ
avec Dom(E) ∩ Dom(E 0 ) = ∅, alors E + {x : σ} + E 0 ` a2 : τ . 2
39
Il faut noter que l’algorithme d’inférence à base de (let-subst) décrit dans cette section, bien
que produisant les mêmes résultats que l’algorithme W , est cependant beaucoup moins efficace:
sur let x = a1 in a2 , l’algorithme W type a1 une seule fois, alors que l’algorithme avec (let-subst)
re-type a1 autant de fois que x est utilisé dans a2 . L’algorithme W est également préférable en
pratique car il fournit des messages d’erreurs qui sont directement reliés au source du programme.
Voici un exemple simple de programme de taille O(n) dont le type principal est de taille O(2n ) si
représenté par un arbre:
Malgré cette complexité extrêmement élevée, l’algorithme W est très efficace en pratique (em-
piriquement, quasi-linéaire en la taille du programme source). Ceci est dû au fait que les pro-
grammes réalistes ne ressemblent pas à l’exemple ci-dessus.
40
Chapter 4
Nous décrivons dans ce chapitre quelques traits du “vrai” langage ML qui s’ajoutent facilement à
mini-ML. D’autres traits plus difficiles à ajouter sont décrits dans les chapitres suivants.
E ` a1 : τ1 ... E ` an : τn
E ` (a1 , . . . , an ) : τ1 × . . . × τn
Les résultats des chapitres 2 et 3 s’étendent sans problèmes aux n-uplets. En particulier, les
hypothèses H0, H1, H2 du chapitre 2 sont vérifiées.
Exercice 4.1 (*)/(**) Une autre manière de traiter les n-uplets est de les encoder par des paires
imbriquées: (a1 , . . . , an ) est vu comme une abréviation pour (a1 , (a2 , (a3 , . . . , (an−1 , an )))).
(*) Définir la projection proji,n en termes de fst et snd.
(**) On note M Lt le langage mini-ML avec tuples “primitifs” (non encodés) et M Lp le langage
mini-ML avec paires “primitives” et tuples encodés comme expliqué précédemment. Formaliser la
traduction T des programmes de M Lt dans M Lp , et montrer qu’elle commute avec la réduction: si
41
∗
a → a0 dans M Lt , alors T (a) → T (a0 ) dans M Lp . Réciproquement, est-il vrai que si T (a) → a00 ,
alors il existe a0 tel que a → a0 et a00 = T (a0 )?
Exemples: un type num regroupant nombres entiers et nombres en virgule flottante s’écrit
Un autre exemple est la syntaxe abstraite des expressions mini-ML, comme dans les exercices de
programmation.
Les types concrets peuvent être paramétrés par un ou plusieurs types, ainsi les types option et
list:
type (α1 , . . . , αn ) t = C1 of τ1 | . . . | Cp of τp
α1 . . . αn sont les paramètres du type t. (Dans le cas fréquent n = 0, on écrit juste type t = . . ..)
C1 . . . Cm sont les constructeurs du type t.
τ1 . . . τn sont les types des arguments des constructeurs.
(On convient de représenter les constructeurs constants comme des constructeurs of unit, où unit
est un type muni d’une seule valeur notée ().)
On impose que L(τi ) ⊆ {α1 , . . . , αn } pour tout i.
La déclaration ci-dessus étend le langage de la manière suivante:
Opérateurs: op ::= . . . | C1 | . . . | Cp | Ft
Expressions de types: τ ::= . . . | (τ1 , . . . , τn ) t
Valeurs: v ::= . . . | C1 (v) | . . . | Cp (v)
42
Contextes: Γ ::= . . . | C1 (Γ) | . . . | Cp (Γ)
L’opérateur Ft est l’opérateur de filtrage associé au type t. Il permet de discriminer sur une valeur
de type t suivant son constructeur de tête. Le filtrage qui s’écrit en ML
Ck : ∀α1 . . . αn . τi → (α1 , . . . , αn ) t
Ft : ∀α1 , . . . , αn , β. ((α1 , . . . , αn ) t × (τ1 → β) × . . . × (τn → β)) → β
Les résultats des chapitres 2 et 3 s’appliquent presque immédiatement à cette extension de mini-
ML. En particulier, l’hypothèse H1 de la page 22 est satisfaite, ce qui garantit la préservation des
types pendant la réduction.
Le seul point délicat est que nous avons maintenant des applications d’opérateurs qui sont des
valeurs et donc ne se réduisent pas: les applications de constructeurs Ck (v). Il faut donc modifier
l’hypothèse H2 de la page 22 de la manière suivante:
ε
H2’ Si ∅ ` op v : τ et op v n’est pas une valeur, alors il existe a0 telle que op v → a0 par une
δ-règle.
43
Il est facile de voir que cette modification de H2 n’invalide pas la preuve du lemme de progression
(proposition 2.6).
Exercice de programmation 4.1 Ajouter les n-uplets et les types concrets à l’un des évaluateurs
mini-ML écrits précédemment (programmes 1.1 ou 2.1).
Exercice 4.2 (*) Montrer que les booléens et l’expression conditionnelle if...then...else sont
des cas particuliers de types concrets.
Exercice 4.3 (*) Justifier la restriction L(τi ) ⊆ {α1 , . . . , αn } sur les types des arguments de con-
structeurs dans la déclaration type. (On montrera que le typage n’est pas sûr si cette restriction
est levée.)
type t = C of t → t
Quelles sont les valeurs de ce type? Montrer qu’il existe deux fonctions totales enrouler : (t →
t) → t et dérouler : t → (t → t). Utiliser ces fonctions pour donner un codage des termes du
λ-calcul pur (non typé) sous forme d’expressions de type t. Est-ce que mini-ML sans opérateur de
point fixe fix mais avec les types concrets est normalisant?
Exercice 4.5 (***) Le langage ML offre des mécanismes de filtrage plus puissants que l’opérateur
de filtrage Ft utilisé ci-dessus. En particulier, on peut tester non seulement sur le constructeur de
tête d’une valeur, mais aussi sur d’autres parties de la valeur. Exemple:
Cette expression renvoie 0 pour les listes vides, 1 pour les listes à un élément, et 2 pour les autres
listes. Pour faire le même calcul en mini-ML, il faut emboı̂ter deux filtrages Flist comme suit:
Flist (l, (fun v → 0), (fun l1 → Flist (l1, (fun v’ → 0), (fun l2 → 2))))
44
4.3 Les enregistrements déclarés
Les enregistrements (records) sont des n-uplets dont les composantes sont nommées (par des
étiquettes) au lieu d’être repérées par position. En Caml, ils sont traités de manière similaire
aux types concrets.
Mt : ∀α1 . . . αn . τ1 × τ2 × . . . × τp → (α1 , . . . , αn ) t
.étiqk : ∀α1 . . . αn . (α1 , . . . , αn ) t → τk
ε
.étiqk (Mt (v1 , . . . , vp )) → vk
Remarque: en fait, l’ordre des étiquettes dans l’expression Caml {étiq1 = a1 ; . . . ; étiqp = ap }
n’est pas forcément le même que dans la déclaration du type t. Pour refléter ce fait, il faut
déterminer le type t et la permutation σ sur {1, . . . , p} tels que t est déclaré comme {étiqσ(1) :
τ1 ; . . . ; étiqσ(p) : τp } et traduire l’expression Caml ci-dessus en Mt (aσ−1 (1) , . . . , aσ−1 (p) ).
Remarque: ce traitement des enregistrements fait qu’une étiquette donnée ne peut appartenir à
plusieurs types enregistrement simultanément. Nous verrons au chapitre 6 un traitement beaucoup
plus souple des enregistrements.
45
4.4 Les contraintes de types
En ML, l’expression (a : τ ) s’évalue comme a, mais force a à avoir le type τ . En mini-ML, on peut
voir (a : τ ) comme une application d’opérateur contrτ (a). Les opérateurs contrτ (un par type τ )
se typent et s’évaluent comme suit:
Si τ contient des variables de types, cette présentation ne force pas a à avoir exactement le type τ ,
mais assure que le type de a est une instance ϕ(τ ). Ainsi, (1 : α) est correct et a le type int. Ce
comportement est celui adopté en Caml, mais Standard ML par exemple exige que a ait exactement
le type τ . Ce dernier comportement ne peut s’exprimer en terme d’applications d’opérateurs; il
faut une règle de typage spéciale.
46
Chapter 5
La programmation impérative
Dans ce chapitre, nous étendons mini-ML avec plusieurs traits caractéristiques des langages
impératifs: la modification en place de variables et de structures de données, et les exceptions.
Une référence liée à un identificateur joue le même rôle qu’une variable dans un langage impératif.
Par exemple, voici une fonction gensym qui renvoie un entier différent à chaque appel:
(La construction a; b évalue a, puis b, et renvoie la valeur de b. On peut la voir comme une
abrévation pour let x = a in b où x n’est pas libre dans b.)
Une structure de données (liste, arbres, etc) contenant des références modélise une structure de
donnée mutable (modifiable en place). Par exemple, on peut représenter les tableaux (mutables)
par des listes (immuables) dont chaque élément est une référence (mutable).
47
type α tableau = α ref list
let rec nième l n = match l with Cons(x, l’) → if n = 0 then x else nième l’ (n-1)
let lire_élément t i = !(nième t i)
let écrire_élément t i v = (nième t i) := v
De même, une liste simplement chaı̂née dont on peut modifier le chaı̂nage en place s’écrit:
let f = fun n →
let r = ref(fun x → 0) in
r := fun x → if x = 0 then 1 else x * (!r)(x-1);
(!r)(n)
Exercice 5.2 (***) Montrer que l’on peut définir le combinateur de point fixe fix à l’aide des
références.
let r = ref 1 in r := 2; !r
Les deux occurrences de r correspondent à la même référence, allouée une fois pour toute par le
ref 1 en partie gauche du let. Si nous effectuons naı̈vement une étape de β-réduction sur cette
expression, nous obtenons:
(ref 1) := 2; !(ref 1)
48
Ce terme a un comportement tout à fait différent du premier: il alloue deux références distinctes
initialisées à 1, modifie la première, et lit la seconde. Il faut donc trouver une sémantique plus fine
que la simple β-réduction sur les termes du langage source.
Pour étendre aux références la sémantique à réduction de la section 2.2, nous formalisons la
notion d’adresse mémoire et d’état mémoire. On se donne un ensemble infini d’adresses mémoires
(locations en anglais), notées `. Un état mémoire (store) s est une fonction partielle des adresses
mémoires dans les valeurs. Les expressions et leurs valeurs possibles sont:
Expressions: a ::= . . . comme précédemment
|` adresse mémoire
Valeurs: v ::= fun x → a valeurs fonctionnelles
|c valeurs constantes
| op primitives non appliquées
| (v1 , v2 ) paire de deux valeurs
|` adresse mémoire
En particulier, une référence s’évalue en son adresse mémoire ` associée. Les programmes initiaux
ne contiennent pas d’adresses mémoire `; ces dernières apparaissent lorsqu’on évalue une création
de référence ref(a).
La relation de réduction devient alors a / s → a0 / s0 (lire: “dans l’état mémoire initial s,
l’expression a se réduit en l’expression a0 , et l’état mémoire à la fin de la réduction est s0 ”). Les
règles définissant la relation de réduction sont les suivantes:
ε
(fun x → a) v / s → a{x ← v} / s (βf un )
ε
(let x = v in a) / s → a{x ← v} / s (βlet )
ε
ref(v) / s → ` / s + {` ← v} si ` ∈
/ Dom(s) (δref )
ε
!` / s → s(`) / s si ` ∈ Dom(s) (δderef )
ε
:= (`, v) / s → ( ) / s + {` ← v} si ` ∈ Dom(s) (δaf f )
ε
a1 / s1 → a2 / s2
(contexte)
Γ(a1 ) / s1 → Γ(a2 ) / s2
Pour les opérateurs qui proviennent de mini-ML “pur” (arithmétique, fst, snd, fix, . . . ), il
ε ε
suffit de transformer leurs δ-règles a1 → a2 en a1 / s → a2 / s. En effet, la réduction de ces
opérateurs ne dépend pas de l’état mémoire, et ne modifie pas non plus l’état mémoire. On a ainsi,
par exemple:
ε
+ (n1 , n2 ) / s → n / s si n1 , n2 entiers et n = n1 + n2 (δ+ )
ε
fst (v1 , v2 ) / s → v1 / s (δf st )
ε
snd (v1 , v2 ) / s → v2 / s (δsnd )
49
Exemple: on a la séquence de réductions suivante:
Exercice 5.3 (*) Donner une sémantique opérationnelle “grands pas” (dans le style de la section
v
1.2) pour mini-ML + références. (Indication: la relation d’évaluation est de la forme a/s → v /s0 .)
let r = ref(fun x → x) in
r := (fun x → +(x,1));
(!r) true
r reçoit le type polymorphe ∀α. (α → α) ref. L’affectation r := (fun x → +(x,1)) est donc bien
typée (on utilise r avec l’instance (int → int) ref), ainsi que l’application (!r) true (on utilise
r avec l’instance (bool → bool) ref). L’expression ci-dessus est donc bien typée. Pourtant, sa
réduction se bloque sur +(true, 1) qui n’est ni une valeur, ni réductible. Ce phénomène s’appelle
“le problème des références polymorphes” dans la littérature.
50
Analyse du problème: esquissons une “preuve” de sûreté du typage pour voir précisément le
problème. Pour étendre les preuves du chapitre 2, il faut savoir typer les étapes intermédiaires de
la réduction, et donc les expressions contenant des adresses mémoire `. Nous traitons les adresses
mémoires comme des identificateurs: l’environnement de typage E associe des types aux adresses
mémoire. Ces types peuvent être des schémas ou des types simples.
Si E associe des schémas σ aux adresses `: la règle de typage pour les adresses ` est alors la
même que pour les identificateurs “normaux”, à savoir:
τ ≤ E(`)
(loc-inst)
E``:τ
Cette approche n’est clairement pas sûre, car il suffit qu’une adresse ` reçoive un schéma de type
non trivial ∀α.τ [α] pour que l’on puisse écrire dans ` une valeur d’un certain type τ [int] [Link]., puis
relire cette même valeur en prétendant qu’elle est d’un autre type τ [bool] [Link]. (C’est ce qui se
passe dans l’exemple ci-dessus.)
Si E associe des types simples τ aux adresses `: la règle de typage des adresses est alors:
E ` ` : E(`) (loc)
Il est maintenant impossible d’utiliser une référence avec plusieurs types différents: on est certain
que les valeurs écrites dans ` puis relues depuis ` auront toutes le même type E(`). Le typage des
opérations ! et := redevient sûr. En revanche, la généralisation des types au moment du let pose
problème: le typage n’est pas préservé par la réduction δref . Considérons
Cette expression est bien typée puisque ref(fun x → x) a le type (α → α) ref et α est généralisable
car non libre dans l’environnement de typage. Après réduction de ref(fun x → x), on obtient le
terme let r = ` in (!r)(1); (!r)(true) dans l’état mémoire {` ← fun x → x}. Cependant, ce terme
n’est plus typable: il faudrait que
mais cela n’est pas possible car α est libre dans l’environnement de typage (dans le type de `) et
donc n’est plus généralisable.
51
5.4 Restreindre la généralisation aux expressions non expansives
La manière la plus simple d’assurer la propriété ci-dessus, et donc d’assurer la sûreté du typage des
références, est de ne généraliser que les types des expressions qui sont non-expansives, c’est-à-dire
dont la forme même garantit que leur évaluation ne crée pas de références:
let r = ref(fun x → x) in
r := (fun x → +(x,1));
(!r) true
est maintenant rejeté, car ref(fun x → x) n’est pas non-expansive, et donc r reçoit le type
simple (α → α) ref avec α non généralisé. α est unifié avec int lorsqu’on type la seconde ligne de
l’exemple, et la troisième ligne (!r) true est donc mal typée.
Les exemples suivants restent bien typés car l’expression liée par let est non-expansive:
En effet, l’expression k 1 n’est pas non-expansive, et donc f reçoit le type simple α → int où α
est non généralisée, et donc f ne peut être utilisée de manière polymorphe par la suite. Pour faire
“passer” cet exemple, le programmeur doit manuellement faire une étape d’eta-expansion sur f:
52
let k = fun x → fun y → x in
let f = fun x → k 1 x in
(f 2, f true)
De manière générale, une étape d’eta-expansion permet de rendre non-expansive (et donc
généralisable) toute définition de fonction résultant d’un calcul (comme l’application k 1 ci-dessus).
La raison pour laquelle toute application de fonction est considérée comme potentiellement
expansive est qu’elle peut cacher (de manière plus ou moins évidente) la création de références.
Voici un exemple de création “évidente”:
let f x = ref(x) in
let r = f(fun x → x) in ...
Voici un exemple nettement moins évident, où la référence est encapsulée dans une paire de fonc-
tions, l’une pour écrire dans la référence, l’autre pour lire son contenu courant:
let ref_fonctionnelle =
fun x →
let r = ref x in ((fun newx → r := newx), (fun ( ) → !r)) in
let p = ref_fonctionnelle(fun x → x) in
let écrire = fst(p) in
let lire = snd(p) in
écrire(fun x → +(x,1));
(lire()) true
ref_fonctionnelle a le type ∀α. α → (α → unit) × (unit → α). Bien que ce type ne mentionne
aucun type ref, le résultat de ref_fonctionnelle est cependant fonctionnellement équivalent
à α ref. Si le résultat de ref_fonctionnelle(fun x → x) était généralisé, le reste du pro-
gramme serait bien typé et provoquerait une erreur à l’exécution. Il est donc crucial de considérer
l’application ref_fonctionnelle(fun x → x) comme expansive.
Remarque: les expressions qui sont des valeurs sont également non-expansives. Une présentation
plus simple mais plus restrictive de la règle de typage du let est donc:
Cette approche s’appelle le polymorphisme restreint aux valeurs (value restriction on polymor-
phism) dans la littérature. Nous préférons introduire une notion distincte d’expression non expan-
sive, car cela permet de typer un peu plus de programmes, comme par exemple:
53
La restriction de la généralisation est-elle gênante? En pratique, très rarement, car presque
toutes les expressions polymorphes “utiles” sont des définitions de fonctions fun x → a. Dans les
rares cas où une fonction polymorphe est le résultat d’un calcul (d’une application de fonction [Link].),
une étape d’eta-expansion permet d’obtenir un programme équivalent et typable (voir l’exemple
avec k ci-dessus).
Exercice 5.4 (**) Trouvez un exemple où l’eta-expansion rendue nécessaire par la restriction de
la généralisation change le comportement du programme ou le rend moins efficace. (***) Essayez
de trouver un tel exemple qui soit réaliste (qu’on pourrait rencontrer dans un programme réel).
Définition: on dit qu’un état mémoire s est bien typé dans un environnement de typage étendu
E, et on écrit E ` s, si ` ∈ Dom(s) ⇔ ` ∈ Dom(E) et pour toute adresse ` ∈ Dom(s), il existe τ
tel que E(`) = τ ref et E ` s(`) : τ .
Remarquons que cette notion d’être “moins typable que” étend celle de la section 2.3.1, comme le
montre la proposition suivante.
54
Démonstration: soient E et τ tels que E ` a1 : τ et E ` s. Par hypothèse a1 v a2 , nous avons
E ` a2 : τ . Si a1 est non-expansive, a2 l’est aussi, et donc a1 / s v a2 / s par définition de v. Si a1
est expansive, nous prenons E 0 = E et nous avons bien E 0 ` a2 : τ et E 0 ` s; donc, a1 / s v a2 / s
par définition de v. 2
∗
Théorème 5.1 (Sûreté du typage) Si ∅ ` a : τ et a / ∅ → a0 / s0 et a0 / s0 est en forme normale
vis-à-vis de →, alors a est une valeur.
Le théorème de sûreté se prouve par une séquence de lemmes analogues à ceux utilisés au
chapitre 2.
ε
Proposition 5.2 (Préservation du typage par réduction de tête) Si a1 / s1 → a2 / s2 , alors
a1 / s1 v a2 / s2 .
Démonstration: soient E et τ tels que E ` a1 : τ et E ` s1 . On raisonne par cas sur la règle de
réduction.
Cas des règles βf un , βlet , et toutes les δ-règles du chapitre 2: ces règles ne font pas intervenir
ε
l’état mémoire, c’est-à-dire que s2 = s1 et de plus a1 → a2 est une réduction de mini-ML sans les
références. Appliquant la proposition 2.3, on a donc a1 v a2 (au sens de la section 2.3.1). De plus,
on vérifie facilement par inspection des règles que si a1 est non-expansive, alors a2 l’est aussi:
ε
(fun x → a) v (expansive) → a[x ← v] (indifférent) (βf un )
ε
let x = v in ane (non-expansive) → ane [x ← v] (non-expansive) (βlet )
ε
let x = v in ae (expansive) → ae [x ← v] (indifférent) (βlet )
ε
+ (n1 , n2 ) (non-expansive) → n (non-expansive) (δ+ )
ε
fst (v1 , v2 ) (non-expansive) → v1 (non-expansive) (δf st )
ε
snd (v1 , v2 ) (non-expansive) → v2 (non-expansive) (δsnd )
ε
fix (fun x → a) (expansive) → a{x ← fix (fun x → a)} (indifférent) (δf ix )
(Pour le second cas, nous utilisons le fait que l’ensemble des expressions non-expansives est clos
par substitution de variables par des expressions non-expansives, et a fortiori par des valeurs.)
D’où a1 / s1 v a2 / s1 par la proposition 5.1, et le résultat annoncé car s2 = s1 .
Cas de la règle δref : on a a1 = ref(v) et a2 = ` et s2 = s1 +{` ← v} avec ` ∈
/ Dom(E). Remarquons
que a1 est expansive. Nous avons:
τ1 → τ1 ref ≤ T C(ref)
E ` ref : τ1 → τ1 ref E ` v : τ1
E ` ref(v) : τ1 ref
D’où E ` v : τ1 . Prenons E 0 = E + {` ← τ1 ref}. Puisque E ` s1 , on a bien E 0 ` s2 . De plus,
E 0 ` ` : τ1 ref par la règle de typage des adresses mémoire.
Cas de la règle δderef : on a a1 = !` et a2 = s1 (`) et ` ∈ Dom(s1 ) et s2 = s1 . Par hypothèse
E ` a1 : τ , nous avons
τ ref → τ ≤ T C(!)
E ` ! : τ ref → τ E ` ` : τ ref
E ` !` : τ
55
Comme E ` s1 et E ` ` : τ ref, il s’ensuit que E(`) = τ ref, et donc E ` s1 (`) : τ . On a bien
E ` a2 : τ et E ` s2 comme désiré (car a1 est non-expansive).
Cas de la règle δaf f : on a a1 =:= (`, v) et a2 = ( ) et ` ∈ Dom(s1 ) et s2 = s1 + {` ← v}. Puisque
a1 est bien typée dans E, nous avons la dérivation suivante:
τ ref × τ → unit ≤ T C(:=) E ` ` : τ ref E`v:τ
E ` (:=) : τ ref × τ → unit E ` (`, v) : τ ref × τ
E `:= (!`, v) : unit
Il s’ensuit E(`) = τ ref et donc E ` s2 . Par ailleurs, E ` ( ) : unit trivialement. D’où le résultat
annoncé (a2 est non-expansive). 2
Proposition 5.3 (Croissance de v) Pour tout contexte d’évaluation Γ, a1 /s1 v a2 /s2 implique
Γ(a1 ) / s1 v Γ(a2 ) / s2 .
C’est ce lemme qui ne serait pas vrai sans la restriction de la généralisation (prendre Γ =
let r = [ ] in a et a1 = ref(fun x → x) et a2 = `).
Démonstration: par récurrence structurelle sur Γ. Le seul cas intéressant est Γ = let x =
Γ0 in a. Soient donc E et τ tels que E ` Γ(a1 ) : τ et E ` s1 .
Si Γ0 (a1 ) est non-expansive: on a la dérivation de typage suivante:
E ` Γ0 (a1 ) : τ1 σ = Gen(τ1 , E) E + {x : σ} ` a : τ
E ` let x = Γ0 (a1 ) in a : τ
Appliquant l’hypothèse de récurrence à Γ0 (a1 ), il vient Γ0 (a1 ) / s1 v Γ0 (a2 ) / s2 . Comme Γ0 (a1 ) est
non-expansive, cela signifie que E ` Γ0 (a2 ) : τ1 et E ` s2 , et de plus Γ0 (a2 ) est non-expansive. Par
conséquent, on peut construire la dérivation suivante:
E ` Γ0 (a2 ) : τ1 σ = Gen(τ1 , E) E + {x : σ} ` a : τ
E ` let x = Γ0 (a2 ) in a : τ
E ` Γ0 (a1 ) : τ1 E + {x : τ1 } ` a : τ
E ` let x = Γ0 (a1 ) in a : τ
56
Proposition 5.4 (Préservation du typage par réduction) Si a1 / s1 → a2 / s2 , alors a1 / s1 v
a2 / s2 .
Proposition 5.5 (Forme des valeurs selon leur type) Soit E un environnement qui ne lie
aucun identificateur x mais seulement des adresses `. Supposons E ` v : τ et E ` s.
Démonstration: par examen des règles de typage qui peuvent s’appliquer suivant la forme de τ .
2
Proposition 5.6 (Lemme de progression) Soit E un environnement qui ne lie aucun identifi-
cateur x mais seulement des adresses `. Supposons E ` a : τ et E ` s. Alors, ou bien a est une
valeur, ou bien il existe a0 et s0 tels que a / s → a0 / s0 .
Ainsi, les adresses mémoire ` reçoivent toujours des types sans variables, et on peut lever les
restrictions sur la généralisation au moment du let.
Cette approche présente deux problèmes. Tout d’abord, il est impossible d’écrire des fonctions
polymorphes qui allouent des structures mutables, soit pour les renvoyer en résultat, soit même
pour les utiliser en interne comme des temporaires. Par exemple, la fonction Caml qui transpose
une matrice
57
let transpose m dimx dimy =
let tm = Array.make_matrix dimy dimx in
(* remplir tm *); tm
ne peut recevoir son type naturel ∀α. α array array → α array array, et doit être spécialisée à un
type sans variable particulier, comme float array array → float array array. Pour transposer
des matrices d’entiers, il faudra alors réécrire une autre fonction transpose.
L’autre problème posé par cette approche est que le système de types n’admet plus de types
principaux. Par exemple, fun x → ref(x) admet tous les types τ → τ ref pour τ sans variables,
mais aucun de ces types ne résume tous les autres. En particulier, leur borne supérieure α → α ref
où α est une variable de type n’est pas un type correct pour cette fonction.
fst : ∀αa , βa . αa × βa → αa
snd : ∀αa , βa . αa × βa → βa
! : ∀αa . αa ref → αa
:= : ∀αa . αa ref × αa → unit
En revanche, l’opérateur ref a un schéma de type “impératif”, où la variable quantifiée est
impérative et ne peut être instanciée plus tard que par des types impératifs:
La règle de généralisation du let est alors modifiée pour ne généraliser que les variables applicatives,
mais pas les variables impératives (qui, intuitivement, sont les variables qui ont pu “participer” à
une opération de création de référence polymorphe):
E ` a1 : τ 0 σ = GenAppl(τ 0 , E) E + {x : σ} ` a2 : τ
E ` let x = a1 in a2 : τ
avec GenAppl(τ, E) = ∀αa,1 . . . αa,n . τ où {αa,1 , . . . , αa,n } = La (τ )\La (E) (les variables applicatives
libres dans τ mais pas dans E).
En fait, SML 90 va plus loin et permet la généralisation des variables impératives lorsque
l’expression liée par let est non-expansive.
58
Gen(τ 0 , E)
si a1 non expansive;
E ` a1 : τ 0 σ= E + {x : σ} ` a2 : τ
GenAppl(τ 0 , E) sinon
E ` let x = a1 in a2 : τ
On peut donc voir l’approche de la section 5.4 comme une simplification de celle de SML 90 où
toutes les variables sont traitées comme des variables impératives.
Exemples:
let id = fun x → x in id : ∀αa . αa → αa
let f = id id in f : ∀αa . αa → αa
(f 1, f true) ok
59
Exemple: try 1 + (raise "Hello") with x → x s’évalue en Hello.
Sémantique: La sémantique des exceptions est plus facile à définir que celle des objets muta-
bles, car elle s’exprime directement par réduction des programmes, sans avoir besoin d’un état
mémoire ou autre construction globale. On ajoute simplement les règles de réduction suivantes
pour try...with:
ε
try v with x → a → v
ε
try raise(v) with x → a → a[x ← v]
Il faut aussi ajouter une règle exprimant la propagation des exceptions vers le haut des expressions:
∆(raise(v)) → raise(v) si ∆ 6= [ ]
Dans cette dernière règle, ∆ est un contexte de réduction ne contenant pas de try...with:
Contextes de réduction:
Γ ::= [ ] | Γ a | v Γ | let x = Γ in a | (Γ, a) | (v, Γ) | try Γ with x → a
Contextes d’exceptions:
∆ ::= [ ] | ∆ a | v ∆ | let x = ∆ in a | (∆, a) | (v, ∆)
Les deuxième et troisième règles expriment donc que si l’évaluation d’une sous-expression lève
une exception, l’exécution continue au niveau du try...with le plus proche englobant la sous-
expression.
Typage des exceptions: ML introduit un type concret spécial exn pour le type des valeurs
d’exceptions (les valeurs passées en argument à raise et récupérées par le try...with). On a les
typages suivants:
E ` a1 : τ E + {x : exn} ` a2 : τ
E ` try a1 with x → a2 : τ
exn est un type concret qui comporte un certain nombre de constructeurs prédéfinis, et auquel le
programmeur peut ajouter des constructeurs par la déclaration
exception C of τ
Ceci ajoute un constructeur C : τ → exn. Comme le constructeur de types exn n’a pas de
paramètres, τ ne doit pas comporter de variables libres (voir la section 4.2).
Exercice 5.5 (**) Montrer la sûreté de ce typage. (Indication: on montrera qu’un programme
bien typé ou bien se réduit en une valeur, ou bien se réduit en raise (v), ou bien ne termine pas.)
Exercice 5.6 (***) Montrer qu’il existe des programmes qui ne terminent pas dans mini-ML +
exceptions (mais sans fix, sans types concrets, et sans références). (Indication: on pourrait bien
sûr définir exception C of (exn → exn) et utiliser C comme dans l’exercice 4.4. Il est plus
intéressant de considérer la déclaration exception M of ((int → int) → (int → int)) et de
définir à l’aide de cette exception deux fonctions mettant en correspondance les type (int → int) →
(int → int) et int → int.)
60
5.8 Continuations et opérateurs de contrôle
Pour aller plus loin. Voir Typing first-class continuations in ML, R. Harper, B. Duba, D. MacQueen,
Journal of Functional Programming, 3(4), 1993, et A Generalization of Exceptions and Control in
ML, C. Gunter, D. Rémy, J. Riecke, ACM Conf. on Functional Programming and Computer
Architecture, 1995.
61
Chapter 6
Les enregistrements déclarés à la Caml (comme décrits section 4.3) souffrent de plusieurs limitations:
Nous allons maintenant étudier un système de types pour enregistrements avec les traits suivants:
• Enregistrements polymorphes (ou encore flexibles): on peut définir et typer une fonction
d’accès fun x → x.e qui s’applique à tout type enregistrement possédant un champ de nom
e.
62
Les règles de réduction pour ces opérateurs sont:
ε
({ei = vi }i∈I ).ej → vj si j ∈ I
ε
{ei = vi }i∈I @{ej = w} → {ej = w; ei = vi }i∈I\{j}
La seconde règle s’applique que ej soit ou non déjà liée dans l’enregistrement qu’on étend: si oui,
la valeur w remplace la valeur précédemment liée à ej ); si non, l’enregistrement résultat a une
étiquette de plus. On parle d’extension libre d’enregistrement. L’extension stricte, où l’étiquette
ajoutée ne doit pas être déjà présente dans l’enregistrement initial, s’obtient par la règle:
ε
{ei = vi }i∈I @{ej = w} → {ej = w; ei = vi }i∈I si j ∈
/I
Exemples:
{e : Pre int; f : Abs; g : Abs} est le type des enregistrements à un champ e de type int.
{e : Pre bool; f : Abs; g : Pre int} est le type des enregistrements à deux champs, e de type bool
et g de type int.
{e : Abs; f : Abs; g : Abs} est le type de l’enregistrement vide.
{e : α1 ; f : α2 ; g : α3 } → {e : Pre int; f : α2 ; g : α3 } est le type d’une fonction qui prend n’importe
quel enregistrement en paramètre et l’étend avec un champ e de type int.
63
Règles de typage:
E ` a1 : τ1 ... E ` an : τn {m1 . . . mk } = {e, f, g} \ {e1 . . . en }
E ` {e1 = a1 ; . . . ; en = an } : {e1 : Pre τ1 ; . . . ; en : Pre τn ; m1 : Abs; . . . ; mk : Abs}
64
Types: τ ::= α | T | τ1 → τ2 | τ1 × τ2 comme précédemment
| {τ } type d’enregistrement
|∅ la rangée vide
| e : τ1 ; τ 2 la rangée contenant e : τ1 plus ce que contient la rangée τ2
| Abs le champ est absent (indéfini)
| Pre τ le champ est présent (défini) avec le type τ
Les types sont identifiés modulo les deux équations suivantes:
e1 : τ1 ; e2 : τ2 ; τ = e2 : τ2 ; e1 : τ1 ; τ (commutativité)
∅ = e : Abs; ∅ (absorption)
L’équation de commutativité exprime que l’ordre dans lequel les étiquettes apparaissent dans une
rangée n’a pas d’importance. L’équation d’absoption capture l’intuition que ∅ représente une infinité
d’étiquettes, toutes absentes.
E ` a1 : τ1 ... E ` an : τn
E ` {e1 = a1 ; . . . ; en = an } : {e1 : Pre τ1 ; . . . ; en : Pre τn ; ∅}
Les champs e1 . . . en sont présents avec les types τ1 , . . . , τn ; tous les autres champs sont absents,
d’où le ∅ à la fin de la rangée.
Exemples: la fonction
65
a le type {a : Pre α; b : Pre β; γ} → α × β. En effet, on a {a : Pre α; b : Pre β; γ} = {b : Pre β; a :
Pre α; γ} par l’équation de commutativité, donc les deux projections sont bien typées.
Voici maintenant quelques exemples de typage de l’extension libre. Premier exemple: ajout
d’un nouveau champ.
{a = 1; b = true} @{c = ”foo”}
| {z }
r
L’enregistrement r a le type {a : Pre int; b : Pre bool; ∅}. Utilisant l’absorption puis la commu-
tativité, on transforme ce type en le type équivalent
Ce type est une instance du type argument de extenc , et on obtient comme type du résultat
Il faut voir r avec le type {b : Pre bool; a : Pre int; ∅}, et on obtient comme type du résultat de
l’extension
{b : Pre string; a : Pre int; ∅}
Dernier exemple: extension dans une fonction polymorphe.
fun r → r@{a = 1}
Il faut instancier τ par int dans le schéma de type pour extena . On obtient le type suivant pour
la fonction:
{a : α; β} → {a : Pre int; β}
6.3.3 Sortes
L’algèbre de types enregistrements que nous venons d’introduire contient un certain nombre de
types absurdes, comme par exemple ∅ → ∅ ou Abs × Pre τ ou α → Pre α. Pour les éviter, il
faut s’imposer une certaine discipline dans l’utilisation des expressions de types, afin de ne pas
confondre:
• les types “normaux”, qui peuvent apparaı̂tre comme types d’expressions du langage, [Link].
int ou int → bool;
• les rangées de types, qui peuvent apparaı̂tre à l’intérieur d’un type enregistrement {. . .}, [Link].
∅ ou (e : Abs; . . .).
• les infos de présence Abs et Pre τ , qui peuvent apparaı̂tre comme annotation d’une étiquette
dans une rangée de type.
66
Plus subtilement, l’algèbre de types contient aussi des types contradictoires, comme par exemple
{a : Pre int; a : Abs; ∅} (a ne peut pas être à la fois absent et présent), ou {a : Pre int; a :
Pre bool; ∅} (a ne peut pas être présent avec deux types différents). De tels types permettent de
typer des programmes incorrects, comme par exemple
Cet exemple serait typable si l’on pouvait attribuer à l’argument de f le type {x : Pre int; x :
Pre bool; ∅}.
Pour éviter les types contradictoires, il faut s’imposer de respecter l’invariant suivant dans tous
les typages:
Une même étiquette e doit apparaı̂tre au plus une fois dans un type enregistrement {ϕ}.
De la sorte, on peut parler sans ambiguı̈té de l’information associée à l’étiquette e dans une rangée τ
([Link]. en écrivant τ de manière non ambiguë sous la forme e : τ1 ; τ2 ).
L’invariant ci-dessus est cependant difficile à maintenir, en particulier par substitution de vari-
ables de rangées. Exemple: le type τ = {a : Pre int; ρ} satisfait l’invariant, ainsi que la rangée
ϕ = a : Pre bool; ∅. Cependant, la substitution τ [ρ ← ϕ] ne satisfait pas l’invariant.
La manière rigoureuse d’assurer l’invariant ci-dessus, et aussi d’empêcher l’apparition de types
absurdes, est d’utiliser des sortes (kinds en anglais). Les sortes sont aux types ce que les types sont
aux programmes: de même que les types éliminent des programmes absurdes tels que 1 2, les sortes
éliminent des types absurdes tels que ∅ → ∅ ou {a : Pre int; a : Pre bool; ∅}.
On va donc définir par des règles d’inférence une relation de “sortage” (kinding) ` τ :: κ, qui
signifie “le type τ est bien formé et de la sorte κ”. L’algèbre des sortes pour les enregistrements
est:
Sortes: κ ::= TYPE | PRE | R({e1 , . . . , en })
TYPE est la sorte des types (d’expressions) bien formés. PRE est celle des infos de présence bien
formées. Enfin, R(E), où E est un ensemble d’étiquettes, est la sorte des rangées bien formées et
qui n’associent pas d’information aux étiquettes e ∈ E. Les règles de “sortage” sont les suivantes:
Pour l’axiome ` α :: K(α), on suppose donnée une fonction K qui associe à chaque variable α
sa sorte K(α). Ainsi, chaque variable de type a une sorte unique quelle que soit l’expression de
type dans laquelle elle apparaı̂t.
L’équation d’absorption ∅ = e : Abs; ∅ pose problème car elle ne préserve pas les sortes. En
effet, le membre gauche a toutes les sortes R(E) et peut donc apparaı̂tre dans tout contexte de
67
rangée, alors que le membre droit a les sortes R(E) pour tout E ne contenant pas e, et ne peut
donc pas apparaı̂tre dans une rangée contenant déjà e. Une solution simple est d’annoter ∅ par sa
sorte E:
` ∅E :: R(E)
et de réécrire l’équation d’absorption comme suit:
∅E = e : Abs; ∅E∪{e} si e ∈
/E (absorption)
Proposition 6.1 (Les sortes passent au quotient) Soient τ1 et τ2 deux types et κ une sorte.
Si ` τ1 :: κ et τ1 et τ2 sont égaux modulo les équations, alors ` τ2 :: κ.
Démonstration: il suffit de prouver le résultat pour les membres gauches et droits des deux
équations; il s’étend ensuite à toute expression de type par une récurrence immédiate. Pour l’axiome
de commutativité, supposons ` e1 : τ1 ; e2 : τ2 ; τ :: κ. Vu les règles de sortage, on a κ = R(E) et la
dérivation suivante:
e2 ∈
/ E ∪ {e1 } ` τ2 :: PRE ` τ :: R(E ∪ {e1 , e2 })
e1 ∈
/E ` τ1 :: PRE ` e2 : τ2 ; τ :: R(E ∪ {e1 })
` e1 : τ1 ; e2 : τ2 ; τ :: R(E)
On a donc e1 6= e2 et e1 ∈
/ E et e2 ∈
/ E. En permutant les étapes finales de cette dérivation, on
obtient:
e1 ∈
/ E ∪ {e2 } ` τ1 :: PRE ` τ :: R(E ∪ {e1 , e2 })
e2 ∈
/E ` τ2 :: PRE ` e1 : τ1 ; τ :: R(E ∪ {e2 })
` e2 : τ2 ; e1 : τ1 ; τ :: R(E)
e∈
/E ` Abs :: PRE ` ∅E∪{e} :: R(E ∪ {e})
` e : Abs; ∅E :: R(E)
Le système de sortes ci-dessus garantit l’invariant qu’une même étiquette apparaı̂t au plus une
seule fois dans une expression de type. En effet, supposons que l’étiquette e apparaisse deux fois
dans une rangée τ bien sortée de sorte R(E). Par commutativité, on aurait τ = e : τ1 ; e : τ2 ; τ 0 .
Comme ` τ :: R(E), il faut e ∈/ E et e : τ2 ; τ 0 :: R(E ∪ {e}), mais ceci est impossible car e ∈ E ∪ {e}.
Substitutions et sortes: On dit qu’une substitution θ préserve les sortes si pour toute variable
α, on a ` θ(α) :: K(α). Il est facile de voir que si θ préserve les sortes, alors ` τ :: κ implique
` θ(τ ) :: κ.
68
Schémas et sortes: un schéma de types ∀~
α. τ est bien sorté si et seulement si ` τ :: TYPE.
Proposition 6.2 (Le typage respecte les sortes) Supposons T C(c) bien sorté pour toute con-
stante ou opérateur c, et E(x) bien sorté pour tout identificateur x ∈ Dom(E). Alors, E ` a : τ
implique ` τ :: TYPE.
Démonstration: récurrence facile sur la dérivation de E ` a : τ . Pour les règles (var-inst), (const-
inst) et (op-inst), le résultat découle des hypothèses sur E et T C, et sur le fait que les substitutions
d’instanciation préservent les sortes. Pour la règle (record), le résultat découle de l’hypothèse de
récurrence et du fait que les étiquettes ei sont deux à deux disjointes. Les autres règles se traitent
par application directe de l’hypothèse de récurrence. 2
69
• Montrer que l’hypothèse (H1) est vérifiée pour proje et extene .
• Montrer un lemme de forme des valeurs selon leur type dans le style du lemme 2.5. En
particulier, montrer que si ∅ ` v : {τ }, alors v est une valeur enregistrement, et que si de plus
τ = e : Pre τ1 ; τ2 , alors v contient un champ e associé à une valeur de type τ1 .
6.5.1 Unification
De manière générale, l’ajout d’une théorie équationnelle à une algèbre libre de termes (telle que
l’algèbre des types de mini-ML) peut changer radicalement la nature et les propriétés des problèmes
d’unification. Ainsi, l’ajout d’axiomes d’associativité et de commutativité pour un opérateur bi-
naire + transforme l’unification en résolution d’équations entre mots, et fait perdre l’existence
d’unificateurs principaux.
Le cas des axiomes de commutativité et d’absorption dans les types des enregistrements est
heureusement plus simple, quoique non trivial. En particulier, il ne suffit plus d’examiner les
symboles de tête de deux types à unifier et de déclarer qu’ils ne sont pas unifiables si ces deux
symboles sont différents.
Exemples: les deux types ∅ et e : α; β n’ont pas le même symbole de tête (∅ pour l’un, “;” pour
l’autre), mais sont pourtant unifiables en prenant α ← Abs et β ← ∅, et en appliquant l’axiome
d’absorption.
De même, les types e : Pre int; α et f : Pre bool; β peuvent sembler non-unifiables au premier
abord (car l’un commence par e : . . . et l’autre par f : . . .), mais sont pourtant unifiables par la
substitution
α ← f : Pre bool; γ β ← e : Pre int; γ
où γ est une nouvelle variable. En effet, en appliquant cette substitution aux deux types, on obtient
les types
e : Pre int; f : Pre bool; γ et f : Pre bool; e : Pre int; γ
qui sont bien égaux modulo commutativité. Plus généralement, pour unifier deux types enreg-
istrement se terminant par des variables différentes {. . . ; α} et {. . . ; β}, on commute les étiquettes
de manière à mettre en premier les étiquettes communes aux deux types:
{e1 : τ1 ; . . . ; en : τn ; f1 : ϕ1 ; . . . ; fk : ϕk ; α}
{e1 : τ10 ; . . . ; en : τn0 ; g1 : ψ1 ; . . . ; gm : ψm ; β}
70
Ensuite, on effectue la substitution “croisée”
α ← g1 : ψ1 ; . . . ; gm : ψm ; γ
β ← f1 : ϕ1 ; . . . ; fk : ϕk ; γ
Algorithme d’unification: soit C un ensemble d’équations entre types bien sortées (c’est-à-
?
dire, pour toute équation τ1 = τ2 dans C, il existe une sorte κ telle que ` τ1 :: κ et ` τ2 :: κ).
L’unificateur principal mgu(C) se calcule par l’algorithme suivant. Les premiers cas sont identiques
à ceux de la section 3.2.3 (unification entre types “normaux”, sans équations):
mgu(∅) = id
?
mgu({α = α} ∪ C = mgu(C)
?
mgu({α = τ } ∪ C) = mgu(C[α ← τ ]) ◦ [α ← τ ] si α n’est pas libre dans τ
?
mgu({τ = α} ∪ C) = mgu(C[α ← τ ]) ◦ [α ← τ ] si α n’est pas libre dans τ
? ? ?
mgu({τ1 → τ2 = τ10 → τ20 } ∪ C) = mgu({τ1 = τ10 ; τ2 = τ20 } ∪ C)
? ? ?
mgu({τ1 × τ2 = τ10 × τ20 } ∪ C) = mgu({τ1 = τ10 ; τ2 = τ20 } ∪ C)
? ?
mgu({ {τ1 } = {τ2 } } ∪ C) = mgu({τ1 = τ2 } ∪ C)
Dans le dernier cas, α est choisie non libre dans le système d’équations initiale et de la sorte qui
va bien pour préserver le bon “sortage” des équations. C’est-à-dire, si R(E) est la sorte commune
à (e : τ1 ; τ10 ) et (f : τ2 ; τ20 ), on choisit α de la sorte R(E ∪ {e; f }).
Enfin, les cas d’unification entre drapeaux de présence sont immédiats:
?
mgu({Abs = Abs} ∪ C) = mgu(C)
? ?
mgu({Pre τ1 = Pre τ 0 } ∪ C) = mgu({τ1 = τ2 } ∪ C)
L’hypothèse que les équations de C sont bien sortées garantit que l’unificateur mgu(C) préserve
les sortes.
71
6.5.2 Inférence de types
Munis de cet algorithme d’unification, il ne nous reste plus qu’à adapter l’algorithme W de la
section 3.3.1 comme suit (ce qui change est souligné):
• Si a est une variable x avec x ∈ Dom(E):
prendre (τ, V 0 ) = Inst(E(x), V ) et ϕ = id .
• Si a est fun x → a1 :
soit α une nouvelle variable de sorte TYPE prise dans V
soit (τ1 , ϕ1 , V1 ) = W (E + {x : α}, a1 , V \ {α})
prendre τ = ϕ1 (α) → τ1 et ϕ = ϕ1 et V = V1 .
• Si a est let x = b in c:
soit (τ1 , ϕ1 , V1 ) = W (E, a1 , V )
soit (τ2 , ϕ2 , V2 ) = W (ϕ1 (E) + {x : Gen(τ1 , ϕ1 (E))}, a2 , V1 )
prendre τ = τ2 et ϕ = ϕ2 ◦ ϕ1 et V = V2 .
• Si a est {e1 = a1 ; . . . ; en = an }:
vérifier que les étiquettes ei sont deux à deux distinctes
soit (τ1 , ϕ1 , V1 ) = W (E, a1 , V )
soit (τ2 , ϕ2 , V2 ) = W (ϕ1 (E), a2 , V1 )
soit . . .
soit (τn , ϕn , Vn ) = W ((ϕn−1 ◦ · · · ◦ ϕ1 )(E), an , Vn−1 )
prendre τ = {e1 : Pre (ϕn ◦ · · · ◦ ϕ2 )(τ1 ); . . . ; en : Pre τn ; ∅} et ϕ = ϕn ◦ · · · ◦ ϕ1 et V = Vn
Dans le cas de l’application a1 a2 , on prend V = V2 \ {α} \ Dom(µ) et non pas juste V = V2 \ {α}
comme dans la section 3.3.1 car maintenant l’algorithme mgu peut introduire de nouvelles variables
de types (dans le cas de deux rangées commençant par des étiquettes différentes), et ces nouvelles
variables doivent être enlevées du résultat V . C’est pour cela que nous enlevons de V toutes les
variables de Dom(µ).
Pour finir, il faut s’assurer que la fonction d’instance triviale respecte les sortes:
72
où β1 , . . . , βn sont n variables distinctes choisies dans V et telles que K(βi ) = K(αi ) pour tout i.
On admettra les résultats de correction et de principalité suivants (analogues aux théorèmes 3.1
et 3.2):
on peut lire
Le seul cas où une vérification de sortes est nécessaire est pour les types fournis par le programmeur,
[Link]. dans des contraintes de types (a : τ ) ou des déclarations de types concrets.
73
6.6 Les sommes ouvertes
De même que les enregistrements polymorphes et extensibles généralisent les enregistrements
déclarés de la section 4.3, on peut généraliser les types concrets de la section 4.2 de façon à ne plus
nécessiter la déclaration préalable du type concret et à pouvoir écrire des fonctions qui s’appliquent
à n’importe quel type somme (type concret) contenant au moins certains constructeurs avec certains
types. Ceci fait l’objet de l’exercice suivant.
Exercice 6.4 (***) On se donne une famille de constructeurs C, C 0 , C1 , C2 , . . . ainsi que pour
chaque constructeur C un opérateur de projection PC et un opérateur de filtrage ouvert FC . Les
règles de réduction pour PC et FC sont:
ε
PC (C(v)) → v
ε
FC (C(v), v1 , v2 ) → v1 v
ε
FC (C 0 (v), v1 , v2 ) → v2 (C 0 (v)) si C 0 6= C
Remarquez que PC ne se réduit pas s’il est appliqué à une valeur C 0 (v) avec C 0 6= C. Autrement dit,
le typage de PC doit garantir que son argument porte le constructeur C et aucun autre. En revanche,
FC est un véritable filtrage en ce sens qu’il teste le constructeur de son premier argument, et appelle
la fonction donnée en second argument ou bien celle donnée en troisième argument suivant que le
constructeur de son premier argument est C ou pas.
Proposer un système de typage aussi flexible que possible pour cette présentation des types
concrets. (Indication: on donnera aux valeurs de types concrets des types de la forme [τ ], où τ
est une rangée construite avec C : ; et ∅ qui décrit tous les constructeurs pouvant apparaı̂tre dans
cette valeur, avec les types de leur argument.) Donner les types des opérateurs C, PC et FC dans
votre système. Quels types votre système donne-t’il aux expressions suivantes?
C(1)
if cond then C(1) else D(true)
fun x → FC (x, fun y → y, fun z → 0)
fun x → FC (x, fun y → y, PD )
74
Chapter 7
La conception d’un système de typage statique sûr pour la programmation par objets pose de sérieux
problèmes. On se fixe comme objectif de garantir statiquement l’absence d’erreurs “message not
understood” correspondant à évaluer obj#m où obj est un objet ne possédant pas la méthode m.
(Ceci s’ajoute bien sûr aux garanties habituelles de sûreté, comme [Link]. qu’on élimine 1(2) ou 1
+ "foo".) Les difficultés proviennent des nombreux traits originaux des objets et des classes, dont
il faut rendre compte:
Une difficulté majeure est de combiner inférence de types et subsomption implicite. La subsomption
est l’acte de considérer une expression a de type τ comme étant d’un super-type τ 0 de τ . Elle est
implicite si le changement de type (de τ à τ 0 ) n’est pas marqué dans le texte du programme, et
explicite sinon — comme par exemple en Objective Caml où la subsomption doit être écrite sous
forme d’une coercion (a : τ :> τ 0 ). On distingue les trois combinaisons suivantes:
1. Subsomption implicite, typage explicite, pas d’inférence de types. On déclare les types des
paramètres des fonctions et des variables locales. C’est l’approche suivie par la plupart des
langages orientés-objets classiques: Java, Eiffel, Modula-3, C++.
2. Subsomption explicite, inférence de types à la ML. C’est l’approche suivie en Objective Caml.
Dans ce cours, nous étudions (2) en détails, car c’est une application directe des rangées de types que
nous avons déjà utilisées au chapitre 6. Nous verrons aussi l’approche (3) dans un cadre simplifié.
Les approches (1) et (3) sont détaillées dans le cours d’option de G. Castagna et F. Pottier.
75
7.1 Un calcul d’objets sans classes
L’approche d’Objective Caml est de traiter les objets comme des enregistrements polymorphes dont
chaque champ correspond à une méthode de l’objet. Les variables d’instance et le paramètre self
sont traités par une sémantique d’auto-application (self-application semantics).
7.1.1 Syntaxe
On commence par étendre mini-ML avec des objets mais pas de classes. La construction d’un objet
se fait donc en listant ses méthodes et ses variables d’instance.
Expressions: a ::= x | c | op | fun x → a | a1 a2
| (a1 , a2 ) | let x = a1 in a2 comme d’habitude
0
| obj(x)h. . . ; val xi = ai ; . . . ; method mj = aj ; . . .i construction d’un objet
Opérateurs: op ::= . . . | #m sélection de la méthode m
On note a#m pour l’application d’opérateur #m a. Ceci correspond à l’appel de la méthode m
de l’objet a.
L’identificateur x dans la construction obj(x)h. . .i correspond au paramètre “self” des méthodes.
Une méthode de cet objet peut donc faire x#m pour rappeler une autre méthode du même objet.
Les variables d’instance sont considérées comme immuables. On peut y mettre des références
comme au chapitre 4 pour modéliser les variables d’instance mutables.
L’auto-application est visible ici par le remplacement de l’identificateur s par l’objet v lui-même
dans le corps aj de la méthode mj . De la sorte, les appels s#m0 présents dans aj feront bien
référence à l’objet v lui-même. Remarquons que l’auto-application est une forme de récursion. Par
exemple, il est facile de définir des fonctions récursives ou mutuellement récursives à l’aide d’un
objet:
76
Contextes:
Γ ::= [ ] | Γ a | v Γ | let x = Γ in a | (Γ, a) | (v, Γ)
| obj(s)h. . . val xi−1 = vi ; val xi = Γ; val xi+1 = ai+1 ; . . . ; method mj = a0j ; . . . ; i
Notons que dans un objet complètement évalué, les variables d’instance sont complètement
évaluées, mais pas les corps des méthodes. En ce sens, la partie “variables d’instance” d’un objet
se comporte comme un n-uplet ou un enregistrement, alors que la partie “méthode” se comporte
comme un corps de fonction (de paramètre s).
Exemples: le type hm : Pre int; n : Pre string; ∅i est le type des objets possédant une méthode
m renvoyant un entier, une méthode n renvoyant une chaı̂ne, et aucune autre méthode. De tels
types “fermés” apparaissent lorsque l’on type la création d’un objet obj(s)h. . .i.
Le type hm : Pre int; αi est le type des objets possédant une méthode m renvoyant un en-
tier, et éventuellement d’autres méthodes (dont le type va instancier α). De tels types “ouverts”
apparaissent naturellement pour les paramètres de fonctions; ainsi,
Théorie équationnelle: comme pour les enregistrements, on considère les types modulo les
équations de commutativité et d’absorption:
m1 : τ1 ; m2 : τ2 ; τ = m2 : τ2 ; m1 : τ1 ; τ (commutativité)
∅ = m : Abs; ∅ (absorption)
Sortes: comme pour les enregistrements, on utilise des sortes pour éviter les types absurdes
hm : int; booli ou contradictoires hm : Pre int; m : Pre bool; ∅i. Le système de sortage est
identique à celui des enregistrements (section 6.3.3).
77
7.1.4 Règles de typage
#m : ∀α, β. hm : Pre α; βi → α
i 6= j ⇒ mi 6= mj E ` vi : τi0 E + {s : τs ; xi : τi0 } ` ak : τk
E ` v : τs
E ` v#mj : τj
78
soit (τ~0 , ϕ2 , V2 ) = W (ϕ1 (E) + {self x : α; val xi : τi }, a~0 , V1 \ {α})
?
soit µ = mgu{ϕ2 (α) = hm1 : Pre τ10 ; . . . ; mk : Pre τk0 ; ∅i}
prendre τ = µ(ϕ2 (α)) et ϕ = µ ◦ ϕ2 ◦ ϕ1 et V = V2 \ Dom(µ).
coerceτ,τ 0 : α. τ → τ 0
∀~ si τ <: τ 0 et α
~ = L(τ ) ∪ L(τ 0 )
ε
coerceτ,τ 0 (v) → v
Remarquez que ces opérateurs coerce généralisent très naturellement les contraintes de types de
ML comme présentées section 4.4.
Relation de sous-typage: La relation de sous-typage <: qui caractérise les opérateurs coerce
valides est définie par les règles d’inférence suivantes:
79
Deux types de base ou deux variables de types sont en relation de sous-typage si et seulement
si ils sont égaux.
Un type objet hτ i est sous-type d’un autre hτ 0 i si toutes les méthodes mentionnées dans la rangée
τ 0 sont également mentionnées dans τ , et leur type dans τ est sous-type de celui dans τ 0 . Si τ 0 se
termine par ∅, la rangée τ peut aussi mentionner des méthodes supplémentaires qui n’apparaissent
pas dans τ 0 (en raison de l’axiome τ <: ∅). En revanche, si τ 0 se termine par une variable de rangée,
τ doit se terminer par la même variable et mentionner les mêmes méthodes que τ 0 .
Pour les types produit, il y a sous-typage si les types des premières composantes sont sous-types,
ainsi que les types des secondes composantes. On dit que le produit est un constructeur de type
covariant en ses deux arguments. Autrement dit, les deux fonctions des types dans les types × τ
et τ × sont des fonctions croissantes pour l’ordre <:.
Enfin, pour le sous-typage entre types flèches, on a covariance en le type du résultat, mais con-
travariance en le type de l’argument: les types arguments doivent être en sous-typage dans l’ordre
inverse du sous-typage entre les types flèche. Autrement dit, la fonction → τ est décroissante,
alors que la fonction τ → est croissante. Ceci se comprend mieux en pensant aux types comme
à des ensembles de valeurs, et à la relation de sous-typage comme à l’inclusion entre ensembles
de valeurs. En théorie des ensembles, on a aussi que A → B (l’ensemble des fonctions de A dans
B) est inclus dans A0 → B 0 (l’ensemble des fonctions de A0 dans B 0 ) si et seulement si A0 ⊆ A et
B ⊆ B0.
E`a:τ τ <: τ 0
(sub)
E ` a : τ0
ε
Avec cette règle, on a bien que la réduction coerceτ,τ 0 (v) → v préserve le typage, puisque v qui a
le type τ par hypothèse a aussi le type τ 0 par application de la règle (sub).
Bien sûr, cette règle (sub) rend l’inférence de types problématique — c’est pour éviter cela que
nous mettons des coercions explicites! Il faut donc typer les programmes source sans la règle (sub),
ce qui permet de faire de l’inférence de types, et n’ajouter la règle (sub) que pour raisonner sur la
préservation du typage pendant la réduction.
80
7.3 Classes
Nous ajoutons maintenant au calcul d’objets une notion de classes avec un mécanisme d’héritage.
Les classes sont des collections de définitions de méthodes et de variables d’instance. Une construc-
tion new explicite permet de prendre une instance d’une classe, c’est-à-dire de construire un objet
ayant les méthodes et les variables indiquées dans la classe. Pour simplifier, nous présentons les
classes comme faisant partie des expressions; dans un langage réaliste, on a tendance à distinguer
un sous-langage de classes distinct du langage des expressions (dans un langage comme Objective
Caml, cela simplifie l’inférence de types).
Autres simplifications: nous traiterons seulement les classes ne contenant pas de variables
d’instances, uniquement des méthodes. Nous ne traitons pas non plus l’héritage multiple. (Voir
l’article de Rémy et Vouillon référencé à la fin de ce chapitre pour un traitement plus complet.)
Expressions: a ::= . . .
| new(a) création d’un objet
| class(x)h. . . mi = ai . . .i définition de classe
| class(x)hinherit(a); m = ai héritage et ajout ou redéfinition d’une méthode
Types: τ ::= . . . | class(τ1 ) τ2 type de classe
ε
new(class(x)hmi = ai i) → obj(x)hmethod mi = ai i
ε
class(x)hinherit(class(y)hmi = ai ii=1...n ); m = ai → class(y)h(mi = ai )i=1...n,mi 6=m ; m = a[x ← y]i
class virtual c =
object(self)
81
method virtual m : int
method n = 1 + self#m
end
reçoit ici le type class(hm : Pre int; αi) hn : Pre int; ∅i.
E ` a : class(τ ) τ
(new)
E ` new(a) : τ
E + {x : τ } ` ai : τi
(classe)
E ` class(x)hmi = ai i : class(τ ) hm1 : Pre τ1 ; . . . ; mk : Pre τk ; ∅i
E ` a1 : class(τx ) hm : Abs; τ i E + {x : τx } ` a2 : τ 0
(exten)
E ` class(x)hinherit(a1 ); m = a2 i : class(τx ) hm : Pre τ 0 ; τ i
E ` a1 : class(τx ) hm : Pre τ 0 ; τ i E + {x : τx } ` a2 : τ 0
(redéf)
E ` class(x)hinherit(a1 ); m = a2 i : class(τx ) hm : Pre τ 0 ; τ i
Pour l’héritage, on a deux règles suivant que l’on ajoute une nouvelle méthode ou que l’on
redéfinit une méthode existant dans la classe héritée. Dans le second cas, la nouvelle définition de
la méthode doit avoir le même type que dans la super-classe.
Dans tous les cas d’héritage, le type de “self” doit être le même dans la nouvelle classe et dans
la classe héritée. Cela garantit que les méthodes héritées qui retournent “self” en résultat restent
bien typées. Ceci ne restreint pas l’expressivité du langage, car en général la classe dont on hérite
est liée à un identificateur, et a donc un schéma de type de la forme
Exemple: voici un fragment d’Objective Caml qui illustre plusieurs points délicats: classe
paramétrée par un type; spécialisation de ce paramètre dans une sous-classe; utilisation de “self-
type” pour typer une méthode qui renvoie “self”.
82
method get = n
method leq obj = self#get <= obj#get
end
let comparable =
class(self) < min = fun y → if self#leq y then self else y > in
let int_comparable =
fun n →
class(self) < inherit(comparable);
method get = n;
method leq = fun obj → self#get <= obj#get >
Une instance du schéma de int_comparable est class(τ 00 ) τ 00 , avec τ 00 = hmin : Pre(τ 00 → τ 00 ); get :
Pre int; leq : Pre(τ 00 → bool); ∅i, ce qui montre que l’on peut faire new(int_comparable).
Cet objet n’est pas typable dans le système de la section 7.1. En effet, le type de l’objet doit avoir
la forme suivante:
τs = hrang : Pre int; min : Pre (τo → τo ); . . .i
mais pour que le if...then...else soit bien typé, il faut τs = τo , et c’est impossible avec notre
algèbre de types car τo est un sous-terme strict de τs .
Pour contourner cette restriction, on peut introduire des types récursifs dans l’algèbre de types.
Intuitivement, un type récursif est une expression de type infinie, comme par exemple int → int →
?
int → . . .. Avec les types récursifs, une équation comme α = τ [α] admet une solution qui est le
type infini τ [τ [τ [. . .]]].
83
7.4.1 Présentations des types récursifs
Il y a plusieurs manières de formaliser rigoureusement les types récursifs:
Limites de suites de types finis: on voit les types récursifs comme des limites de suites
d’approximations finies. Ainsi, int → int → int → . . . est la limite de la suite
int, (int → int), (int → int → int), . . .. L’exercice 7.5 explore cette approche.
Arbres infinis rationnels: de même que les expressions de types normales peuvent être vues
comme des arbres finis (avec des nœuds étiquetés par T , →, ×, α, . . . ), on peut voir les types
récursifs comme des arbres infinis. On impose que ces arbres soient rationnels, c’est-à-dire
comportent un nombre fini de sous-arbres différents.
Graphes: on représente les types comme des graphes finis dont les nœuds sont étiquetés par T ,
→, ×, α, . . . Les types normaux correspondent à des graphes acycliques; les types récursifs,
à des graphes comportant des cycles. L’exercice 7.4 explore cette approche.
Présentation syntaxique avec des µ-types: on enrichit les expressions de types comme suit:
Le type µα. τ est une représentation finie du seul type τ 0 (fini ou infini) qui vérifie l’égalité
τ 0 = τ [α ← τ 0 ].
Par exemple, µα.int → α est le type infini int → int → int → . . .. C’est la seule solution
de l’équation τ 0 = int → τ 0 .
Dans l’exemple min ci-dessus, un type correct pour l’objet est
µα.hrang : Pre int; min : Pre(α → α); ∅i
L’axiome (renommage) exprime que α dans µα. τ est une variable liée et peut être renommée à
volonter. L’axiome (déroulage) permet d’“enrouler” et de “dérouler” un type µ à volonté pour
satisfaire des égalités de types. Elle capture l’idée que µα. τ est une solution de l’équation
?
α = τ . Enfin, la règle d’inférence (unicité) exprime que µα. τ est la seule solution de l’équation
?
α = τ . Donc, si τ1 et τ2 satisfont cette équation, ils sont forcément égaux.
Exemple: les deux types µα. int → α et µα. int → int → α sont égaux, car ils sont tous
?
deux solution de α = int → int → α: en déroulant le premier type deux fois, on a bien
µα. int → α = int → (µα. int → α) = int → int → (µα. int → α)
et en déroulant le second une fois,
µα. int → int → α = int → int → (µα. int → int → α)
84
Présentation syntaxique sous forme de types avec équations: on manipule syntaxique-
ment à la fois des expressions de types et des équations entre variables de types et types.
Par exemple, int → int → . . . est vu comme le type α dans le contexte de l’équation
α = int → α.
Quelle que soit la présentation des types récursifs retenue, on conserve exactement les mêmes règles
de typage que dans le cas non récursif. Simplement, certaines contraintes d’égalité imposées par les
règles sont maintenant satisfiables par des types récursifs, alors qu’elles n’avaient pas de solution
avec les types normaux.
85
7.4.3 Inférence en présence de types récursifs
L’introduction de types récursifs ne modifie pas l’algorithme W , mais nécessite de remplacer
l’unification entre termes finis par de l’unification entre termes rationnels, c’est-à-dire de
l’unification entre graphes.
L’idée de base est de faire comme dans l’algorithme d’unification entre termes, sauf qu’on
?
supprime le test d’occurrence dans le cas α = τ : au lieu de prendre [α ← τ ] si α ∈ / L(τ ) et
d’échouer sinon, on prend dans tous les cas [α ← µα. τ ]. Par l’équation de déroulement, on a bien
µα. τ = τ [α ← µα. τ ]. Remarquez que si α ∈ / L(τ ), on retrouve la même solution que dans le cas
des termes finis, car alors µα. τ = τ .
La difficulté est d’assurer la terminaison de l’algorithme d’unification. Pour ce faire, il faut
introduire des formalismes plus complexes que ceux que nous avons employé jusqu’ici: unification
entre graphes, ou bien multi-équations. L’exercice 7.4 est une introduction à l’unification entre
graphes.
86
Proposition 7.1 La relation H ` <: est transitive.
Règles de typage: les règles de typage sont celles de mini-ML monomorphe (section 1.3.2), plus
une règle pour les objets, une pour les appels de méthodes, et une règle de subsomption implicite.
87
?
• Si a est b#m: C(a) = {αb <: hm : αa i} ∪ C(b).
Remarquons que C(a) est un ensemble d’inéquations entre types finis (il ne contient pas de types
récursifs µα. τ ).
On a:
?
C(a) = { αx → αb <: αa ;
?
αc × αe <: αb ;
?
αd <: hm : αc i;
?
αx <: αd ;
?
αf <: hm0 : αe i;
?
αx <: αf }
Proposition 7.2 (Correction des solutions vis-à-vis du typage) Si ϕ est une solution de
C(a), alors E ` a : ϕ(αa ) où E est l’environnement de typage {x : ϕ(αx ) | x libre dans a}.
Proposition 7.3 (Complétude des solutions vis-à-vis du typage) Soit a une expression.
S’il existe un environnement E et un type τ tels que E ` a : τ , alors le système d’équations
C(a) admet une solution.
88
Au lieu d’essayer de résoudre l’ensemble de contraintes C(a), nous allons simplement établir qu’il
existe une solution de C(a) sans la calculer entièrement. Cela suffit à garantir que le programme a
est bien typé et s’exécute sans erreurs.
On établit la solvabilité (l’existence d’une solution) d’un ensemble de contraintes C en deux
temps: d’abord on calcule la fermeture C ∗ de C; ensuite, on vérifie que C ∗ ne contient pas
d’incohérences immédiates.
Fermeture: on dit qu’un ensemble de contraintes C entre types finis est fermé (par transitivité
et par propagation) s’il satisfait les conditions suivantes:
? ? ?
• Si τ1 <: τ2 ∈ C et τ2 <: τ3 ∈ C, alors τ1 <: τ3 ∈ C.
? ? ?
• Si (τ1 → τ2 ) <: (ϕ1 → ϕ2 ) ∈ C, alors ϕ1 <: τ1 ∈ C et τ2 <: ϕ2 ∈ C.
? ? ?
• Si (τ1 × τ2 ) <: (ϕ1 × ϕ2 ) ∈ C, alors τ1 <: ϕ1 ∈ C et τ2 <: ϕ2 ∈ C.
?
• Si hmi : τi i <: hnj : ϕj i ∈ C, alors τi <: ϕj ∈ C pour tous i, j tels que mi = nj (i.e. pour tous
les noms de méthodes qui apparaissent à la fois dans les deux types objet).
On note C ∗ la fermeture de C, c’est-à-dire le plus petit ensemble fermé contenant C. On l’obtient
à partir de C en ajoutant à C toutes les contraintes nécessaires pour satisfaire les conditions ci-
? ? ? ?
dessus. Par exemple, si τ1 <: τ2 ∈ C et τ2 <: τ3 ∈ C mais τ1 <: τ3 ∈ / C, on ajoute τ1 <: τ3 à C. Le
processus termine forcément, car les contraintes ajoutées sont des contraintes entre types qui sont
des sous-termes de types apparaissant dans l’ensemble initial C, et ces sous-termes sont en nombre
fini.
• τ1 = ⊥;
• τ2 = >;
89
• τ1 = hmi : ϕi i, τ2 = hnj : ψj i, et l’ensemble de noms de méthodes {nj } est inclus dans
l’ensemble des noms de méthodes {mi }.
Un ensemble qui n’est pas immédiatement cohérent est dit immédiatement incohérent.
La réciproque de la proposition précédente n’est pas vraie si C n’est pas fermé. Par exemple,
? ?
{int → int <: α; α <: int × int} est immédiatement cohérent, mais n’admet pas de solutions.
Cependant, si C est fermé, nous avons le théorème suivant (que nous admettrons):
Démonstration: la partie “si” découle des propositions 7.2, 7.4 et 7.5. La partie “seulement si”
est corollaire des propositions 7.3, 7.4 et 7.6. 2
• Didier Rémy et Jérôme Vouillon, Objective ML: An effective object-oriented extension to ML,
Theory And Practice of Object Systems, 4(1):27–50, 1998, [Link]
Projects/cristal/[Link]/objective-ml![Link]
L’approche Objective Caml.
• Roberto Amadio et Luca Cardelli, Subtyping recursive types, ACM Transactions on Program-
ming Languages and Systems, 15(4), 1993, [Link]
Papers/[Link]
La référence sur le sous-typage entre types récursifs.
90
Exercices
Exercice 7.1 (*)/(**) Montrer que la relation de sous-typage (sans types récursifs) est une rela-
tion d’ordre: réflexive (τ <: τ ), transitive (τ1 <: τ2 et τ2 <: τ3 implique τ1 <: τ3 ) et antisymétrique
(τ <: τ 0 et τ 0 <: τ impliquent τ = τ 0 ).
Exercice 7.2 (**)/(***) Montrer le cas βf un de la préservation du typage par réduction de tête
(l’analogue de la proposition 2.3) lorsqu’on ajoute la règle (sub). (Indication: attention, il y a un
piège.)
Exercice 7.3 (*) Montrer que les types récursifs permettent de typer en ML tous les termes du
λ-calcul pur. Quel est le type qu’ont tous les λ-termes?
Exercice 7.4 (**)/(***) Le but de cet exercice est de comprendre la représentation des types
récursifs par des graphes et de programmer l’algorithme d’unification correspondant.
Un graphe de types est un graphe orienté. Chaque noeud est étiqueté ou bien par le symbole
V (signifiant que ce noeud représente une variable de type), ou bien par un constructeur de type
comme int, bool, →, ×. (Pour simplifier, on ne considère pas les types objets.) Chaque noeud
doit avoir un nombre de noeuds fils égal à l’arité A(c) de son étiquette c, avec bien sûr A(V ) =
A(int) = A(bool) = A(∅) = 0 (pas de fils), et A(→) = A(×) = 2 (deux fils). Un noeud du graphe
représente donc une expression de type dont le constructeur de tête est donné par l’étiquette du type
et dont les sous-expressions sont représentées par les fils éventuels de ce noeud. Les types récursifs
apparaissent naturellement sous forme de cycles dans le graphe.
Si n est un noeud du graphe, on note C(n) son constructeur de type et Fi (n) le noeud du ie fils
de n (avec 1 ≤ i ≤ A(C(n))).
Une substitution, dans ce formalisme, est une relation d’équivalence R entre les noeuds du
graphe qui vérifie les propriétés suivantes:
91
et retourne une relation d’équivalence qui est l’unificateur principal.
mgu(∅, R) = R
?
mgu({n = n0 } ∪ E, R) = mgu(E, R) si n R n0
?
mgu({n = n0 } ∪ E, R) = mgu(E, R + {n = n0 }) si C(n) = V ou C(n0 ) = V
? ? ?
mgu({n = n0 } ∪ E, R) = mgu(E ∪ {F1 (n) = F1 (n0 ); . . . ; Fk (n) = Fk (n0 )}, R + {n = n0 })
si C(n) 6= V et C(n0 ) = C(n) et k = A(C(n))
?
mgu({n = n0 } ∪ E, R) = échec si C(n) 6= V et C(n0 ) 6= C(n)
On a noté R + {n = n0 } la plus fine relation d’équivalence qui contient R et qui relie n et n0 . Elle
s’obtient à partir de R en fusionnant les classes d’équivalence de n et n0 dans R.
1) Dessiner les graphes représentant les types suivants:
int → bool; α × β; α × α; µα. int → α; µα. β → γ → α.
2) Faire tourner à la main l’algorithme sur la représentation sous forme de graphe du problème
?
d’unification µα. int → α = µα. β → γ → α. (On partira de la relation identité comme second
paramètre initial de mgu.) Quelle est la forme de la substitution renvoyée?
3) Montrer que si R = mgu(E, id ) (où id est la relation identité) est définie, alors R est une
substitution. Montrer que R est un unificateur de E. Montrer que R est un unificateur principal
de E.
4) Montrer que l’algorithme mgu termine toujours.
Exercice de programmation 7.2 Implémenter l’algorithme d’unification de graphes de
l’exercice précédent. (Indication: on représentera la relation d’équivalence entre noeuds par une
structure de type union-find. C’est-à-dire, on placera dans chaque noeud un champ mutable de
type noeud option, dont la signification est la suivante: si None, cela veut dire que le noeud n’est
encore pas identifié à un autre noeud; si Some(n), cela veut dire que le noeud est dans la même
classe d’équivalence que le noeud n. Au lieu de renvoyer une relation d’équivalence comme résultat
de l’unification, on modifiera en place ces champs mutables types pour représenter cette relation.)
Exercice 7.5 (***, pour mathématiciens) Le but de cet exercice est de justifier mathématiquement
l’existence des types µα. τ . L’idée est de construire les types infinis comme limites de suites conver-
gentes de types finis, de même que Cantor construisit les réels comme limites de suites convergentes
de rationnels.
1) Pour simplifier, on considère uniquement l’algèbre de types τ ::= α | τ1 → τ2 . On définit la
distance d(τ1 , τ2 ) entre deux types (finis) τ1 et τ2 de la façon suivante:
1
d(τ1 → ϕ1 , τ2 → ϕ2 ) = max(d(τ1 , τ2 ), d(ϕ1 , ϕ2 ))
2
d(α, α) = 0
d(α, β) = 1 si α 6= β
d(α, τ2 → ϕ2 ) = 1
d(τ1 → ϕ1 , β) = 1
Montrer que d est une distance ultramétrique, c’est-à-dire qu’elle satisfait l’inégalité du triangle
ultramétrique d(τ1 , τ3 ) ≤ max(d(τ1 , τ2 ), d(τ2 , τ3 )), qu’elle est symétrique, et que de plus d(τ1 , τ2 ) = 0
si et seulement si τ1 = τ2 .
92
2) (Complétion d’un espace métrique.) On considère l’ensemble S dont les éléments sont des
suites de Cauchy de types (τn )n∈N . On rappelle qu’une suite (τn ) est de Cauchy si
∀ε.∃n.∀p, q ≥ n. d(τp , τq ) ≤ ε.
On définit la distance d(s, s0 ) entre deux telles suites s = (τn ) et s0 = (τn0 ) par
a) Montrer que cette limite existe toujours. b) Montrer que la relation entre suites ∼ = définie
par s ∼ = s0 ⇔ d(s, s0 ) = 0 est une relation d’équivalence. c) Montrer que l’ensemble quotient
T = S/ ∼ = muni de la distance d/ ∼ = est un espace ultramétrique. d) Montrer que les types simples
se plongent naturellement dans T et que les distances sont préservées par le plongement. e) Montrer
ou admettre que T est complet (toute suite de Cauchy d’éléments de T converge vers un élement
de T ).
3) (Théorème de Banach-Tarski.) Soit (E, d) un espace métrique complet. Une fonction F de
E dans E est dite contractive s’il existe une constante k ∈ ]0, 1[ telle que d(F (x), F (y)) ≤ k d(x, y)
pour tous x, y ∈ E. Montrer que toute fonction contractive admet un point fixe et que ce point fixe
est unique.
4) Soit α une variable de type et τ ∈ T tel que τ 6= α. Montrer qu’il existe un et un seul τ 0 ∈ T
tel que τ 0 = τ [α ← τ 0 ].
93
Chapter 8
Systèmes de modules
Pour conclure ce cours, nous étendons les systèmes de types vers la programmation modulaire
(programmation à grande échelle). Nous suivons l’approche ML où le système de modules se
présente comme un petit langage fonctionnel typé opérant au-dessus du langage de base. Le langage
de base considéré ici est mini-ML, mais l’approche s’étend facilement à une classe très vaste de
langages de base typés.
94
Types: τ ::= t type nommé
| p.t composante de type d’une structure
| α | T | τ1 → τ2 | τ1 × τ2 comme d’habitude
Schémas de types: σ ::= ∀α1 . . . αn . τ
8.2 Évaluation
8.2.1 Sémantique par traduction
L’évaluation des modules s’exprime très facilement par une traduction dans mini-ML avec enreg-
istrements: on effaçe les composantes de types des structures, on transforme les structures en
enregistrements, et les foncteurs en fonctions. Cette traduction, notée [[· · ·]], est définie par:
[[X]] = X
[[p.X]] = [[p]].X
[[struct d end]] = L(d∗ , {. . . xi = xi ; . . . ; Xj = Xj ; . . .})
∗
L(ε, a) = a
L(let x = a; d∗ , b) = let x = a in L(d∗ , b)
L(type t = T ; d∗ , b) = L(d∗ , b)
L(module X = m; d∗ , b) = let X = [[m]] in L(d∗ , b)
a pour traduction
95
Une solution simple à ce problème est d’autoriser toute expression de module m dans les projec-
tions .x, .t et .X. Autrement dit, on prendrait p ::= m dans la grammaire ci-dessus. Le problème
de cette approche est que les expressions de types p.t deviennent extrêmement compliquées: p
peut être une expression de module arbitrairement complexe. En particulier, il devient difficile
de décider si deux expressions de types p.t et p0 .t représentent le même type: il faudrait réduire
(évaluer) p et p0 pendant le typage pour voir s’ils se réduisent sur des valeurs de modules identiques.
Une telle évaluation pourrait ne pas terminer, rendant le typage indécidable. De manière générale,
nous voulons préserver une certaine distinction de phase entre le typage (pendant la compilation) et
l’évaluation (pendant l’exécution); devoir réduire des expressions pendant le typage brouille cette
distinction.
Une solution intermédiaire, proposée par Harper et Lillibridge, consiste à ajouter à la classe
des chemins d’accès les valeurs de modules, c’est-à-dire les expressions de modules entièrement
évaluées:
Chemins d’accès: p ::= X | p.X | V
Valeurs de modules: V ::= struct d∗V end | functor(X : M ) → a
Définitions entièrement évaluées:: dV ::= let x = v | type t = τ | module X = V
Valeurs du langage de base: v ::= c | op | fun x → a | (v1 , v2 )
Les valeurs de modules, étant déjà entièrement réduites, se comparent simplement par égalité
syntaxique. Cela permet de décider facilement si deux types V1 .t et V2 .t sont identiques.
Dans l’approche Harper-Lillibridge, la grammaire du langage n’est toujours pas stable par
substitution [X ← m] où m est une expression de module arbitraire; mais elle est stable par
substitution [X ← V ] où V est une valeur de module. C’est suffisant pour donner une sémantique
à réduction en appel par valeur:
ε
(struct d∗V ; val x = v; d∗V 0 end) → v (proj-val)
ε
(struct d∗V ; module X=V ; d∗V 0 end) → V (proj-mod)
ε
(functor (X : M ) → m) V → m[X ← V ] βfunctor
ε
(V : M ) → V (contrainte)
Pour tenir compte du fait qu’une composante de structure peut faire référence aux noms des
composantes précédentes ([Link]. struct val x = 1; val y = x + 1 end), il faut ajouter les deux
règles de “propagation” de valeurs suivantes:
ε
struct d∗V ; let x = v; d∗ end → struct d∗V ; let x = v; d∗ [x ← v] end (prop-val)
ε
struct d∗V ; module ∗
X = V ; d end → struct d∗V ; module ∗
X = V ; d [X ← V ] end (prop-mod)
Enfin, pour les réductions en profondeur, on utilise les contextes suivants:
Contextes de modules:
Γm ::= [ ] | Γm .X
| struct d∗V ; let x = Γa ; d∗ end
| struct d∗V ; module X = Γm ; d∗ end
| Γm m | V Γm | (Γ : M )
Contextes d’expressions de base:
Γa ::= [ ] | Γm .x | Γa a | v Γa | (Γa , a) | (v, Γa ) | let x = Γa in a
96
8.3 Règles de typage
Le typage des modules soulève plusieurs difficultés. Premièrement, il faut prendre en compte les
équivalences entre types de base induites par les types manifestes dans les signatures. Par exemple,
si X : sig type t = int end, alors le type X.t est équivalent à int. Dans les chapitres précédents,
nous avons vu plusieurs exemples de théories équationnelles ajoutées à l’algèbre de types. La
différence dans le cas des modules est que les équations ne sont pas fixées une fois pour toute, mais
dépendent des types qui peuvent être donnés aux modules.
La seconde difficulté est de prendre en compte l’oubli d’informations concernant les signatures:
on peut oublier la présence de certains composants; on peut aussi oublier des égalités de types
en voyant un type manifeste comme un cas particulier de type abstrait. Ceci est reflété dans une
relation de sous-typage entre types de modules, avec une règle de subsomption implicite (nous ne
faisons pas d’inférence de types sur le langage de modules).
La dernière difficulté est la prise en compte des dépendances entre composantes de structures,
d’une part, et de l’autre entre l’argument et le résultat d’un foncteur. Par exemple, le foncteur
functor (X : sig type t end) → struct type u = X.t * X.t end
reçoit le type
functor (X : sig type t end) → sig type u = X.t * X.t end
dans lequel la signature du résultat fait intervenir le nom X du paramètre formel.
L’environnement E est en fait une séquence de spécifications S1 ; . . . Sn , tout comme l’intérieur d’une
signature sig. . . end.
Les règles définissant le prédicat E ` τ1 ≈ τ2 sont:
97
La règle (eq-projection) est compliquée par le fait que les composantes de la signature affectée
à p peuvent dépendre les unes des autres. Par conséquent, le type τ manifestement égal à la
composante t peut faire référence à des identificateurs de types et de modules liés au début de la
signature. Il n’est donc pas correct en général de dire que E ` p.t ≈ τ , car certains identificateurs de
τ vont être sortis de leur portée et devenir libre. Il faut au contraire préfixer par p les identificateurs
X et t liés précédemment dans la signature.
Exemple: supposons E ` p : sig type t; type u; type v = u × t end. Il n’est pas correct de
dire E ` p.v ≈ u × t, car ce type fait référence à des identificateurs de types u et t inconnus. En
revanche, nous pouvons déduire E ` p.v ≈ (u × t)[t ← p.t; u ← p.u], c’est-à-dire E ` p.v ≈ p.u × p.t.
Le type qui s’appelle u à l’intérieur de la signature est référencé à l’extérieur de la signature par
p.u, et de même pour t.
E = E1 ; val x : σ; E2 τ ≤σ
(var-inst)
E`x:τ
E ` p : sig S1∗ ; val x : σ; S2∗ end τ ≤ σ{z ← p.z | z lié dans S1∗ }
(val-projection)
E ` p.x : τ
E`a:τ E ` τ ≈ τ0
(equiv)
E ` a : τ0
Pour l’accès aux composantes de valeurs de structures (règle (proj-val)), on effectue la même
opération de “préfixage” par p décrite plus haut à propos de la règle (eq-proj).
Les autres règles de typage sont reprises directement de celles du chapitre 1:
98
8.3.3 Sous-typage entre types de modules
Nous définissons maintenant une relation de sous-typage entre types de modules E ` M1 <: M2
qui reflète les deux possibilités d’oubli d’information dans les signatures mentionnées plus haut
(oubli de composantes et transformation de types manifestes en types abstraits). Au passage, nous
définissons également le sous-typage entre deux spécifications E ` S1 <: S2 .
99
Le sous-typage entre composantes de signatures E ` S <: S 0 se comprend facilement en voyant
les composantes de signatures comme des spécifications: S est “sous-type” de S 0 si toute déclaration
(composante de structure) satisfaisant la spécification S satisfait aussi S 0 .
• Pour deux spécifications de valeurs val x : σ et val x : σ 0 , il faut que le schéma σ soit plus
général que σ 0 (i.e. σ au moins aussi polymorphe que σ 0 ), de manière à ce que toute instance
de σ soit aussi instance de σ 0 .
Comme les composantes des signatures peuvent faire référence à des identificateurs liés par
d’autres composantes, on ne peut pas les comparer dans l’environnement initial E: il faut ajouter
à E des hypothèses de typage sur les identificateurs liés par les signatures. Comme tous les iden-
tificateurs liés par M 0 (la plus grande des deux signatures) le sont aussi par M (la plus petite), et
ont a priori des types plus précis dans M , il suffit d’ajouter à E toutes les composantes S1 . . . Sn
de M . C’est pourquoi la règle (sub-sig) compare les composantes deux à deux dans E; S1 ; . . . ; Sn .
100
Exemples de non sous-typage entre signatures:
Il manque une composante dans M :
6 : (sig type t = int val v : t end)
(sig type t = int end) <
Erreur sur le nom d’une composante:
6 : (sig type t = int val v : t end)
(sig type t = int val n : t end) <
Désaccord sur la définition d’un type manifeste:
6 : (sig type t = bool end)
(sig type t = int end) <
Un type abstrait n’est pas prouvablement égal à un type manifeste:
6 : (sig type t = bool end)
(sig type t end) <
car sous l’hypothèse X : sig type t = int end on peut prouver que X.t ≈ int, et donc que
sig type t = X.t end <: sig type t = int end. Ce ne serait pas possible sous l’hypothèse X :
sig type t end.
E = E1 ; module X : M ; E2
(mod-var)
E`X:M
E ` p : sig S1∗ ; module X : M ; S2∗ end
(mod-projection)
E ` p.X : M {z ← p.z | z lié dans S1∗ }
E`m:M E`m:M E ` M <: M 0
(mod-contrainte) (mod-sub)
E ` (m : M ) : M E ` m : M0
101
Typage des structures
E ` d∗ : S ∗
(struct)
E ` (struct d∗ end) : (sig S ∗ end)
E`a:τ E; val v : τ ` d∗ : S ∗
E ` ε : ε (struct-vide) (struct-val)
E ` (let v = a; d∗ ) : (val v : τ ; S ∗ )
t∈
/ Dom(E) E; type t = τ ` d∗ : S ∗
(struct-type)
E ` (type t = τ ; d∗ ) : (type t = τ ; S ∗ )
E`m:M X∈
/ Dom(E) E; module X : M ` d∗ : S ∗
(struct-mod)
E ` (module X = m; d∗ ) : (module X : M ; S ∗ )
Lorsqu’on type une struture, les définitions de types reçoivent des types manifestes, et sont
donc transparentes par défaut. Par exemple, la structure
module S = struct type t = int; let x = 0 end
reçoit la signature sig type t = int; val x: int end, ou de manière équivalente sig type t
= int; val x: t end. Dans les deux cas, nous pouvons typer 1 + S.f 0 par exemple.
Pour rendre abstrait un type, il faut utiliser une contrainte de signature:
module S = (struct type t = int; let x = 0 end : sig type t; val x: t end)
Les conditions t ∈
/ Dom(E) et X ∈ / Dom(E) dans les règles (struct-type) et (struct-mod) évitent
des incohérences de typage lorsqu’on redéfinit un nom de type ou de module existant. Par exemple:
struct
type t = int t est équivalent à int
let x = (1 : t) x a le type t
type t = bool t est équivalent à int
let y = (true : t) y a le type t et x aussi
... if x = y then ... x et y ont le même type t
end
La condition t ∈/ Dom(E) dans la règle (struct-type) et la condition X ∈ / Dom(E) dans (struct-
mod) évitent ce problème, mais sont un peu trop restrictives. En particulier, on ne peut pas définir
deux fois le même nom de type à des niveaux d’emboı̂tement de structures différents:
struct
type t = int
module X = struct type t = bool ... end
end
Pour traiter plus souplement les redéfinitions, on peut distinguer dans les structures les noms des
composantes (qui servent à faire référence aux composantes dans les projections et ne peuvent
donc pas être renommées) et les identificateurs liés par les définitions de composantes (qui servent
à faire référence aux composantes dans le reste de la structure et peuvent être renommés par
alpha-conversion). Ainsi, l’exemple ci-dessus devient (les identificateurs sont marqués en italiques):
102
struct
type t/t1 = int
let x/x = (1 : t1 ) x a le type t1
type t/t2 = int
let y/y = (true : t2 ) y a le type t2
... if x = y then ... x et y ont des types différents
end
X∈
/ Dom(E) E; X : M ` m : M 0
(mod-foncteur)
E ` (functor (X : M ) → m) : (functor (X : M ) → M 0 )
E ` m1 : (functor (X : M ) → M 0 ) E ` m2 : M
(mod-appl)
E ` m1 (m2 ) : M 0 [X ← m2 ]
E ` m1 : (functor (X : M ) → M 0 ) E ` m2 : M / L(M 0 )
X∈
(mod-appl-nondep)
E ` m1 (m2 ) : M 0
Si l’argument m2 du foncteur n’est pas un chemin d’accès et que X apparaı̂t dans le type M 0 du
résultat du foncteur, la substitution M 0 [X ← m2 ] n’est pas un type bien formé. La règle (mod-appl)
n’est alors pas applicable directement. Exemple:
module B = Id(struct type t = int end)
Pour appliquer (mod-appl), il faudrait dans le type sig type t = X.t end remplacer X par struct
type t = int end, obtenant le type mal formé
sig type t = (struct type t = int).t end
Une solution simple à ce problème est de toujours nommer les arguments de foncteurs qui ne sont
pas des chemins:
module A = F(m) ⇒ module B = m; module A = F(B)
103
Une solution plus subtile consiste à utiliser la règle de sous-typage (mod-sub) pour faire dis-
paraı̂tre la dépendance entre argument et résultat dans le type du foncteur. Dans l’exemple Id
ci-dessus, remarquons que
Le super-type est un type non dépendant: le paramètre formel X n’apparaı̂t plus dans le type du
résultat. On peut donc construire la dérivation suivante:
La règle de renforcement
Soit p un chemin désignant une structure avec un type t abstrait:
L’implémentation du type p.t est inconnue. Donc, le type p.t est a priori incompatible avec tout
autre type. Cependant, la composante t de la structure désignée par p n’est pas, elle, n’importe
quel type: nous savons qu’elle est forcément égale à p.t. Le chemin p a donc aussi le type suivant:
Plus généralement, nous appelons renforcement cette opération de remplacement de types abstraits
par des types manifestement égaux à eux-même dans la signature d’un chemin. Si M est un type
de module et p un chemin, nous définissons le type renforcé M/p comme suit:
E`p:M
(mod-renforcement)
E ` p : (M/p)
Le renforcement est nécessaire dans plusieurs situations. La première est lorsqu’on prend une
vue restreinte d’un module contenant des types abstraits. Supposons par exemple
104
E : sig type t; val x: t; val y: t → t end
Nous voulons prendre une vue de E qui cache la composante y. Si nous faisons
nous cachons y, mais rendons le type B.t abstrait, et donc différent de E.t. Pour conserver la
compatibilité entre B.t et E.t, il faut écrire
Pour typer cette contrainte, il faut montrer que le type de E est sous-type de sig type t = E.t;
val x: t end. Si l’on part de E : sig type t; . . ., ce n’est pas possible. Il faut renforcer au
préalable le type de E, obtenant sig type t = E.t; . . ., pour montrer que la contrainte de signature
est bien typée.
La seconde utilité de la règle de renforcement est pour détecter la propagation des types à
travers les foncteurs. Reprenons le foncteur identité vu plus haut:
Sans règle de renforcement, le type le plus précis que l’on puisse lui attribuer est
et ce type ne traduit pas que la composante t du résultat est égale à la composante t de l’argument.
En appliquant la règle de renforcement au type de X, nous obtenons le type plus précis:
Une troisième application du renforcement est pour vérifier des contraintes de partage. Un
foncteur à plusieurs arguments peut avoir à imposer que des composantes de types de ses arguments
soient égales afin que le corps du foncteur soit bien typé. C’est ce qu’on appelle une contrainte
de partage entre les arguments d’un foncteur, et cette contrainte de partage s’exprime facilement
avec des types manifestes en position d’argument de foncteur. Par exemple, voici un foncteur qui
compose des opérations entre types abstraits:
module Compose =
functor(X : sig type t; val f: t → t end) →
functor(Y : sig type t = X.t; val f: t → t end) →
struct
type t = X.t
let f = fun x → X.f(Y.f(x))
end
Grâce à la spécification Y : sig type t = X.t; . . . , le corps du foncteur est typé sous l’hypothèse
X.t = Y.t, et cela assure que la composition des fonctions X.f et Y.f est bien typée. Si on
avait déclaré Y : sig type t; . . . , X.t et Y.t auraient été considérés comme incompatibles, et
la définition de la fonction f comme mal typée.
La vérification des contraintes de partage lors de l’application du foncteur s’effectue automa-
tiquement par les règles de typage de l’application et de sous-typage. Par exemple, supposons
105
module A : sig type t = τ1 ; val f: t → t end
module B : sig type t = τ2 ; val f: t → t end
Compose(A) :
functor (Y : sig type t = A.t end; val f : t → t end) →
sig type t = A.t; val f : t → t end
Pour que Compose(A)(B) soit bien typé, il faut que B possède la signature sig type t = B.t;
val f: t → t, et cela nécessite d’appliquer la règle de renforcement au type de B.
Preuve de sûreté du typage: la thèse suivante étudie les propriétés formelles d’un cal-
cul de modules proche de celui présenté dans ce chapitre, en particulier la sûreté du ty-
page: Translucent sums: a foundation for higher-order module systems, M. Lillibridge, PhD
thesis, Carnegie-Mellon University, 1997, [Link]
Mark Lillibridge/Papers/Thesis/[Link].
106
Exercices
Exercice 8.1 (*)/(**) Montrer que la relation de sous-typage <: est réflexive (*) et transitive
(**).
Exercice 8.2 (*) On dit que deux signatures S1 et S2 sont équivalentes dans l’environnement A,
et on note A ` S1 ≈ S2 , si A ` S1 <: S2 et A ` S2 <: S1 . Donner une axiomatisation directe de
A ` S1 ≈ S2 sous forme de règles d’inférence.
Exercice 8.3 (***) Montrer qu’on ne perd pas d’expressivité si on restreint les règles de projection
(eq-projection), (val-projection) et (mod-projection) au cas où le type de la composante extraite ne
dépend pas du début S1∗ de la signature:
On a noté L(τ ) les identificateurs de types et de modules libres dans le type τ et B(S ∗ ) les identi-
ficateurs de types et de modules liés par la signature S ∗ . (Indication: on peut toujours appliquer la
règle de renforcement à p avant de typer la projection.)
107
Appendix A
Exercice 1.1 La construction ML let rec f x = a1 in a2 peut être vue comme du “sucre
syntaxique” pour
let f = fix(fun f → fun x → a1 ) in a2
Exercice 1.2 Le let rec multiple peut toujours se ramener à un let rec simple en
paramétrisant l’une des définitions par-rapport à l’autre. Autrement dit, let rec f x =
a1 and g y = a2 in a3 peut se transformer en
let rec f g x = a1 in
let rec g y = let f = f g in a2 in
let f = f g in
a3
Ensuite, on encode ces deux let rec simples en termes de fix comme dans l’exercice 1.1.
Exercice 1.3 On montre facilement que si deux prédicats P et Q satisfont les règles, alors leur
conjonction P ∧ Q les satisfait aussi. En effet, si P et Q satisfont les axiomes, alors P (ai (x)) est
vrai pour tout x, ainsi que Q(ai (x)), et donc (P ∧ Q)(ai (x)) est vrai. Pour ce qui est des règles,
supposons que (P ∧ Q)(bkj (x)) est vrai pour tout k = 1 . . . n. Alors, P (bkj (x)) est vrai pour tout k,
et donc P (cj (x)) est vrai puisque P satisfait la règle j. De même, Q(bkj (x)) est vrai pour tout k,
et donc Q(cj (x)) est vrai puisque Q satisfait la règle j. Il s’ensuit que l’implication
les prédicats satisfaisant les règles). Par le résultat précédent, Pmin satisfait les règles, et par
construction il est plus petit que tout autre prédicat P satisfaisant les règles.
108
Exercice 1.4 On note D(x) le prédicat “il existe une dérivation de l’énoncé P (x) dans le système
de règles”. La preuve que D est le plus petit prédicat satisfaisant les règles est en deux temps:
(1) on montre que D satisfait les règles, et (2) on montre que pour tout prédicat Q satisfaisant les
règles, D(x) implique Q(x).
Pour (1), il est vrai que ∀x. D(ai (x)), puisque pour tout x donné, P (ai (x)) est une dérivation
valide réduite à une feuille. De même, si pour un certain x, nous avons D(b1j (x)) ∧ . . . ∧ D(bnj (x)),
cela signifie que nous avons des dérivations de P (b1j (x)) . . . P (bnj (x)); on peut donc construire une
dérivation de noeud racine P (cj (x)) et de fils les dérivations de P (b1j (x)) . . . P (bnj (x)), et c’est une
dérivation valide. Donc, D((cj (x)) est vrai. Il s’ensuit que D satisfait les règles.
Pour (2), on se donne un prédicat Q satisfaisant les règles, et on montre par récurrence struc-
turelle sur la dérivation que pour tout x, si l’on a une dérivation de l’énoncé P (x), alors Q(x)
est vrai. Il s’ensuit D(x) implique Q(x) pour tout x, et donc D est plus petit que Q. Prenant
Q = Pmin , par minimalité de Pmin , il s’ensuit D = Pmin comme annoncé.
v
Exercice 1.5 Pour a = 1 2, une dérivation de a → v devrait se terminer par une des règles 4, 7,
8 ou 9. Mais pour que ces règles s’appliquent, il faudrait que 1 s’évalue en une fonction (pour la
règle 4) ou en une opération (pour les autres règles). Cependant, la seule valeur en laquelle 1 peut
v
s’évaluer est 1, qui n’est rien de tout cela. Donc, il n’y a pas de dérivation de a → v pour tout v.
v
Pour a0 = (fun f → f f ) (fun f → f f ), notons b = (fun f → f f ). Une dérivation de a0 → v
doit nécessairement se terminer ainsi:
v v v
b→b b→b (f f )[f ← b] → v
v
bb→v
v
Mais (f f )[f ← b] = b b = a0 , donc toute dérivation de a0 → v doit contenir une sous-dérivation de
v
a0 → v; il n’existe bien sûr pas de dérivation finie satisfaisant cette propriété.
La différence entre a et a0 est que a est un terme essentiellement mal formé, alors que a0 est un
terme bien formé mais dont l’évaluation ne termine pas.
Exercice 1.6 Cas a = let x = a1 in a2 . La seule règle qui s’applique est 6, et donc D est de la
forme
(D1 ) (D2 )
.. ..
. .
v v
a1 → v1 a2 [x ← v1 ] → v2
v
a1 a2 → v2
Vu la forme de a, D0 se termine nécessairement par la règle 6 elle aussi. Donc, D0 contient des
v v
sous-dérivations D10 : a1 → v10 et D20 : a2 [x ← v10 ] → v20 pour certaines valeurs v10 et v20 . Comme D1
est une sous-dérivation de D et D10 une sous-dérivation de D0 , nous pouvons appliquer l’hypothèse
de récurrence à D1 et D10 . Il vient v1 = v10 . Par conséquent, a2 [x ← v1 ] = a2 [x ← v10 ] et nous
pouvons appliquer l’hypothèse de récurrence à D2 et D20 . Il vient v2 = v20 , ce qui entraı̂ne le résultat
attendu v = v 0 .
109
Exercice 1.7 Pour typer 1 2, il faudrait pouvoir attribuer à 1 un type flèche τ1 → τ2 , ce qui est
bien sûr impossible car 1 a le type int dans tous les environnements de typage.
Pour typer fun f → f f , il faudrait construire une dérivation de la forme suivante:
E + {f : τ1 } ` f : τ1 → τ2 E + {f : τ1 } ` f : τ2
E + {f : τ1 } ` f f : τ2
E ` fun f → f f : τ1 → τ2
Pour que les feuilles de la dérivation soient justifiées par l’axiome (var), il faudrait que τ1 = τ1 → τ2
et τ1 = τ2 . La première de ces égalités est impossible, car τ1 serait alors un sous-terme strict de
lui-même, ce qui est impossible pour tout terme τ1 fini.
Enfin, dans le cas de let f = fun x → x in (f 1, f true), nous pouvons attribuer à fun x → x
le type τ → τ pour n’importe quel τ . Mais pour que f 1 soit bien typé, il faudrait prendre τ = int,
et pour que f true soit bien typé, il faudrait prendre τ = bool, et il est impossible de satisfaire
ces deux contraintes simultanément.
Pour la dernière égalité, on s’appuie sur le fait que {γ1 . . . γq } ∩ {β1 . . . βn } = ∅ car sinon l’une des
βi serait libre dans σ. D’où L(σ) = L(σ 0 ). CQFD.
110
Exercice 1.9 Pour le terme let f = fun x → x in f f , on donne à f le schéma ∀α. α → α, puis
on donne à la première occurrence de f un type (τ → τ ) → (τ → τ ), et à la seconde occurrence
τ → τ . Le terme entier a donc le type τ → τ pour τ arbitraire.
Pour fun f → f f , ce terme n’est toujours pas typable. En effet, une dérivation de typage de
ce terme devrait se terminer par:
τ → τ2 ≤ τ1 τ ≤ τ1
{f : τ1 } ` f : τ → τ2 {f : τ1 } ` f : τ
{f : τ1 } ` f f : τ2
∅ ` fun f → f f : τ1 → τ2
Exercice 1.11 Commençons par définir l’image ϕ(σ) d’un schéma σ = ∀α1 . . . αn . τ par une
substitution ϕ. Ensuite, ϕ(E) sera simplement l’application point à point de ϕ sur les schémas
contenus dans E, c’est-à-dire ϕ(E) = E 0 est tel que E 0 (x) = ϕ(E(x)) pour tout x ∈ Dom(E).
Naı̈vement, on prendrait
ϕ(∀α1 . . . αn . τ ) = ∀α1 . . . αn . ϕ(τ )
mais cela pose des problèmes de capture de variables liées par le quantificateur ∀. Par exemple, si
ϕ = [α ← β], cela donnerait:
et on voit que ces deux résultats sont incorrects en se rappelant que les variables liées α et β
dans les deux schémas de types peuvent être renommées en toute autre variable γ sans changer la
signification du schéma de types. Or,
Autrement dit, la définition naı̈ve ci-dessus ne passe pas au quotient par alpha-conversion (renom-
mage des variables liées): suivant les rennomages que l’on effectue sur les variables liées du schéma
argument, on obtient des schémas résultats différents, même à alpha-conversion près.
L’idée est de forcer le rennomage “qui va bien” dans le schéma argument afin d’éviter toute
interférence entre les variables liées et la substitution. On prend donc:
Dans cette définition, on dit qu’une variable α est hors de portée d’une substitution ϕ si
111
1. ϕ(α) = α (c’est-à-dire, ϕ ne modifie pas α)
2. si α n’est pas libre dans τ , alors α n’est pas libre dans ϕ(τ ) (c’est-à-dire, ϕ n’introduit pas α
dans son résultat).
Par exemple, prenant ϕ = [α ← β], on voit que α n’est pas hors de portée de ϕ (car ϕ(α) = β,
donc la condition 1 n’est pas vraie), et β n’est pas hors de portée de ϕ non plus (car β n’est pas
libre dans α, mais β est libre dans ϕ(α) = β, donc la condition 2 n’est pas vraie). En revanche, γ
est hors de portée de ϕ, car ϕ(γ) = γ, et de plus si γ n’est pas libre dans τ , alors τ ne contient que
des variables α, β, δ, . . ., que ϕ transforme en β, β, δ, . . . respectivement, donc γ n’est pas non plus
libre dans ϕ(γ).
Notez que dans la définition de ϕ(∀α1 . . . αn . τ ), la condition “α1 , . . . , αn sont hors de portée de
ϕ” peut toujours être satisfaite en renommant préalablement les α1 . . . αn . (Il y a un nombre infini
de variables hors de portée d’une substitution donnée.) On a donc défini ϕ(σ) pour tout schéma σ.
Passons à la preuve de la proposition 1.2. La preuve est par récurrence sur la dérivation de
typage de E ` a : τ et par cas sur la dernière règle de typage utilisée.
Cas règle (var-inst). Nous avons E ` x : τ avec τ ≤ E(x). Écrivons E(x) = ∀α1 . . . αn .τx . Nous
avons donc τ = τx [α1 ← τ1 , . . . , αn ← τn ]. Quitte à renommer les αi , nous pouvons de plus supposer
les αi hors de portée de ϕ. Donc:
Ceci montre que ϕ(τ ) ≤ (ϕ(E))(x). Par conséquent, la règle (var-inst) nous permet de conclure
que ϕ(E) ` x : ϕ(τ ), ce qui est le résultat désiré.
Cas règle (const-inst) ou (op-inst). Comme les schémas T C(c) et T C(op) sont clos (sans variables
libres) pour tous c et op, on a ϕ(T C(c)) = T C(c) et de même ϕ(T C(op)) = T C(op). On conclut
alors par le même raisonnement que pour la règle (var-inst).
Cas règle (fun). Nous avons E ` (fun x → a) : τ1 → τ2 en conséquence de la prémisse E + {x :
τ1 } ` a : τ2 . Appliquant l’hypothèse de récurrence à cette prémisse, nous obtenons une dérivation
de ϕ(E + {x : τ1 }) ` a : ϕ(τ2 ), c’est-à-dire ϕ(E) + {x : ϕ(τ1 )} ` a : ϕ(τ2 ). Par application de la
règle (fun), nous concluons ϕ(E) ` (fun x → a) : ϕ(τ1 ) → ϕ(τ2 ), ce qui est le résultat désiré.
Cas règle (app) ou (paire). Même raisonnement que pour la règle (fun).
Cas règle (let). C’est là que les choses se compliquent. Nous avons donc E ` (let x = a1 in a2 ) : τ2
en conséquence des prémisses E ` a1 : τ1 et E + {x : Gen(τ1 , E)} ` a2 : τ2 . Le problème est que
les variables généralisées par Gen, c’est-à-dire {α1 , . . . , αn } = L(τ1 ) \ L(E), ne sont pas forcément
hors de portée de ϕ, et donc on n’a pas, en général,
112
L’astuce est d’arriver à renommer les variables généralisées αi afin qu’elles soient hors de portée
de ϕ. Pour ce faire, on va appliquer l’hypothèse de récurrence à E ` a1 : τ1 et non pas à la
substitution ϕ, mais à une substitution ψ “proche” de ϕ mais contournant les problèmes de capture.
Plus précisément, on se donne des variables β1 , . . . , βn non libres dans E et hors de portée de
ϕ, et on considère la substitution
ψ = ϕ ◦ [α1 ← β1 , . . . , αn ← βn ]
Par application de l’hypothèse de récurrence, on a ψ(E) ` a1 : ψ(τ1 ). Comme les βi ne sont pas
libres dans E, on a [α1 ← β1 , . . . , αn ← βn ](E) = E et donc ψ(E) = ϕ(E). La dérivation obtenue
par récurrence prouve donc
ϕ(E) ` a1 : ψ(τ1 )
On applique également l’hypothèse de récurrence à la seconde prémisse, avec la substitution ϕ cette
fois-ci. On obtient une dérivation de
Pour conclure le résultat attendu par application de la règle (let-gen), il reste donc à montrer que
Les variables libres dans ψ(τ1 ) mais pas dans ϕ(E) sont exactement {β1 , . . . , βn }. En effet, les
variables libres dans τ1 sont
Les βi ne sont pas libres dans ϕ(E), car par hypothèse βi hors de portée de ϕ, cela impliquerait βi
libre dans E, contredisant l’hypothèse βi non libre dans E. Par conséquent,
Or, Gen(τ1 , E) = ∀α1 , . . . , αn .τ1 = ∀β1 , . . . , βn .τ1 [αi ← βi ] à alpha-conversion près. De plus, les βi
sont hors de portée de ϕ, donc:
Nous avons donc montré ϕ(Gen(τ1 , E)) = Gen(ψ(τ1 ), ϕ(E)), et le résultat attendu en découle.
113
Appendix B
Exercice 2.1 L’évaluation de droite à gauche s’obtient en définissant les contextes d’évaluation
par
Contextes d’évaluation (droite-gauche):
Γ ::= [ ] évaluation en tête
|aΓ évaluation à droite d’une application
|Γv évaluation à gauche d’une application
| let x = Γ in a évaluation à gauche d’un let
| (a, Γ) évaluation à droite d’une paire
| (Γ, v) évaluation à gauche d’une paire
L’évaluation sans ordre imposé d’évaluation, mais toujours en appel par valeur, s’obtient par:
Contextes d’évaluation (sans ordre imposé):
Γ ::= [ ] évaluation en tête
|Γa évaluation à gauche d’une application
|aΓ évaluation à droite d’une application
| let x = Γ in a évaluation à gauche d’un let
| (Γ, a) évaluation à gauche d’une paire
| (a, Γ) évaluation à droite d’une paire
v ∗
Exercice 2.2 On montre d’abord l’implication (a → v) ⇒ (a → v) par récurrence sur la
v
dérivation de l’évaluation a → v et par cas sur la dernière règle utilisée. Si c’est un des axiomes 1,
2, 3, le résultat est immédiat car v = a. Si c’est la règle 4, on a:
v v v
a → (fun x → c) b → v2 c[x ← v2 ] → v
v
ab→v
114
Par hypothèse de récurrence appliquée aux trois sous-dérivations des prémisses, nous savons qu’il
existe des séquences de réductions de la forme
a → a1 → . . . → an → v1 = (fun x → c)
b → b1 → . . . → bp → v2
c[x ← v2 ] → c1 → . . . → cq → v
En appliquant la règle (contexte) à chaque étape des deux premières séquences (avec les contextes
[ ] b et v1 [ ]), nous obtenons
a b → a1 b → . . . → an b → v1 b
v1 b → v1 b1 → . . . → v1 bp → v1 v2
a b → . . . → v1 b → . . . → v1 v2 = (fun x → c) v2 → c[x ← v2 ] → . . . → v
∗
D’où le résultat attendu a b → v. Le raisonnement est le même pour les autres règles d’évaluation
(5, 6, 7, 8, 9).
∗ v
Montrons maintenant l’implication inverse (a → v) ⇒ (a → v). Il suffit de montrer les deux
lemmes suivants:
v
1. Pour toute valeur v, v → v.
v v
2. Si a → a0 et a0 → v, alors a → v.
v v
En effet, si l’on a a → a1 → . . . an → v, il s’ensuit que v → v par (1), puis an → v par (2), puis
v v
an−1 → v par (2), et ainsi de suite jusqu’à a → v par applications répétées de (2).
Le lemme (1) est immédiat par récurrence structurelle sur v.
ε
Pour (2), on montre d’abord le résultat pour une réduction de tête a → a0 , en examinant les
axiomes de réduction. Prenons comme exemple βf un : on a a = (fun x → a1 ) v2 et a0 = a1 [x ← v2 ].
On peut construire la dérivation suivante:
v v v
(fun x → a1 ) → (fun x → a1 ) v2 → v2 a1 [x ← v2 ] → v
v
(fun x → a1 ) v2 → v
(La prémisse de gauche est l’axiome 3; celle du milieu vient du lemme (2); celle de droite de
v v
l’hypothèse a1 [x ← v2 ] → v.) On a donc bien montré a → v. La preuve pour les autres axiomes de
réduction en tête est similaire.
ε
Pour finir la preuve de (2), il faut montrer que tout cela passe bien au contexte: si a → a0 et
v v
Γ(a0 ) → v, alors Γ(a) → v. Cela se fait par récurrence structurelle sur Γ. Le cas de base Γ = [ ] est
le résultat précédent sur les réductions de tête. Faisons le cas Γ = ∆ a2 par exemple. Supposons
v
donc Γ(a0 ) → v. Comme Γ(a0 ) = ∆(a0 ) a2 , nous avons donc une dérivation de la forme
v v v
∆(a0 ) → fun x → a3 a2 → v2 a3 {x ← v2 } → v
v
∆(a0 ) a2 → v
115
v
Par hypothèse de récurrence, on a ∆(a) → fun x → a3 . On peut donc construire la dérivation
v v v
∆(a) → fun x → a3 a2 → v2 a3 {x ← v2 } → v
v
∆(a) a2 → v
v
qui conclut Γ(a) → v comme attendu. La preuve pour les autres types de contextes est similaire.
ε
Exercice 2.3 H0 est trivialement vérifiée. Pour H1, on regarde chaque δ-règle a → a0 et à partir
d’une dérivation de typage de E ` a : τ (à gauche), on construit une dérivation de typage de
E ` a0 : τ (à droite):
E ` n1 : int E ` n2 : int
E ` + : int × int → int E ` (n1 , n2 ) : int E ` n : int si n = n1 + n2
E ` +(n1 , n2 ) : int
E ` v1 : τ1 E ` v2 : τ2
E ` fst : τ1 × τ2 → τ1 E ` (v1 , v2 ) : τ1 × τ2 E ` v1 : τ1
E ` fst(v1 , v2 ) : τ1
E ` v1 : τ1 E ` v2 : τ2
E ` snd : τ1 × τ2 → τ2 E ` (v1 , v2 ) : τ1 × τ2 E ` v2 : τ2
E ` snd(v1 , v2 ) : τ2
E + {x : τ } ` a : τ
E ` fix : (τ → τ ) → τ E ` fun x → a : τ → τ E ` a[x ← fix(fun x → a)] : τ
E ` fix(fun x → a) : τ
116
Appendix C
La traduction T de M Lt dans M Lp :
T (x) = x
T (c) = c
T (projn,n ) = fun x → sndn−1 (x)
T (proji,n ) = fun x → fst(sndi−1 (x)) si i < n
T (op) = op pour les autres opérateurs op
T ((v1 , . . . , vn )) = (T (v1 ), (T (v2 ), . . . (T (vn−1 ), T (vn ))))
T (fun x → a) = fun x → T (a)
T (a1 (a2 )) = T (a1 )(T (a2 ))
T (let x = a1 in a2 ) = let x = T (a1 ) in T (a2 )
La commutation entre T et la réduction se montre d’abord pour chaque règle de réduction en tête.
ε
La plus intéressante est bien sûr la δ-règle pour les tuples: proji,n (v1 , . . . , vn ) → vi . Si i = n, on a:
T (projn,n (v1 , . . . , vn ))
= (fun x → sndn−1 (x))(T (v1 ), (T (v2 ), . . . (T (vn−1 ), T (vn ))))
→ sndn−1 (T (v1 ), (T (v2 ), . . . (T (vn−1 ), T (vn )))) par βf un
→ sndn−2 (T (v2 ), . . . (T (vn−1 ), T (vn ))) par δsnd
∗
→ T (vn ) par δsnd
De même, si i < n, on a:
T (projn,n (v1 , . . . , vn ))
= (fun x → fst(sndi−1 (x)))(T (v1 ), (T (v2 ), . . . (T (vn−1 ), T (vn ))))
117
→ fst(sndi−1 (T (v1 ), (T (v2 ), . . . (T (vn−1 ), T (vn ))))) par βf un
→ fst(sndi−2 (T (v2 ), . . . (T (vn−1 ), T (vn )))) par δsnd
∗
→ fst(T (vi ), . . .) par δsnd
→ T (vi ) par δf st
Le résultat est immédiat pour βf un et βlet car T commute avec la substitution: T (a[x ← b]) =
T (a)[x ← T (b)]. Enfin, pour la règle (contexte), on utilise la commutation de T avec l’application
∗
de contexte: T (Γ(a)) = T (Γ)(T (a)). D’où le résultat: si a → a0 dans M Lt , alors T (a) → T (a0 )
dans M Lp .
Réciproquement, si T (a) → a00 , a00 n’est pas nécessairement la traduction d’un terme a0 tel que
a → a0 . Exemple:
Le terme de gauche est la traduction de proj3,3 (1, 2, 3), mais les deux étapes suivantes de la
réduction ne sont pas des traductions de termes de M Lt . Si l’on ignore les projections non ap-
pliquées et que l’on prend une traduction plus directe des applications de projections:
Exercice 4.2 Il suffit de définir type bool = false of unit | true of unit. L’opérateur de
filtrage Fbool permet de définir la conditionnelle comme suit:
118
Exercice 4.4 Voici quelques valeurs du type t:
C(fun x → x)
C(fun y → C(fun x → x))
C(fun y → C(fun x → y))
[[x]] = x
[[λx.M ]] = enrouler(fun x → [[M ]])
[[M N ]] = dérouler[[M ]] [[N ]]
En corollaire, on voit qu’il existe des expressions de type t (la traduction de (λf.f f )(λf.f f ) [Link].)
dont l’évaluation ne termine pas, bien qu’elles soient construites sans un seul let rec. Un exemple
qui ne passe même pas par le codage du λ-calcul pur est:
Exercice 4.5
1) On définit la substitution F (p, v) comme suit:
F ( , v) = id
F (x, v) = [x ← v]
F (c, c) = id
F (C(p), C(v)) = F (p, v)
F ((p1 , . . . , pn ), (v1 , . . . , vn )) = F (p1 , v1 ) + · · · + F (pn , vn )
(Pour le dernier cas, on suppose qu’une même variable x n’apparait jamais deux fois dans un motif
p.) Si aucun des cas ci-dessus ne s’applique, F (p, v) est indéfini. La réduction du match est alors:
ε
(match v with p → a2 | → a3 ) → σ(a2 ) si σ = F (p, v) est défini
ε
(match v with p → a2 | → a3 ) → a3 si F (p, v) est indéfini
2) On définit l’énoncé de typage auxiliaire ` p : τ, E (“le motif p filtre des valeurs de type τ , et ce
faisant il lie les variables x ∈ Dom(E) à des valeurs de type E(x)”).
τ 0 → τ ≤ T C(C) ` p : τ 0, E
` : τ, ∅ ` x : τ, {x : τ }
` C(p) : τ, E
` p1 : τ1 , E 1 ... ` pn : τn , E n
` (p1 , . . . , pn ) : τ1 × . . . × τn , E1 + . . . + En
119
La règle de typage du match est alors:
E ` a1 : τ 0 ` p : τ 0, E0 E + E 0 ` a2 : τ E ` a3 : τ
E ` (match a1 with p → a2 | → a3 ) : τ
C(a, , b, c) = b
C(a, x, b, c) = let x = a in b
C(a, C(p), b, c) = Ft (a, fn , fn , . . . , fn , fo , fn , . . . , fn )
| {z }
fois
i−1
e
si C est le i constructeur du type t
et fn = fun x → c x non libre dans c
et fo = fun x → C(x, p, b, c) x non libre dans b et c
C(a, (p1 , . . . , pn ), b, c) = C(proj1,n (a), p1 , C(proj2,n (a), p2 , . . . , C(projn,n (a), pn , b, c)))
120
Appendix D
Exercice 5.1 La fonction f calcule la fonction factorielle. En effet, une fois que l’on a évalué
l’affectation
r := fun x → if x = 0 then 1 else x * (!r)(x-1)
on a bien que la fonction g = !r est égale à fun x → if x = 0 then 1 else x * (!r)(x-1),
c’est-à-dire fun x → if x = 0 then 1 else x * g(x-1).
Exercice 5.2 Voici l’opérateur de point fixe pour les fonctions des entiers dans les entiers:
let fix = fun f →
let r = ref(fun x → 0) in
r := (fun x → f (!r) x);
(!r)
On peut le généraliser pour qu’il opère sur toutes les fonctions à condition de se donner une
expression ω de type ∀α.α et qui bien sûr ne termine pas ([Link]. une boucle infinie ou encore une
levée d’exception raise E):
let fix = fun f →
let r = ref(fun x → ω) in
r := (fun x → f (!r) x);
(!r)
Le fix ci-dessus a le type ∀α, β. ((α → β) → (α → β)) → (α → β).
L’opérateur fix sur des types non-fonctionnels ([Link]. (int → int) → int) n’est pas définissable
avec des références.
Exercice 5.3
v v v
c/s → c/s op/s → op/s (fun x → a)/s → (fun x → a)/s
v v v
a1 /s → (fun x → a)/s1 a2 /s1 → v2 /s2 a[x ← v2 ]/s2 → v/s3
v
a1 a2 /s → v/s3
121
v v v v
a1 /s → v1 /s1 a2 /s1 → v2 /s2 a1 /s → v1 /s1 a2 [x ← v1 ]/s1 → v/s2
v v
(a1 , a2 )/s → (v1 , v2 )/s2 (let x = a1 in a2 )/s → v/s2
v v
a/s → v/s1 `∈
/ Dom(s1 ) a/s → `/s1 ` ∈ Dom(s1 )
v v
(ref(a))/s → `/s1 + [` ← v] !a/s → s1 (`)/s1
v v
a1 /s → `/s1 ` ∈ Dom(s1 ) a2 /s1 → v2 /s2
v
s, (a1 := a2 ) → ( )s2 + [` ← v2 ]
Exercice 5.4 L’eta-expansion a pour effet de changer l’ordre dans lequel une fonction entrelace
passage d’arguments et calculs internes. Par exemple:
let f = fun x →
print_string "f";
fun y → (x, y) in
let g = f 1 in
(g true, g "hello")
La chaı̂ne f est affichée une seule fois, alors que si l’on fait une eta-expansion dans la définition de
g (afin de la rendre non-expansive), on obtient:
let f = fun x →
print_string "f";
fun y → (x, y) in
let g = fun y → f 1 y in
(g true, g "hello")
et maintenant f est affichée deux fois. Toute fonction qui effectue des effets de bords entre le
passage de deux arguments permet donc d’observer une différence de comportement lorsqu’on eta-
expanse une application partielle de cette fonction. De tels exemples n’apparaissent cependant que
très rarement en pratique. Un peu plus plausible est l’exemple de fonctions qui font une grande
quantité de calculs (sans effets de bord) entre le passage de deux arguments. Là, l’eta-expansion va
changer non pas la sémantique du programme, mais son temps d’exécution. Exemple: on considère
une fonction qui trie des tables (clé, valeurs) par ordre croissant des clés. On peut vouloir l’écrire
sous la forme d’une fonction qui prend d’abord le tableau des clés, calcule la permutation qui trie
ces clés, puis prend un tableau de valeurs et y applique la permutation:
Cette écriture est avantageuse si l’on s’attend à avoir plusieurs tables de valeurs qui partagent les
mêmes clés: on peut alors calculer la permutation de tri une seule fois.
122
Avec la restriction de la généralisation aux expressions non-expansives, fonction_de_tri devient
monomorphe, et donc l’écriture ci-dessus n’est possible que si données1 et données2 sont du même
type. Mais sinon, il faut faire une eta-expansion sur fonction_de_tri:
Si ∅ ` a : τ , alors ou bien a est une valeur, ou bien a = raise(v) pour une certaine
valeur v, ou bien il existe un terme a0 tel que a → a0 .
La preuve de ce lemme est semblable à celle de la proposition 2.6, avec des cas supplémentaires
montrant que si une sous-expression est raise(v), alors l’expression tout entière se réduit, soit par
la règle pour try raise(v) with . . ., soit par la règle pour ∆(raise(v)).
Finalement, on obtient qu’une expression a close et bien typée se réduit en une valeur, ou se
réduit en raise(v), ou diverge.
Exercice 5.6 Avec les exceptions, on peut écrire une fonction qui a plusieurs résultats: son
résultat “normal” (la valeur du corps de la fonction) plus un autre résultat qui est renvoyé en
levant une exception contenant cet autre résultat dedans. Autant le type du résultat “normal”
est apparent dans le type de la fonction (et ne peut donc être plus complexe que le type de la
fonction elle-même), autant le type du résultat “exceptionnel” n’est pas visible dans le type de la
fonction et peut être plus complexe que ce dernier. En appliquant cette idée, on peut “cacher”
une fonctionnelle de type (int → int) → (int → int) à l’intérieur d’une humble fonction de type
int → int:
123
exception M of (int → int) → (int → int)
La fonction f cachée dans le résultat de cacher f peut ensuite être extraite par la fonction suivante:
Ceci permet d’exprimer l’exemple bien connu de λ-terme qui boucle (λf.f f ) (λf.f f ) de la manière
suivante:
On peut aussi définir l’opérateur de point fixe fix = λf. (λg.λx.f (g g) x) (λg.λx.f (g g) x) comme
suit:
124
Appendix E
Exercice 6.1
Exercice 6.2
E ` v1 : τ1 ... E ` en : τn
E ` proje : {ei : Pre τ ; . . .} → τ E ` {e1 = v1 ; . . . ; en = vn } : {e1 : Pre τ1 ; . . . ; en : Pre τn ; ∅}
E ` proje ({e1 = v1 ; . . . ; en = vn }) : τ
125
Hypothèse (H1) pour extene : supposons E ` extene ({e1 = v1 ; . . . ; en = vn }, v) : τ . Si e n’est
pas l’une des ei , la dérivation de ce typage est de la forme:
E ` v1 : τ1 ... E ` en : τn
E ` {e1 = v1 ; . . . ; en = vn } : τ 0 E ` v : τv
E ` extene : τ 0 × τv → τ E ` ({e1 = v1 ; . . . ; en = vn }, v) : τ 0 × τv
E ` extene ({e1 = v1 ; . . . ; en = vn }, v) : τ
Forme des valeurs selon leur type: on examine les règles de typage qui peuvent s’appliquer
à des valeurs (const-inst, op-inst, fun, paire, record) et on remplit la matrice suivante des combi-
naisons (valeur, type) possibles:
(Rappelons que par l’hypothèse H0 un opérateur a toujours un type flèche). De plus, le type d’une
valeur enregistrement {. . . ei = vi . . .} est nécessairement de la forme {. . . ei : Pre τi . . . ; ∅} avec
∅ ` vi : τi . Donc, toutes les étiquettes marquées présentes dans ce type enregistrement sont bien
présentes dans la valeur.
Hypothèse (H2) pour proje : supposons ∅ ` proje (v) : τ . Vu le schéma de type de proje , nous
avons ∅ ` v : {e : Pre τ1 ; τ2 }. Donc, v est un enregistrement et contient un champ étiqueté e. Par
conséquent, l’application de proje se réduit par la delta-règle pour les projections.
Exercice 6.3
Algorithme de sortage: S(τ, κ, K) = K 0 si τ est de la sorte κ, ou échec sinon.
• Si τ = α et α ∈
/ Dom(K):
prendre K 0 = K + {α ← κ}.
126
• Si τ = α et α ∈ Dom(K):
si κ = K(α), prendre K 0 = K, sinon échec.
• Si τ = T :
si κ = TYPE, prendre K 0 = K, sinon échec.
• Si τ = τ1 → τ2 ou τ = τ1 × τ2 :
si κ = TYPE, prendre K 0 = S(τ2 , TYPE, S(τ1 , TYPE, K)), sinon échec.
• Si τ = {τ 0 }:
si κ = TYPE, prendre K 0 = S(τ 0 , R(∅), τ 0 ), sinon échec.
• Si τ = ∅:
si κ = R(E) pour un certain E, prendre K 0 = K, sinon échec.
• Si τ = (e : τ1 ; τ2 ):
Si κ = TYPE ou κ = PRE, échec.
Si κ = R(E) et e ∈ E, échec.
Si κ = R(E) et e ∈ / E, prendre K 0 = S(τ2 , R(E ∪ {e}), S(τ1 , TYPE, K)).
• Si τ = Abs:
si κ = PRE, prendre K 0 = K, sinon échec.
• Si τ = Pre τ 0 :
si κ = PRE, prendre K 0 = S(τ 0 , TYPE, K), sinon échec.
Exercice 6.4
L’idée est d’interpréter la rangée τ dans le type somme [τ ] comme un “ou”, et non plus comme
un “et” comme dans le cas des enregistrements. Ainsi, le type enregistrement {e : Pre int; f :
Pre bool; ∅} signifie “il y a un champ e de type int et un champ f de type bool et rien d’autre”.
Le type somme [C : Pre int; D : Pre bool; ∅] signifie, lui, “il y a un constructeur C qui porte
un argument de type int ou un constructeur D d’argument bool ou rien d’autre”. Si la rangée
se termine par une variable α au lieu de ∅, cela signifie “. . . ou d’autres constructeurs” au lieu de
“. . . ou rien d’autre”. Avec ces intuitions, on obtient les types suivants pour les opérateurs:
C : ∀α, β. α → [C : Pre α; β]
PC : ∀α. [C : Pre α; ∅] → α
FC : ∀α, β, γ. [C : Pre α; β] × (α → γ) × ([β] → γ) → γ
127
Le type de PC exprime que l’argument doit posséder le constructeur C et aucun autre, c.à.d.
que l’on est sûr statiquement que la projection ne peut pas échouer.
Enfin, le type de FC indique que le premier argument doit contenir le constructeur C et peut-
être d’autres constructeurs. Le second argument doit s’appliquer à l’argument de C. Quant au
troisième argument, il doit s’appliquer à tous les constructeurs qui peuvent être dans le premier
argument, sauf C. En effet, le troisième argument ne sera jamais appliqué si le premier est de
constructeur C. On obtient en particulier les types suivants:
La première fonction correspond, en ML, à un filtrage “ouvert” (avec un cas par défaut à la fin):
elle peut s’appliquer à n’importe quelle somme contenant au moins le constructeur C d’argument
int. La seconde fonction correspond à un filtrage “fermé” (sans cas attrape-tout à la fin): elle ne
peut s’appliquer qu’à des sommes qui contiennent au plus les constructeurs C et D.
128
Appendix F
Exercice 7.1 La réflexivité τ <: τ est immédiate par récurrence structurelle sur τ . Pour la
transitivité (τ1 <: τ2 et τ2 <: τ3 implique τ1 <: τ3 ) on procède par récurrence structurelle sur
τ1 , τ2 , τ3 et par cas sur le constructeur de tête de ces trois types. On est forcément dans l’un des
cas suivants:
τ1 τ2 τ3
T T T On a bien T <: T par axiome
α α α Là aussi, α <: α est un axiome
ϕ1 → ψ 1 ϕ2 → ψ 2 ϕ3 → ψ 3 On a ϕ3 <: ϕ2 et ϕ2 <: ϕ1 et ψ1 <: ψ2 et ψ2 <: ψ3 .
Par hypothèse de récurrence, ϕ3 <: ϕ1 et ψ1 <: ψ3 .
D’où ϕ1 → ψ1 <: ϕ3 → ψ3 par la règle de sous-typage
des types flèche.
ϕ1 × ψ 1 ϕ2 × ψ 2 ϕ3 × ψ 3 Même raisonnement que pour les types flèche.
hϕ1 i hϕ2 i hϕ3 i On a ϕ1 <: ϕ2 et ϕ2 <: ϕ3 , d’où ϕ1 <: ϕ3 par hy-
pothèse de récurrence, et hϕ1 i <: hϕ3 i par la règle de
sous-typage des types objets.
∅ ∅ ∅ ∅ <: ∅ par axiome.
τ1 ∅ ∅ τ1 <: ∅ par axiome.
τ1 τ2 ∅ τ1 <: ∅ par axiome.
m : ϕ1 ; ψ 1 m : ϕ2 ; ψ 2 m : ϕ3 ; ψ 3 Même raisonnement que pour les types produit.
129
Exercice 7.2 Supposons E ` (fun x → a) v : τ . Une dérivation de ce typage est nécessairement
de la forme suivante:
E + {x : ϕ1 } ` a : τ1
E ` fun x → a : ϕ1 → τ1 ϕ1 → τ1 <: ϕ2 → τ2
..
.
E ` fun x → a : ϕn → τn ϕn → τn <: ϕ → τ
E ` fun x → a : ϕ → τ E`v:ϕ
E ` (fun x → a) v : τ
En effet, les règles de typage ne sont plus dirigées par la syntaxe: pour tout terme a, il y a deux
règles qui peuvent dériver E ` a : τ , la règle (sub) et la règle propre à la forme de a ([Link]. (fun) si
a est une fonction). Donc, la forme générale d’une dérivation de E ` fun x → a : ϕ → τ est une
étape de règle (fun) suivie par zéro, une ou plusieurs étapes de (sub).
Par transitivité du sous-typage (exercice 7.1), nous avons ϕ1 → τ1 <: ϕ → τ , ce qui implique
ϕ <: ϕ1 et τ1 <: τ . Appliquant la règle (sub), on a donc E ` v : ϕ1 . Comme de plus E + {x : ϕ1 } `
a : τ1 , un lemme de substitution analogue au lemme 2.2 montre que E ` a[x ← v] : τ1 . Appliquant
une dernière fois la règle (sub), il vient E ` a[x ← v] : τ ; c’est le résultat attendu.
Exercice 7.3 Tout terme du lambda-calcul pur peut être vu comme une expression de mini-ML
ayant le type τ = µα. α → α. Considérons par exemple fun x → a. Si sous l’hypothèse x : τ le
type de a est τ , alors fun x → a a le type τ → τ qui par enroulage est égal à τ . De même, si a1
et a2 ont le type τ , alors par déroulage a1 a aussi le type τ → τ , donc l’application a1 a2 est bien
typée et a le type τ .
Exercice 7.4
1)
______ _________
| | | |
-> * * -> | -> |
/ \ / \ / \ / \ | / \ |
int bool V V \ / int \____| V -> |
V / \ |
V \____|
2) La substitution renvoyée a deux classes d’équivalence: l’une contient les trois noeuds → du
graphe de départ, et l’autre les trois noeuds représentant int, α et β dans le graphe de départ.
3) Tout d’abord, il est clair que si R est une relation d’équivalence et R0 = mgu(E, R) est définie,
alors R0 est une relation d’équivalence, et de plus les classes d’équivalence de R sont incluses dans
celles de R0 .
Ensuite, considérons un appel mgu(E, R) qui, récursivement, appelle mgu(E 0 , R0 ). Dans tous les
? ?
cas de l’algorithme, pour tout (n1 = n2 ) ∈ E, on a ou bien (n1 = n2 ) ∈ E 0 , ou bien n1 R n2 .
130
Donc, par récurrence sur le déroulement de l’algorithme, il vient que R = mgu(E, id ) satisfait les
?
équations de E: pour tout (n1 = n2 ) ∈ E, on a n1 R n2 .
Il reste à vérifier que R = mgu(E, id ) vérifie les conditions de compatibilité et de fermeture. Si
n R n0 et C(n) 6= V et C(n0 ) 6= V , alors forcément une des étapes de l’algorithme a été
? ? ?
mgu({n = n0 } ∪ E, R) = mgu(E ∪ {F1 (n) = F1 (n0 ); . . . ; Fk (n) = Fk (n0 )}, R + {n = n0 })
si C(n) 6= V et C(n0 ) = C(n) et k = A(C(n))
?
Donc C(n) = C(n0 ), et de plus la relation R satisfait les équations de E ∪ {F1 (n) =
?
F1 (n0 ); . . . ; Fk (n) = Fk (n0 )}, d’où Fi (n) R Fi (n0 ) pour tout i. Par conséquent, R est une sub-
stitution, et comme elle satisfait toutes les équations de E, c’est un unificateur de E.
Soit maintenant R0 un unificateur de E. On montre par récurrence sur le déroulement de
l’algorithme que si R1 est plus fine que R0 et R2 = mgu(E, R1 ), alors R2 est plus fine que R0 .
Faisons par exemple le cas
? ? ?
mgu({n = n0 } ∪ E, R1 ) = mgu(E ∪ {F1 (n) = F1 (n0 ); . . . ; Fk (n) = Fk (n0 )}, R1 + {n = n0 })
si C(n) 6= V et C(n0 ) = C(n) et k = A(C(n))
?
Puisque R0 est un unificateur de {n = n0 } ∪ E, on a nécessairement n R0 n0 . Comme R0 est une
relation d’équivalence et qu’elle est moins fine que R1 , elle est aussi moins fine que R1 +{n = n0 }. De
? ?
plus, R0 est un unificateur de E ∪ {F1 (n) = F1 (n0 ); . . . ; Fk (n) = Fk (n0 )} puisque c’est un unificateur
?
de E ∪ {n = n0 } et puisque R0 satisfait la condition de fermeture. Appliquant l’hypothèse de
? ?
récurrence, il vient que R2 = mgu(E ∪ {F1 (n) = F1 (n0 ); . . . ; Fk (n) = Fk (n0 )}, R1 + {n = n0 }) est
?
plus fine que R0 . C’est le résultat attendu, puisque R2 = mgu({n = n0 } ∪ E, R1 ).
4) À chaque appel récursif de mgu(E, R), ou bien le nombre de classes d’équivalences de R
diminue d’un, ou bien R est inchangé mais le nombre d’équations de E diminue d’un. Ceci garantit
que mgu ne peut pas boucler.
Exercice 7.5
1) La symétrie est évidente par récurrence sur les deux types.
Si d(τ1 , τ2 ) = 0, ou bien τ1 et τ2 sont la même variable de type, ou bien τ1 et τ2 sont deux types
flèche ϕ1 → ψ1 et ϕ2 → ψ2 , et d(ϕ1 , ϕ2 ) = 0 et d(ψ1 , ψ2 ) = 0. Par récurrence, il vient ϕ1 = ϕ2 et
ψ1 = ψ2 , d’où τ1 = τ2 .
Pour l’inégalité du triangle ultramétrique, on raisonne par récurrence et par cas sur les trois
types τ1 , τ2 , τ3 . On dit que deux types sont en désaccord si ce sont deux variables différentes, ou
si l’un est un type flèche et l’autre une variable. La distance entre deux types en désaccord est
toujours 1.
Si τ1 et τ2 sont en désaccord, ou τ2 et τ3 en désaccord: alors max(d(τ1 , τ2 ), d(τ2 , τ3 )) = 1 et
l’inégalité est vérifiée, car d(τ1 , τ3 ) ≤ 1 quels que soient τ1 et τ3 .
Si τ1 = τ2 = τ3 = α, les trois distances sont nulles et l’inégalité est vérifiée.
Enfin, si τ1 = ϕ1 → ψ1 et τ2 = ϕ2 → ψ2 et τ3 = ϕ3 → ψ3 : par hypothèse de récurrence, on a
d(ϕ1 , ϕ3 ) ≤ max(d(ϕ1 , ϕ2 ), d(ϕ2 , ϕ3 )) et de même d(ψ1 , ψ3 ) ≤ max(d(ψ1 , ψ2 ), d(ψ2 , ψ3 )). D’où:
131
≤ 1/2 max(d(ϕ1 , ϕ2 ), d(ϕ2 , ϕ3 ), d(ψ1 , ψ2 ), d(ψ2 , ψ3 ))
= max(1/2 max(d(ϕ1 , ϕ2 ), d(ψ1 , ψ2 )), 1/2 max(d(ϕ2 , ϕ3 ), d(ψ2 , ψ3 )))
= max(d(ϕ1 → ψ1 , ϕ2 → ψ2 ), d(ϕ2 → ψ2 , ϕ3 → ψ3 ))
2a) Soient (τn ) et (τn0 ) deux suites de Cauchy. On montre que la suite (d(τn , τn0 )) à valeurs dans
R est de Cauchy. En effet, pour tous p, q, on a:
d’où
d(τp , τp0 ) − d(τq , τq0 ) ≤ max(d(τp , τq ), d(τq0 , τp0 ))
et, en intervertissant les rôles de p et q,
d’où
|d(τp , τp0 ) − d(τq , τq0 )| ≤ max(d(τq , τp ), d(τp0 , τq0 )).
Soit ε > 0. Soient N1 et N2 tels que p, q ≥ N1 ⇒ d(τp , τq ) ≤ ε et p, q ≥ N2 ⇒ d(τp0 , τq0 ) ≤ ε. Pour
tous p, q ≥ max(N1 , N2 ), on a donc |d(τp , τp0 ) − d(τq , τq0 )| ≤ max(ε, ε) = ε. Donc la suite (d(τn , τn0 ))
est de Cauchy dans R. Elle converge donc.
2b) La réflexivité de ∼
= découle de d(τ, τ ) = 0 pour tout τ . La symétrie de ∼= découle de celle
∼ ∼ 0 0 ∼ 00
de d. Pour la transitivité de =, supposons (τn ) = (τn ) et (τn ) = (τn ). Pour tout n, on a:
d’où (τn ) ∼
= (τn00 ).
2c) Par passage à la limite sur l’inégalité du triangle ultramétrique, on a d(s, s00 ) ≤
max(d(s, s0 ), d(s0 , s00 )) pour toutes suites s, s0 , s00 . De même, d(s, s0 ) = d(s0 , s).
On vérifie maintenant que d passe au quotient par ∼ =. Si s ∼
= s0 et u ∼ = u0 , on a
et de même
d(s, u) ≤ max(d(s, s0 ), d(s0 , u0 ), d(u0 , u)) = d(s0 , u0 ).
∼
Donc d(s, u) = d(s0 , u0 ), et d passe au quotient par =.
Par définition de =, d(s, u) = 0 si et seulement si s ∼
∼ = u, c’est-à-dire si et seulement si s et u
sont égales dans S/ ∼=.
2d) À tout type simple τ on associe la suite constante (τ, τ, . . .). La distance entre deux telles
suites constantes (τ ) et (τ 0 ) est bien sûr d(τ, τ 0 ).
132
2e) Soit (sn ) une suite de Cauchy à valeurs dans T , c’est-à-dire une suite de Cauchy de suites
de Cauchy. On note sn,p le pième élément de la suite sn .
Par définition de T , la suite (sn,p )p∈N , vue comme suite à valeurs dans T , converge vers sn .
Donc, pour tout n > 0, il existe N (n) tel que
1
p ≥ N (n) ⇒ d(sn,p , sn ) ≤
n
On définit la suite diagonale u par un = sn,N (n) . Montrons que u est de Cauchy et que (sn )
converge vers u. Pour tous p, q, on a:
1 1
d(up , uq ) = d(sp,N (p) , sq,N (q) ) ≤ max(d(sp,N (p) , sp ), d(sp , sq ), d(sq , sq,N (q) )) ≤ max( , d(sp , sq ), )
p q
Soit ε > 0. Soit N0 tel que
p, q ≥ N0 ⇒ d(sp , sq ) ≤ ε.
Soit N1 tel que 1/N1 ≤ ε. Pour tous p, q ≥ max(N0 , N1 ), on a
1 1 1 1
d(up , uq ) ≤ max( , d(sp , sq ), ) ≤ max( , ε, )≤ε
p q N1 N1
Donc la suite u est bien de Cauchy.
Montrons que (sn ) converge vers u. Pour tous p et q,
1
d(up , sq ) = d(sp,N (p) , sq ) ≤ max(d(sp,N (p) , sp ), d(sp , sq )) ≤ max( , d(sp , sq ))
p
Soit ε > 0. Soit N0 tel que
p, q ≥ N0 ⇒ d(sp , sq ) ≤ ε.
Soit N1 tel que 1/N1 ≤ ε. Pour tous p, q ≥ max(N0 , N1 ), on a
1 1
d(up , sq ) ≤ max( , d(sp , sq )) ≤ max( , ε) ≤ ε
p N1
Faisant tendre p vers ∞, il vient d(u, sq ) ≤ ε. Donc, pour tout ε > 0, il existe N = max(N0 , N1 )
tel que q ≥ N ⇒ d(u, sq ) ≤ ε. Ceci montre que u est la limite de (sq ).
3) Unicité du point fixe: si x et y sont deux points fixes de F , on a x = F (x) et y = F (y), d’où
kn
d(xn+p , xn ) ≤ d(xn+p , xn+p−1 ) + · · · + d(xn+1 , xn ) ≤ (k n+p + · · · + k n )d(x1 , x0 ) ≤ d(x1 , x0 )
1−k
133
kN
Soit alors ε > 0. Soit N suffisamment grand pour que n ≥ N entraı̂ne 1−k d(x1 , x0 ) ≤ ε/2. Pour
tous p, q ≥ N , on a
kN kN
d(xp , xq ) ≤ d(xp , xN ) + d(xN , xq ) ≤ d(x1 , x0 ) + d(x1 , x0 ) ≤ ε
1−k 1−k
Donc la suite (xn ) est de Cauchy. Soit x sa limite. Pour tout n, on a d(xn+1 , F (x)) ≤ k d(xn , x).
Faisant tendre n vers ∞, il vient que F (x) est la limite de la suite (xn ). Par unicité de la limite, il
s’ensuit F (x) = x, et x est un point fixe de F .
4) Pour tous types finis τ, τ 0 , τ 00 , on montre par une récurrence facile sur τ que
d(τ [α ← τ 0 ], τ [α ← τ 00 ]) ≤ d(τ 0 , τ 00 )
Si de plus τ 6= α, on a
1
d(τ [α ← τ 0 ], τ [α ← τ 00 ]) ≤ d(τ 0 , τ 00 ).
2
En effet, ou bien τ est une variable de type différente de α, et alors τ [α ← τ 0 ] = τ [α ← τ 00 ], ou bien
τ est un type flèche τ1 → τ2 et alors
1 1
d(τ [α ← τ 0 ], τ [α ← τ 00 ]) ≤ max(d(τ1 [α ← τ 0 ], τ1 [α ← τ 00 ]), d(τ2 [α ← τ 0 ], τ2 [α ← τ 00 ])) ≤ d(τ 0 , τ 00 )
2 2
Cette inégalité s’étend ensuite à des types τ, τ 0 , τ 00 infinis par passage à la limite.
Par conséquent, l’opérateur F (τ 0 ) = τ [α ← τ 0 ] est contractif: d(F (τ 0 , τ 00 )) ≤ 12 d(τ 0 , τ 00 ). Appli-
quant le théorème de Banach-Tarski, il vient qu’il existe un et un seul point fixe τ 0 de F . Donc,
τ 0 = τ [α ← τ 0 ] et τ 0 est le seul type qui vérifie cette égalité.
134
Appendix G
Exercice 8.1
E; S1 ; . . . ; Sn ` Si <: Si (1)
pour tout i = 1, . . . , n.
Si Si = (val v : σ), on a E; S1 ; . . . ; Sn ` σ ≈ σ (axiome de transitivité sur ≈ plus règle
(schémas)), d’où (1) par application de la règle (sub-val).
Si Si = (type t), (1) s’ensuit de la règle (sub-abstr-abstr).
Si Si = (type t = τ ), on a E; S1 ; . . . ; Sn ` τ ≈ τ par la règle (eq-réflexivité), d’où (1) par la
règle (sub-mani-mani).
Si Si = (module X : M1 ), on a E; S1 ; . . . ; Sn ` M1 <: M1 par application de l’hypothèse de
récurrence (M1 est un sous-terme strict de M ). Utilisant la règle (sub-mod), on conclut (1).
D’où le résultat attendu, E ` M <: M , par application de la règle (8).
Cas M = functor(X : M1 ) → M2 . En appliquant l’hypothèse de récurrence à M1 , on obtient
E ` M1 <: M1
et en l’appliquant à M2 ,
E; module X : M1 ` M2 <: M2
D’où E ` M <: M en appliquant la règle (sub-foncteur). 2
Pour prouver la transitivité de <:, il faut introduire une relation de sous-typage entre en-
vironnements de typage. Un environnement de typage peut être vu comme l’intérieur d’une
signature sig . . . end: les deux sont des séquences de spécifications. On dit par conséquent
que deux environnements E et A0 sont en relation de sous-typage, et on note ` E <: A0 , si
135
∅ ` sig E end <: sig A0 end; c’est-à-dire, notant E = S1 ; . . . ; Sm et A0 = S10 ; . . . ; Sn0 , il existe une
injection ρ telle que E ` Sρ(i) <: Si0 pour tout i = 1, . . . , n.
L’intérêt de cette notion est que, si ` E <: E 0 , tout résultat de typage qui peut être dérivé sous
les hypothèses E 0 peut également être dérivé sous les hypothèses E (hypothèses plus fortes). Plus
précisément, on a le lemme suivant:
1. Si E 0 ` τ ≈ τ 0 , alors E ` τ ≈ τ 0 .
2. Si E 0 ` σ ≥ σ 0 , alors E ` σ ≥ σ 0 .
Démonstration: par récurrence structurelle sur les types M , M 0 , M 00 . Vu les règles (sub-sig) et
(sub-foncteur), ces trois types sont ou bien trois signatures, ou bien trois types de foncteurs.
Cas M = sig S1 ; . . . ; Sm end et M 0 = sig S10 ; . . . ; Sn0 end et M 00 = sig S100 ; . . . ; Sp00 end. La seule
règle ayant pu conclure E ` M <: M 0 et E ` M 0 <: M 00 est la règle (sub-sig). Ses prémisses
sont donc nécessairement vraies. Il existe donc deux injections ϕ : {1 . . . n} 7→ {1 . . . m} et ψ :
{1 . . . p} 7→ {1 . . . n} telles que
136
Considérons alors ρ = ϕ ◦ ψ. C’est une injection de {1 . . . p} dans {1 . . . m}. Fixons i dans {1 . . . p}.
Par (2) et (4), nous avons
0 0
B ` Sρ(i) <: Sψ(i) et B ` Sψ(i) <: Si00
Nous montrons maintenant que B ` Sρ(i) <: Si00 en discutant sur la forme de Sρ(i) , Sψ(i)
0 et Si00 . Les
cas suivants sont à considérer:
Sρ(i) 0
Sψ(i) Si00
val v : σ val v : σ 0 val v : σ 00 On a B ` σ ≥ σ 0 et B ` σ 0 ≥ σ 00 , d’où
B ` σ ≥ σ 00 car ≥ est transitive, et le
résultat attendu par la règle (sub-val).
type t Trivial par (sub-mani-abstr) ou (sub-
abstr-abstr).
type t type t type t = τ 00 De (4) il vient B ` t ≈ τ 00 , d’où le résultat
par la règle (sub-abstr-mani).
type t type t = τ 0 type t = τ 00 De (4) il vient B ` t ≈ τ 0 et B ` τ 0 ≈ τ 00 ,
d’où B ` t ≈ τ 00 par transitivité de ≈ et
le résultat par la règle (sub-abstr-mani).
type t = τ type t type t = τ 00 On a B ` t ≈ τ 00 , et d’autre part B `
t ≈ τ trivialement puisque B contient
l’hypothèse type t = τ . D’où le résultat
par transitivité de ≈ et la règle (sub-mani-
mani).
type t = τ type t = τ 0 type t = τ 00 Transitivité de ≈ et règle (sub-mani-
mani).
module X : M1 module X : M10 module X : M100 On a B ` M1 <: M10 et B ` M10 <: M100 .
Les types M1 , M10 , M100 étant sous-termes
stricts de M, M 0 , M 00 respectivement, on
peut appliquer l’hypothèse de récurrence,
obtenant B ` M1 <: M100 et le résultat
attendu via la règle (sub-mod).
Ayant ainsi montré B ` Sρ(i) <: Si00 pour tout i = 1, . . . , p, nous pouvons conclure
137
On a clairement ` (E; module X : P 00 ) <: (E; module X : P 0 ), d’où par la proposition G.2,
ρ permutation de {1 . . . n}
E ` σ ≈ σ0
E; S1 ; . . . ; Sn ` Sρ(i) ≈ Si0 pour i = 1, . . . , n
E ` (val v : σ) ≈ (val v : σ 0 )
E ` (sig S1 ; . . . ; Sn end) ≈ (sig S10 ; . . . ; Sn0 end)
E`τ ≈t E ` τ ≈ τ0
E ` (type t) ≈ (type t)
E ` (type t = τ ) ≈ (type t) E ` (type t = τ ) ≈ (type t = τ 0 )
E`τ ≈t E ` M ≈ M0
E ` (type t) ≈ (type t = τ ) E ` (module X : M ) ≈ (module X : M 0 )
E ` P1 ≈ P2 E; module X : P2 ` R1 ≈ R2
E ` (functor (X : P1 ) → R1 ) ≈ (functor (X : P2 ) → R2 )
Exercice 8.3 Informellement, toute signature qui ne contient pas de spécification de type abstrait
possède toujours une signature équivalente (au sens de l’exercice 8.2) dans laquelle il n’y a pas de
dépendances entre les composantes. On l’obtient en expansant de manière répétée les égalités sur
les types manifestes dans le reste de la signature. Par exemple, si on part de la signature
module type S =
sig
type t = int
type u = t
module X : sig val v : u end
end
et qu’on remplace chaque utilisation de u par t, puis chaque utilisation de t par int, on obtient la
signature non-dépendante équivalente
sig
type t = int
type u = int
module X : sig val v : int end
end
138
D’autre part, si un chemin p a une signature M , on peut toujours lui attribuer la signature M/p
(règle de renforcement), dans laquelle toute les spécifications de types sont manifestes.
En combinant les deux remarques, l’idée est donc de remplacer chaque utilisation des règles de
projections non restreintes (eq-projection), (val-projection) et (mod-projection) par une étape de
renforcement (mod-renforcement), une étape de sous-typage vers un type non dépendant équivalent
(mod-sub), une projection restreinte (eq-projection’), (val-projection’), (mod-projection’), et enfin
une étape d’équivalence de type ou de sous-typage (equiv), (mod-sub) pour revenir au type ini-
tialement obtenu comme conclusion de (eq-projection), (val-projection), (mod-projection). Faisons
le cas (val-projection) plus en détails. Considérons une occurrence de
E ` p : sig S1∗ ; val v : σ; S2∗ end τ ≤ σ{z ← p.z | z lié dans S1∗ }
E ` p.v : τ
dans une dérivation. Notons M = sig S1∗ ; val v : σ; S2∗ end et M 0 la signature non dépendante
équivalente à M/p. Par construction, M 0 est de la forme sig S10∗ ; val v : σ 0 ; S20∗ end. On peut
donc construire la dérivation suivante:
E`p:M
E ` p : M/p E ` M/p <: M 0
E ` p : M0 L(σ 0 ) ∩ B(S10∗ ) = ∅ τ 0 ≤ σ0
E ` p.v : τ 0 E ` τ0 ≈ τ
E ` p.v : τ
Il reste bien sûr à montrer que E ` τ 0 ≈ τ . Ceci découle de E ` σ 0 ≈ σ, qui est conséquence des
lemmes suivants:
1. Si E ` p : M , alors E ` M ≈ M/p.
3. Si E ` (sig S1∗ ; val v : σ; S2∗ end) <: (sig S10∗ ; val v : σ 0 ; S20∗ end), alors
139