Chapitre 3

Ajout de constructions impératives.

Les variantes du noyau du langage ML étudiées précédemment ne possèdent que des constructions fonctionnelles. Dans ce chapitre nous considérons des extensions de ML avec des constructions impératives. Nous étudions en détail une extension indispensable : l’ajout d’objets mutables. Nous présentons plus brièvement les autres constructions impératives : exceptions, continuations, communications.

3.1 Constructions impératives

Dans les langages purement fonctionnels, si une expression close a_{1} se réduit en une expression a_{2} (en respectant la stratégie du langage, par exemple appel par valeur), alors les programmes E[a_{1}] et E[a_{2}] sont équivalents, c’est-à-dire qu’ils terminent sur les mêmes entrées et retournent les mêmes valeurs. Formellement cela découle de la règle de réduction Contexte.

Cette propriété implique qu’il n’y a pas de notion de partage, puisqu’il est toujours possible de remplacer une valeur liée à une variable x par un programme qui reconstruit cette valeur. Elle implique également que plusieurs évaluations d’une même expression avec les mêmes paramètres produisent toujours le même résultat. On peut alors “comprendre” une fonction du langage comme une fonction mathématique dans un certain ensemble d’objets représentants les valeurs du langage. C’est ce que fait la sémantique dénotationnelle. La sémantique opérationnelle (naturelle ou à réduction) d’un langage purement fonctionnel est elle-même très simple, parce que la sémantique d’un programme peut s’exprimer uniquement en fonction de ce programme et des valeurs de ses arguments au cours de son évaluation.

Pourtant, il est de nombreuses situations où l’on souhaite que plusieurs évaluations successives d’une même expression produisent des résultats différents : C’est le cas, par exemple, si l’on veut réaliser un compteur. De façon abstraite, un compteur est un objet que nous pouvons interroger pour connaître sa valeur ; nous pouvons aussi l’incrémenter. Son interface pourra être de la forme :

    lire : unit → int
    incrémenter : unit → unit

Clairement, plusieurs exécutions de la fonction lire séparées par des exécutions de la fonction incrémenter doivent retourner des résultats différents. Il y a forcément des paramètres cachés ; ce sont des cellules mémoire partagées entre les fonctions lire et incrémenter qui peuvent consulter et affecter la mémoire. Nous parlerons d’objets mutables ou de références plutôt que de cellules mémoire.

Les objets mutables permettent également de simuler la liaison dynamique en la remplaçant par une liaison statique sur un objet mutable. Ils correspondent bien entendu à la notion de pointeurs des langages Pascal, C, etc. Ils permettent également de coder des structures de graphe par des graphes en mémoire, ce qui est souvent indispensable pour écrire certains algorithmes de manière efficace. Il est clair également que les communications entre un programme et le monde extérieur (la mémoire) s’effectuent de façon impérative ; un fichier peut être vu comme un objet dans lequel il est possible, en général, de lire et d’écrire. Par exemple, plusieurs lectures successives retourneront les caractères consécutifs du fichier.

Enfin, il existe d’autres formes de constructions impératives que les objets mutables. Par exemple, les exceptions, et plus généralement, les opérations de contrôle. Les canaux de communications dans les langages parallèles sont également des opérations essentiellement impératives. Les objets mutables sont donc indispensables, et il n’est guère de programmes réels qui puissent aisément s’en priver.

3.2 Une sémantique à réduction pour les objets mutables

Dans le chapitre 1, nous avons décrit la sémantique opérationnelle du noyau ML par réduction des expressions du langage sur elles-mêmes jusqu’à aboutir à une forme normale, qui s’est révélée être toujours une valeur pour les programmes bien typés.

Nous limitons maintenant notre étude à l’ajout de références au langage ML, la forme la plus simple d’objets mutables. Plutôt que d’étendre la syntaxe du langage, nous essayons d’ajouter deux primitives (ref ) et (! ) d’arité 1 et une primitive ( := ) d’arité 2.

Comment expliquer le comportement de ref v, ou plus difficile encore, celui de v_{1} := v_{2} dont le seul effet est global, plus précisément celui de changer le comportement ultérieur de toutes les lectures de v_{1} ? Au début de ce chapitre, nous avons justifié l’introduction des constructions impératives dans le langage par la nécessité d’invalider parfois la règle de réduction Contexte de la partie 2.1, page 15 que nous rappelons ci-dessous :

si a_{1} ⟶ a_{2}, alors E[a_{1}] ⟶ E[a_{2}]

Nous ne pourrons donc pas donner une sémantique du langage simplement en ajoutant de nouvelles règles pour réduire les opérations manipulant des références.

3.2. UNE SÉMANTIQUE À RÉDUCTION POUR LES OBJETS MUTABLES 31

Utilisons l’idée intuitive de cellule mémoire. Nous nous donnons un ensemble infini dénombrable de locations mémoire que nous désignerons par la lettre ℓ. Nous définissons un état mémoire comme une fonction de domaine fini des locations mémoire vers les valeurs. Nous les désignons par la lettre s. De façon informelle, une référence ref v s’évalue en une nouvelle location mémoire non encore utilisée ℓ, augmentant ainsi l’état mémoire s d’une liaison ℓ ↦ v. Nous devons donc étendre le langage afin de pouvoir y manipuler les locations. Pour cela, nous étendons la syntaxe des expressions avec les locations mémoire. Nous considérons les locations mémoire comme des valeurs, i.e. nous étendons la définition de v par (les “...” signifient que nous étendons la définition précédente) :

v ::= … | ℓ

Nous pouvons maintenant décrire la sémantique du langage. La relation de réduction est définie sur des paires notées a/s formées d’une expression a et d’un état mémoire s. Elle est définie comme la plus petite relation satisfaisant les règles de la figure 3.1. Les règles Fun et Let ne consultent ni ne modifient l’état mémoire. Pour évaluer une

(fun (x) a) v/s ⟶ a[v/x]/s  Fun
let x = v in a/s ⟶ a[v/x]/s  Let
If ℓ ∉ dom (s),  ref v/s ⟶ ℓ/s ⊕ (ℓ : v)  Ref
If ℓ ∈ dom (s),  !ℓ/s ⟶ s(ℓ)/s  Deref
If ℓ ∈ dom (s),  ℓ := v ⟶ v/s ⊕ (ℓ : v)  Assign
If a_{1}/s_{1} ⟶_{ϵ} a_{2}/s_{2},  E[a_{1}]/s_{1} ⟶ E[a_{2}]/s_{2}  Contexte

Figure 3.1 : Règles de réduction avec objets mutables

expression ref a on évalue a en une valeur v puis on alloue une location mémoire ℓ avec la valeur initiale v et on retourne cette location en résultat. L’opération !a retourne la valeur v pourvu que a s’évalue en une location de contenu v. L’opération a_{1} := a_{2} modifie, si a_{1} s’évalue en une location, le contenu de cette location avec le résultat v_{2} de l’évaluation de a_{2} et retourne v_{2}. En fait, la valeur retournée par l’affectation importe peu tant que ce choix est cohérent avec les règles de typage. Par exemple, il serait possible de retourner la valeur sans information unit, mais il faudrait introduire cette nouvelle constante dans le langage. Les contextes d’évaluation sont inchangés.

Ainsi l’évaluation d’un programme a se fait en réduisant le programme dans un état mémoire initial vide et conduit, si l’évaluation termine, à une valeur v dans un état mémoire final s. Cet état mémoire représente toute la mémoire utilisée au cours du calcul. En général, la valeur v contient des locations liées dans l’état mémoire et ne peut pas en être séparée. En revanche, la mémoire possède sans doute des locations qui ne sont plus utilisées. La récupération de la mémoire ne peut pas être formalisée simplement en ajoutant une règle d’évaluation locale qui jetterait les locations inaccessibles. Il faudrait englober la réduction dans une relation définie sur les programmes uniquement (et non pas définie récursivement sur les sous-expressions) puis ajouter une règle globale de glanage de cellules. Il est aussi possible de rendre la notion de mémoire complètement locale, mais au prix d’une complication du formalisme [?].

3.3 Typage des références

Nous allons voir qu’une extension naïve n’est pas correcte. Nous étendons d’abord les types avec un symbole Ref :

τ ::= … | τ Ref

Le traitement des constructions impératives comme des constantes conduit aux règles de typage dérivées suivantes :

(Ref)

\frac{A ⊢ a : τ}{A ⊢ ref a : τ Ref}

(Deref)

\frac{A ⊢ a : τ Ref}{A ⊢ !a : τ}

(Assign)

\frac{A ⊢ a_{1} : τ Ref A ⊢ a_{2} : τ}{A ⊢ a_{1} := a_{2} : τ}

Cependant, la combinaison de ces règles avec la règle Let déjà présente est incorrecte. En effet, considérons le programme suivant :

    let I = ref (fun x → x);;
    I := succ;;
    !I (fun (x) x):;;

Il est facile de vérifier que ce programme est bien typé pour les règles ci-dessus. Son évaluation est cependant bloquée. En effet, l’évaluation de la dernière phrase se réduit à l’application du contenu de I, qui est alors la fonction qui attend un entier, à la fonction fun (x) x qui n’est donc pas un entier. L’identificateur I est lié à une référence de type ∀ α. α → α. Dans la seconde phrase, il est vu, grâce au lemme de substitution, comme liée à une référence de type Int → Int. Cette phrase est donc bien typé. Son exécution remplace le contenu de I par la valeur succ. Cependant, I dont le type n’a pas changé peut être vu dans la dernière phrase comme une référence vers une valeur de type (α_{1} → α_{1}) → α_{0}, ce qui est erroné. L’incohérence est d’avoir remplacé une référence par une valeur dont le type est moins polymorphe que celui de la valeur initiale.

Le problème est encore plus apparent si on l’analyse formellement. Ayant introduit des locations mémoire puis une mémoire, nous devons d’abord leur donner une contrepartie dans le typage. Dans un premier temps, il est nécessaire d’étendre les environnements de typage aux locations mémoire :

A ::= … | A ⊕ (ℓ : ∀ ᾱ. τ)

Le problème décrit plus haut apparaît dès qu’une location a un type polymorphe, puisqu’il est alors possible de remplacer cette location par une valeur de type τ[τ̄_{1}/ᾱ] puis de la lire comme une valeur de type τ[τ̄_{2}/ᾱ], ce qui sera erroné au moins chaque fois que τ̄_{1} et τ̄_{2} sont des instances incompatibles.

Il suffit donc interdire de créer des locations mémoire avec un type polymorphe, c’est-à-dire imposer :

A ::= … | A ⊕ (ℓ : τ)

Il ne faut pas oublier d’ajouter une règle de typage pour les locations mémoire :

\begin{aligned}ℓ : τ ∈ A \\ & (Loc) \\ A ⊢ ℓ : τ Ref \end{aligned}

L’ajout de cette règle change a priori le système de typage et donc les résultats associés. Cependant, il est facile de voir que A ⊢ a : τ est correct dans le système avec locations si et seulement si A′ ⊢ a′ : τ est correct dans le système sans locations, où A′ est obtenu en remplaçant ℓ : τ dans A par x_{ℓ} : τ Ref et a′ en remplaçant ℓ par x_{ℓ} dans a. Les variables x_{ℓ} sont bien entendu des variables qui n’apparaissent pas dans A ni dans a. Cette correspondance, permet de transporter les propriétés du typage de ML à ML avec locations (3.3).

Le critère de correction “Ne pas créer de location mémoire de type polymorphe” fait intervenir la sémantique dynamique puisque les locations n’apparaissent pas dans le programme initial. Il faut donc trouver un critère statique qui garantit le critère dynamique. Allons plus loin dans la formalisation et relions le type des locations au type des valeurs liées par ces locations.

Nous dirons qu’un état mémoire s est en accord avec un environnement de typage A, et nous noterons ⊢ s : A, si s et A sont définis sur exactement les mêmes locations mémoire, et si pour toute location mémoire de ce domaine nous avons A ⊢ s(ℓ) : A(ℓ).

Il s’agit donc de ne pas donner un type polymorphe aux valeurs qui pourraient initialiser la création de références, ce que l’on peut garantir de deux façons simples et opposées :

1. Ne sachant pas quand les références seront effectivement créées, on interdit de généraliser les variables de type qui apparaissent dans le type de la construction d’une référence.

2. Pour interdire de généraliser une expression dont l’évaluation pourrait créer des références polymorphes, une approche drastique est de ne généraliser que le type des expressions qui sont des valeurs (dont l’évaluation ne fait rien, donc ne crée rien).

La lecture d’une référence et sa modification ne posent alors plus de problème. Chacune des hypothèses ci-dessus peut être garantie par une modification simple du typage. Dans le cas (1), le plus simple est de partitionner les variables de types V en deux classes V_{N} et V_{G} de variables non généralisables et de variables généralisables. Il faut alors modifier la règle de typage des références :

(Ref)

\frac{A ⊢ a : τ F V (τ) ⊂ V_{N}}{A ⊢ ref a : τ Ref}

et conjointement restreindre la généralisation de τ dans A:

Gen(τ, A) =^{def} (F V (τ) \ F V (A)) \ V_{N}

Dans le cas (2), les règles de typages sont inchangées, mais il faut restreindre la construction de liaison aux valeurs :

a ::= … | let x = v in a

La première approche est celle qui a été longtemps utilisée pour ML, mais la seconde, de loin la plus simple est aussi celle qui tend à être communément admise comme le meilleur compromis. Pour cette raison, c’est celle-ci que nous retiendrons et pour laquelle nous montrerons la correction du typage. La première solution se formalise de façon similaire et ne pose pas de difficulté particulière.

Exercice 19 (*) Trouver un exemple intéressant de programme (i.e. un programme que l’on souhaite écrire) qui n’est pas typable par la première approche. Ce programme est-il typable avec la seconde approche ? N’existe-t-il pas un programme équivalent (qui réalise le même algorithme) qui est typable avec la seconde approche ?

Exercice 20 (*) Dans la seconde approche, il n’est plus possible d’écrire de nombreux programmes, par exemple let x = 1 + 2 in x ∗ x. Comment peut-on réintroduire la construction let x = a_{1} in a_{2} dans le cas où a_{1} n’est pas une valeur ? Pourquoi avons nous exclu ce cas ci-dessus ?

Exercice 21 (**) On suppose que la liaison est autorisée sur des expressions qui ne sont pas des valeurs comme dans l’exercice précédent. Il arrive parfois de spécialiser une fonction polymorphe g à plusieurs arguments sur le premier argument. On écrit alors un programme de la forme let g′ = g v in a. Malheureusement g′ ne sera pas polymorphe dans a. Peut-on écrire un programme équivalent qui permettent à g′ d’être polymorphe.

3.4 Correction de la sémantique

La correction du typage par rapport à la sémantique se prouve en suivant exactement la même démarche que pour le noyau ML. La seule difficulté consiste à bien énoncer la correction du typage. Ensuite, il sera facile d’adapter les preuves.

Puisque le typage des constructions impératives n’est maintenant plus restreint, nous pouvons considérer celles-ci comme des applications de constantes fonctionnelles. Nous rappelons les différentes classes syntaxiques :

a ::= x | c | a_{1} a_{2} | fun (x) a | let x = v in a_{2}
v ::= c^{k} v_{1} … v_{q} | C^{k} v_{1} … v_{k} | fun (x) a (q < k)
c ::= (ref ) | (! ) | ( := )
E ::= [] | E a | v E

En particulier, les contextes d’évaluation ne comprennent plus la construction de liaison, puisque celle-ci est maintenant restreinte à des liaisons à des valeurs. Nous nous limitons aux constantes ci-dessus dans le but de simplifier le formalisme, mais nous pourrions bien entendu abstraire le formalisme par rapport à un ensemble de constantes, leur typage et leurs δ-règles associées, comme dans le chapitre 1. Clairement, les constantes (ref ) et (! ) sont des primitives d’arité 1 et ( := ) est une primitive d’arité 2.

L’environnement de typage initial A_{0} est le suivant :

(ref ) : ∀ α. α →Ref(α)
(! ) : ∀ α. Ref(α) → α
( := ) : ∀ α. Ref(α) → α → α

Nous appelons extension mémoire d’un environnement de typage A une extension de A avec un nombre quelconque d’assertions de la forme ℓ : τ. Nous écrivons a_{1}/s_{1} ⊑ a_{2}/s_{2} si pour tout environnement de typage A_{1} et tout type τ tels que A_{1} ⊢ a_{1} : τ et ⊢ s_{1} : A_{1}, il existe une extension mémoire A_{2} de A_{1} telle que A_{2} ⊢ a_{2} : τ et ⊢ s_{2} : A_{2}.

La sécurité du typage s’exprime en reformulant les deux théorèmes 1 et 2, page 23 du chapitre 1 :

Théorème 3 (Auto-Réduction) La réduction préserve les typages (i.e. ⟶ est une sous relation de ⊑).

Théorème 4 (Formes Normales) Les expressions irréductibles et bien typées relativement à une extension mémoire de l’environnement initial sont des valeurs.

C’est-à-dire, soit A une extension mémoire de l’environnement de typage initial A_{0}. Si A ⊢ a : τ et ⊢ s : A et si a/s est irréductible, alors a est une valeur.

Le théorème d’auto-réduction est une combinaison immédiate des lemmes de contraction de radical et de remplacement dans un contexte :

Lemme 7 (Remplacement dans un contexte) Pour tout contexte E, si a_{1}/s_{1} ⊑ a_{2}/s_{2} alors E[a_{1}]/s_{1} ⊑ E[a_{2}]/s_{2}.

\underline{Preuve} : Par induction structurelle sur E. Soit A_{1} un environnement de typage et τ un type tel que A ⊢ C[a_{1}] : τ (1) et ⊢ s_{1} : A_{1}. Nous montrons qu’il existe une extension mémoire A_{2} de A_{1} telle que A_{2} ⊢ a_{2} : τ (2) and ⊢ s_{2} : A_{2}.

Cas a est [] a: Une dérivation de (1) se termine par :

(3) A_{1} ⊢ a_{1} : τ_{1} → τ (4) A_{1} ⊢ a : τ_{1} (App)

A_{1} ⊢ a_{1} a : τ Par hypothèse appliquée à (3), il existe une extension mémoire A_{2} de A_{1} telle que A_{2} ⊢ a_{2} : τ et ⊢ A_{2} : s_{2}. Par le lemme d’extension, appliqué à (3), nous avons A_{2} ⊢ a : τ d’où la conclusion par une règle App.

36 CHAPITRE 3. AJOUT DE CONSTRUCTIONS IMPÉRATIVES.

Cas a est v [] : Aussi simple que le précédent.

Bien que la preuve soit similaire à celle du chapitre précédent, il est important de noter qu’elle n’en découle pas. En particulier le cas où a est let x = E in a′ ne peut pas être montré. Heureusement, nous avons exclu ce contexte des contextes d’évaluation.

Lemme 8 (Contraction de radicaux) Si a_{1}/s_{1} ⟶_{ϵ} a_{2}/s_{2} alors a_{1}/s_{1} ⊑ a_{2}/s_{2}.

Chaque cas de radical peut être traité indépendamment, et, après avoir prouvé le lemme suivant, les preuves sont immédiates.

Lemme 9 (Remplacement dans un terme) Si les formules A ⊢ v : τ_{0} (1) et A ⊕ (x : ∀ ᾱ_{0}. τ_{0}) ⊢ a : τ (2) sont prouvables et si les variables liées de a ne sont pas libres dans v et les variables ᾱ_{0} ne sont pas libres dans A, alors A ⊢ a[v/x] : τ (3) est prouvable.

\underline{Preuve} : Puisqu’il ne s’agit ici que d’un résultat de typage, donc ne faisant pas intervenir la sémantique, on peut cette fois-ci réutiliser la preuve du chapitre précédent. Nous reposons cependant sur la remarque donnée dans la section précédente que le système de typage avec locations est équivalent à un système de typage sans locations. Nous utilisons également le fait que la restriction syntaxique (l’ensemble des programmes ML qui n’autorise que la liason à des valeurs) est stable par substitution par une valeur.

On pourrait également faire une preuve directe, similaire à celle du chapitre précédent, dans laquelle il faudrait ajouter le cas où a est ℓ et qui se traite comme le cas a est y (ce n’est pas une surprise, puisque dans la traduction présentée ci-dessus 3.3, page 33, les locations sont remplacées par des variables).

\underline{Preuve} : (de la contraction de radical) À nouveau, la démonstration copie celle du chapitre 1. Soit A_{1} un environnement de typage et τ un type tels que A_{1} ⊢ a_{1} : τ (1) et ⊢ s_{1} : A_{1}. Nous montrons qu’il existe une extension mémoire A_{2} de A_{1} telle que A_{2} ⊢ a_{2} : τ (2) et ⊢ s_{2} : A_{2} par cas sur le radical a_{1}. Chaque cas peut être vérifié indépendamment. Nous incorporons le cas des δ-règles.

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

\begin{aligned}(3) A_{1} ⊕ (x : τ_{1}) ⊢ a : τ \\ & (Fun) \\ A_{1} ⊢ a : τ_{1} → τ \end{aligned} (4) A_{1} ⊢ v : τ_{1} (App)

A_{1} ⊢ a_{1} : τ

Le lemme de remplacement appliqué à (4) et (3) montre la conclusion en choisissant A_{1} pour A_{2}.

Cas a_{1} est let x = v in a: Une dérivation de (1) se termine par :

(3) A_{1} ⊢ v : τ_{1} (4) A_{1}[x : Gen(τ_{1}, A)] ⊢ a : τ (Let)

A_{1} ⊢ let x = v in a : τ

Nous concluons en appliquant le lemme précédent (remplacement dans un terme) à (3) et (4) en choisissant A_{1} pour A_{2}. Les cas suivants correspondent à la vérification de l’hypothèse H1 sur les δ-règles.

3.4. CORRECTION DE LA SÉMANTIQUE 37

Cas a est ref v: Une dérivation de (1) se termine par :

A_{1} ⊢ v : τ_{1} (2) A_{1} ⊢ ref: τ_{1} → τ_{1} Ref

(App)

A_{1} ⊢ ref v : τ_{1} Ref

Nous choisissons A_{1} ⊕ (ℓ : τ_{1}) pour A_{2}. D’une part, A_{2} ⊢ ℓ : τ_{1}. D’autre part, notons s′ égal à s ⊕ ℓ : v. En utilisant (3), nous avons A_{1} ⊢ σ(ℓ′) : A_{2}(ℓ′) pour chaque ℓ′ du domaine de A_{2}. Par extension de contexte (lemme ??), nous pouvons remplacer l’hypothèse A_{1} par A_{2}, et donc conlure A_{2} ⊢ σ ⊕ ℓ : v.

Cas a est ℓ := v: Nécessairement τ est de la forme τ_{1} Ref, ℓ : τ_{1} est dans A_{1}, et A_{1} ⊢ v : τ_{1}. La conclusion est satisfaite, en choisissant A_{2} égal à A_{1}.

Cas a est !(ℓ) : Nécessairement ℓ : τ est dans A_{1}, donc A_{1} ⊢ s(ℓ) : τ. En prenant A_{1} pour A_{2}, nous avons bien A_{2} ⊢ s(ℓ) : τ et ⊢ s_{2} : A_{2}.

Le second théorème énonce que les termes bien typés qui ne peuvent être réduits sont des valeurs, en conséquence l’évaluation des termes bien typés n’est jamais bloquée. La preuve est une récurrence structurelle sur la valeur en utilisant le lemme suivant :

Lemme 10 Soit A une extension mémoire de A_{0} telle que A ⊢ v : τ.

• Si τ est un type fonctionnel alors a est une fonction ou une constante fonctionnelle partiellement appliquée.

• Si τ est τ_{1} Ref alors v est une location mémoire.

\underline{Preuve} : Nous montrons séparément que pour toute valeur v et une extension mémoire A de l’environnement initial A_{0} telle que A ⊢ v : τ ( ? ?),

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

• Si v est une location mémoire alors τ est τ_{1} Ref.

Chaque cas se vérifie facilement par analyse de la dérivation (1). Les sous-ensembles des types sont disjoints. Les sous-ensembles de valeur correspondantes forment une partition de l’ensemble des valeurs. On peut donc inverser les implications.

\underline{Preuve} : (des formes normales) La preuve est par récurrence structurelle sur a. Soit A une extension mémoire de l’environnement initial de typage telle que A ⊢ a : τ (1) pour un certain type τ et ⊢ s : A (2) pour un état mémoire s. Nous supposons que a/s ne peut pas être réduit.

Cas a est x: Puisque le domaine de A est réduit à des constantes et à des locations mémoire, ce cas n’est pas possible.

Cas a est a_{1} a_{2} : Une dérivation de (1) montre qu’il existe un type τ_{1} tel que A ⊢ a_{1} : τ_{1} → τ et A ⊢ a_{2} : τ_{1}. L’hypothèse de récurrence appliquée à a_{1}/s avec l’environnement A et le type τ_{1} → τ montre que a_{1} est une valeur v. Ce ne peut pas être une fonction, car sinon a pourrait être réduit. Puisqu’elle a un type fonctionnel, c’est donc une constante fonctionnelle partiellement appliquée. L’hypothèse de récurrence appliquée à (2) montre que a_{2} est une valeur. Nous raisonnons maintenant par cas sur la constante v:

Sous-cas v est ref : Alors a pourrait être réduite.

Sous-cas v est ! : Alors a_{1} est une valeur de type τ_{1} Ref dans A, donc une location ℓ. De (2), nous déduisons que ℓ est dans le domaine de s donc a est réductible.

Sous-cas v est ( := ) : Alors a est effectivement une valeur.

Sous-cas v est (v_{1} := ) : Alors v_{1} est une location mémoire ℓ liée dans s. Donc a est réductible.

Cas a est let x = v in a_{2} : Alors a est réductible.

Autres cas : Il ne reste donc plus que les cas où a est une constante, une fonction ou une location mémoire, c’est-à-dire une valeur.

Exercice 22 Faire la preuve de correction pour l’autre solution proposée, interdisant de généraliser toute variable ayant apparu sous un constructuer Ref.

Exercice 23 Peut-on proposer une solution combinée consistant à type let x = v in aina de façon polymorphe, et let x = a_{0} in a en interdisant de généraliser les variables qui apparaissent dans des expressions sous un type Ref ?

3.5 Les autres formalismes

Nous avons proposé deux solutions pour typer correctement les références qui consistent à restreindre soit l’ensemble des variables généralisables, soit l’ensemble des termes généralisables. Aucune n’est entièrement satisfaisante.

La première solution proposée est une extension conservative de ML, car si un programme n’utilise pas de référence, il est toujours possible de le typer en n’utilisant que des variables généralisables. Mais cette solution contraint beaucoup la construction des références, et par exemple, elle ne permet pas de typer la fonction fun (x) ref x qui illustre en fait un grand nombre de cas pratiques où il est souhaitable d’écrire une fonction polymorphe qui crée des références, mais de n’appliquer cette fonction ensuite que dans des cas monomorphes.

La seconde solution qui permet de traiter l’exemple ci-dessus, et la plupart des exemples utiles en pratique, n’est cependant pas une extension conservative de ML, c’est-à-dire qu’il existe des programmes n’utilisant pas les références qui étaient auparavant typables et qui ne le sont plus. Par exemple,

    let I = (fun x → x) (fun x → x) in I I;;

En effet, la définition de I fait intervenir une application et n’est donc pas généralisable donc le corps du programme I I n’est pas typable.

En pratique, la seconde solution est de loin la meilleure, même si elle restreint le polymorphisme de ML. Y a-t-il un meilleur compromis ?

Nous présentons ci-dessous une solution trop simple qui rejette trop de programmes, et deux solutions trop sophistiquées, qui permettent de typer à peu près tous les programmes souhaitables, mais qui utilisent une structure de type trop complexe pour permettre à l’utilisateur de les manipuler, et par exemple d’écrire les interfaces des modules.

Exercice 24 Montrer que l’on peut coder le point fixe Y avec des références, et sans utiliser l’opérateur de récursion, ni les types récursifs.

Les variables mutables

Une restriction très forte sur les constructions mutables consiste à ne pas les autoriser dans des fermetures. Les cellules mémoire ont alors une durée de vie connue statiquement, ce qui permet de les généraliser sans restriction. La contrepartie étant bien entendu que ces cellules mémoire sont moins expressives. La restriction peut être assurée en déréférençant automatiquement les variables à chaque utilisation et en interdisant aux variables de traverser les liaisons λ. Cette solution est trop restrictive pour être suffisante, mais elle pourrait être combinée avec une des solutions précédentes.

La syntaxe de ML serait alors étendue avec les constructions :

a ::= … | letvar ℓ = a_{1} in a_{2} | ℓ

et les règles de typage suivantes :

(Var)

\frac{A ⊢ a_{1} : τ_{1} A ⊕ (ℓ : τ_{1}) ⊢ a_{2} : τ_{2}}{A ⊢ letvar ℓ = a_{1} in a_{2} : τ_{2}}

(Loc) ; \frac{ℓ : τ ∈ A}{A ⊢ ℓ : τ}

Il convient de modifier en plus la règle d’abstraction pour interdire à une location mémoire d’être exportée dans une fermeture :

(Fun) ; \frac{Ā ⊕ (x : τ_{0}) ⊢ a : τ}{A ⊢ fun (x) a : τ_{0} → τ}

où Ā est l’environnement A privé de ses locations mémoire.

Les contextes d’évaluation sont simplement :

E ::= … | letvar ℓ = E in a

Il faut bien remarqué qu’ici, les locations ℓ ne sont plus considérées comme des valeurs. Par exemple, elles ne peuvent pas être mémorisées dans des structures de données. Les règles de réduction sont les suivantes :

(fun (x) a) v/s ⟶ a[v/x]/s  Fun
let x = v in a/s ⟶ a[v/x]/s  Let
If ℓ′ ∉ dom (s),  letvar ℓ = v in a/s ⟶ a[ℓ′/ℓ]/s ⊕ (ℓ′ : v)  Var
If ℓ ∈ dom (s),  ℓ/s ⟶ s(ℓ)/s  Deref
If ℓ ∈ dom (s),  ℓ := v ⟶ v/s ⊕ (ℓ : v)  Assign
If a_{1}/s_{1} ⟶_{ϵ} a_{2}/s_{2},  E[a_{1}]/s_{1} ⟶ E[a_{2}]/s_{2}  Contexte

Le sémantique ci-dessus ne reflète cependant pas la portée syntaxique des variables mutables. Pour donner une sémantique plus précise, nous introduisons les contextes d’évaluation

E ::= E a | v E | letvar ℓ = v in E_{ℓ}

où E_{ℓ} est un contexte E qui ne lie pas ℓ sur son chemin. On peut alors donner la sémantique plus élégante suivante :

(fun (x) a) v ⟶ a[v/x]  Fun
let x = v in a ⟶ a[v/x]  Let
letvar ℓ = v in v′ ⟶ v′  Var
letvar ℓ = v in E_{ℓ}[ℓ] ⟶ letvar ℓ = v in E_{ℓ}[v]  Deref
letvar ℓ = v in E_{ℓ}[ℓ := v′] ⟶ letvar ℓ = v′ in E_{ℓ}[v′]  Assign
If a_{1}/s_{1} ⟶_{ϵ} a_{2}/s_{2},  E[a_{1}]/s_{1} ⟶ E[a_{2}]/s_{2}  Contexte

En particulier la règle Var repose sur le fait qu’une valeur ne peut pas contenir de locations.

Exercice 25 Montrer la correction du typage vis à vis de la sémantique pour cette extension du noyau ML.

Les variables faibles de SML

Dans la solution que nous avons retenue, il est garanti que l’évaluation des expressions généralisables ne crée pas de références puisque ce sont des valeurs. Nous dirons qu’une expression est non expansive si son évaluation ne crée pas de référence. Il existe bien sûr de nombreux autres programmes non-expansifs que les valeurs. Par exemple on peut définir la classe suivante :

\begin{matrix}b ::= & v | let x = v in b | b_{0} \\ b_{0} ::= & (! ) | ( := ) | b_{0} b \end{matrix}

Il est important que ref ne soit pas dans la classe b_{0}, car en effet son application crée une référence.

Si b est une classe de programmes non-expansifs, on peut alors admettre la construction let x = b in a dans le langage et préserver la correction forte. Mais il est difficile d’identifier de façon purement syntaxique une sous-classe de programmes non-expansifs plus grande que b.

L’idée des variables faibles est d’utiliser un mécanisme associé au typage pour identifier une classe plus large de programmes non expansifs. Par exemple, la fonction ref est typée comme ∀ α^{0}. α^{0} → α^{0} où l’exposant signifie que son application à un argument risque de créer une référence de type α. La variable de type α^{0} est dite faible. On pourra se reporter à [?] pour une présentation détaillée, mais cette solution autrefois utilisée dans le langage Sml-nj a été abandonnée en raison de sa complexité.

3.5.1 Le typage des fermetures

La première solution que nous avons proposée interdit de généraliser les variables qui apparaissent dans le type d’une valeur qui est mise dans une référence. Cette interdiction est globale et ad-eternum, c’est-à-dire qu’une variable ayant servi pour communiquer avec une référence ne peut plus être généralisée, même lorsque les locations correspondantes ne peuvent plus être atteintes.

Le typage des fermetures tente d’éviter cette contamination, en calculant au moment de la généralisation quelles sont les variables de types qui peuvent apparaître dans le type d’une référence en n’examinant que le type à généraliser.

En effet, le type d’une valeur construite décrit entièrement la structure de cette valeur. Cette propriété n’est plus vraie en général pour les fonctionnelles car les fonctions peuvent cachée des valeurs dans leur fermetures, sans en révéler le type. Par exemple, dans le programme suivant, la fonction deux est une valeur qui contient dans sa fermeture la valeur un.

    let id x = x in let deux x = id (id x) in deux 0;;

L’approche consiste à typer les fonctions en montrant tous les types des valeurs qui sont libres dans leur corps, y compris le type des valeurs dans la fermeture. Ce mécanisme de typage est relativement complexe à mettre en œuvre. Se reporter à [?].

3.5.2 Les régions

Cette solution consiste à déterminer, par un mécanisme lié à la synthèse des types, des régions du programme qui ne peuvent pas communiquer entre elles. L’utilisation d’une référence dans une région sera alors sans influence sur le typage d’une région disjointe. Ce mécanisme de typage est également complexe à mettre en œuvre. Se reporter à [?].

Le typage des régions fournit aussi une information sur la connectivité du programme qui peut se révéler très utile pour la compilation. Par exemple cette méthode à été utiliser pour réaliser un compilateur de ML sans glanage de cellules, toutes les valeurs étant stockées dans la pile, dans des régions de taille variable, mais désallouées en bloc [?].

3.6 D’autres constructions impératives

Les exceptions

Par leur importance les exceptions sont sans aucun doute la seconde construction impérative dans les langages fonctionnels. Elle sont indispensables pour programmer proprement les cas pathologiques et ratrapper correctement les erreurs.

Pour ajouter les exceptions dans le langage, il nous faut d’abord introduire deux nouvelles constructions :

a ::= … | try a with x ⇒ a | Raise a

La sémantique des exceptions est plus facile à définir que celle des objets mutables, car elle peut se faire directement sur les programmes sans devoir ajouter une construction globale analogue à la mémoire. Les contextes d’évaluation sont :

E ::= … | try E with x ⇒ a | Raise E

Nous ajoutons simplement aux constructions de ML les règles de réduction suivantes :

                        try v with x ⇒ a ⟶^{ϵ} v
                try E′[Raise v] with x ⇒ a ⟶^{ϵ} let x = v in a

Dans la seconde règle, le contexte E′ est un contexte d’évaluation ne contenant pas de nœud (try with ⇒ ), c’est-à-dire défini par la grammaire suivante :

\begin{matrix}E′ ::= & [] \\ | & E′ a \\ | & v E′ \\ | & Raise E′ \end{matrix}

Informellement, La seconde règle exprime que si l’évaluation de a lève une exception avec la valeur v, alors l’évaluation continue au niveau de la garde la plus proche.

Le typage des exceptions pose un problème similaire à celui des références : si le type des exceptions pouvait être un schéma σ, alors une exception pourrait être levée avec une instance τ_{1} de σ et capturée avec une autre instance τ_{2}, ce qui conduirait à une erreur de typage si les deux instances τ_{1} et τ_{2} sont incompatibles. Le type des exceptions sera donc toujours monomorphe.

Privilégions un type τ_{0} sans variables libres. Les règles de typage pour les exceptions sont :

(Raise)

\frac{A ⊢ a : τ_{0}}{A ⊢ Raise a : α}

(Try)

\frac{A ⊢ a_{1} : τ A ⊕ x : τ_{0} ⊢ a_{2} : τ}{A ⊢ try a_{1} with x ⇒ a_{2} : τ}

Exercice 26 Montrer la correction de cette extension.

Exercice 27 (***) Peut-on coder le point fixe avec les exceptions ?

3.6.1 Les opérations de contrôle

Pour mémoire, se reporter à [?].

Conclusion

Le formalisme de la sémantique à réduction s’adapte assez simplement aux constructions impératives du langage. Bien plus difficile est de trouver la bonne façon de typer les constructions impératives. Ce problème a des rapports très étroits avec d’autres analyses fines des programmes, par exemple avec la compilation sûre d’un plus grand ensemble de valeurs récursives. Là il ne faut plus garantir qu’une fonction n’a pas encore été appliquée, mais, ce qui est très similaire, qu’elle n’a pas encore lu les composantes de son argument.

Le typage fin des constructions impératives est un problème difficile qui n’a pas encore trouvé de solution idéale ; mais la solution minimaliste de restreindre le polymorphisme aux valeurs ne semble pas trop pénalisante, pour un gaint considérable de simplifité. Finalement, c’est peut être la meilleure solution.

Pour en savoir plus

Dans [?], on pourra trouver un traitement local de la mémoire dans la sémantique à réduction à petits pas.

Solutions des exercices

Exercice 19, page 34

Si vous n’avez pas trouvé de contre-exemple, cherchez encore. Si vous avez répondu négativement à la dernière question, faites les deux exercices suivants et reposez vous la question. Si vous avez toujours une réponse négative, alors votre exemple est intéressant.

Exercice 20, page 34

On peut toujours écrire (fun (x) a_{2}) a_{1}. Donc il n’y a pas de problème à écrire let x = a_{1} in a_{2}, mais il faut le comprendre comme du sucre syntaxique pour l’expression ci-dessus, et donc typer cette expression sans généraliser.

Exercice 21, page 34

Par η-conversion, on peut remplacer g v par fun (y) g v y qui est une valeur et permet donc à g′ d’être polymorphe dans a. Si g est lui de la forme fun (z x) a_{0}, alors les deux programmes sont équivalents. Mais ce n’est plus nécessairement le cas si g est de la forme fun (z) a_{1} a_{2} : au mieux la sémantique sera la même (avec un calcul moins efficace), mais la sémantique peut aussi être différente si l’évaluation de a_{1} a_{2} modifie la mémoire.

Exercice 23, page 38

Non, les deux solutions reposent sur des invariants globaux incompatibles. Voici un contre-exemple :

    let isomorphe a ref x =
      let r = ref x in let ecrit y = r := y and lit () = !r in
      (ecrit, lit) in
    let poly ref = isomorphe a ref (fun x → x) in
      (fst poly ref) succ; (snd poly ref) true;;

La fonction isomorphe a ref crée une référence et rend les fonctions qui permettent d’écrire et de lire dans cette référence ; ceci en cache le type. Elle est polymorphe car c’est une valeur. Le reste du programme est polymorphe car le type REF n’y apparaît pas bien que des références y sont crées.

Exercice 24, page 39

Étant donné F, on veut trouver f égal à Y F tel que f x soit égal à F f x. Supposons que f soit dans le contenu d’une référence r. On a donc f x égal à F f x… qu’il suffit de mettre dans le contenu de la référence r avant de retourner f. Cela donne le programme :

    let Y F =
      let r = ref (fun → raise (Failure "Y")) in
      let f x = F !r in
      r := f; !f;;

On peut aussi utiliser le type option pour initialiser le contenu de la référence avec None puis le remplacer plus tard par None f.

Exercice 27, page 42

Oui, car les exceptions peuvent cacher des types récursifs. L’exercice 16 a montrer comment définir Y à partir de deux fonctions replier et deplier à partir d’un type récursif à occurence négative. On peut utiliser une exception :

    exception Masque of ((unit → unit) → (unit → unit));;

pour écrire les fonctions

    let replier = fun x → fun (y:unit) → (raise (Masque x); ())
    and deplier = fun x → try (x(): unit); fun x → x with Masque y → y;;

3.6. D’AUTRES CONSTRUCTIONS IMPÉRATIVES 45 Les fonctions replier et deplier sont des coercions inverses :

U

                              − deplier −^{}
                              − replier −

(U → U)

où U est égal à unit → unit. Elle peuvent donc servir a‘ emrober tout terme du lambda-calcul pour le rendre typable avec les types simples. Le codage est classique :

\begin{aligned}[[x]] & = x \\ [[fun (x) a]] & = replier(fun (x) [[a]]) \\ [[a_{1} a_{2}]] & = deplier([[a_{1}]] [[a_{2}]]) \end{aligned}

En particulier on peut écrire le combinateur [[Y]].