Examen du DEA d’informatique Sémantique et programmation

Typage et Programmation

10 décembre 1997

Durée 2h30

Exceptions et types concrets

Les parties 1, 2 et 3 sont indépendantes. La partie 4 ne dépend que de la partie 1. On pourra admette les résultats des parties 1, 2, 3 et 4 dans la partie 5. Il y a des questions faciles dans chacune des parties, et la plupart des réponses sont courtes. Les questions plus longues ou plus difficiles sont marquées par ∗.

1 Exceptions On considère un langage L qui étend le noyau ML avec une seule sorte d’exception.

a ::= x | a a | v | let x = v in a | raise a | try a with v v ::= λx.a

Les contextes d’évaluations sont définis par :

E ::= {} | E a | v E | raise E | try E with v  Contextes d’évaluation
E′ ::= {} | E′ a | v E′ | raise E′  Contextes applicatifs

La réduction étend celle de ML avec les règles suivantes

try v_{0} with v ⟶ v_{0} (Success) try E′{raise v_{0}} with v ⟶ v v_{0} (Jump)

1.1 Montrer sur un exemple que remplacer E′ par E ne donnerait pas la sémantique attendue.

Réponse On pourrait alors “sauter” au dessus d’une construction “try”. On aurait par exemple

                       tryraise v_{1} with v_{2} ⟶ raise v_{1}

puisque try {} with v_{2} serait un contexte d’évaluation correct.

On suppose donné un type τ_{0} sans variable. On donne les deux nouvelles règles de typage :

\frac{A ⊢ a : τ_{0}}{A ⊢ raise a : τ} (Raise)  \frac{A ⊢ a : τ  A ⊢ v : τ_{0} → τ}{A ⊢ try a with v : τ} (Try)

1.2 Donner un exemple de programme bien typé qui n’est pas une valeur.

Réponse raise v (comme l’énoncé ne précisait pas explicitement irréductible, (λx.x)(λx.x) est aussi une réponse correcte).

1.3 Quelle est la forme des programmes bien typés irréductibles.

Réponse Les programmes bien typés irréductibles sont des valeurs ou des exceptions non rattrappées, i.e. de la forme E′{raise v}.

1.4 On note ⟶^{X} la relation ⟶ étendue avec les règles suivantes :

               raise (raise v) ⟶ raise v  (Raise)

(raise v) a ⟶ raise v  (Left)
v (raise v′) ⟶ raise v′  (Right)

Vérifier que si E′_{1}{raise v} ⟶^{X} a, alors a est de la forme E′_{2}{raise v}.

Réponse Considérons d’abord les réductions en tête. Il ne peut pas s’agir d’une règle β car raise v n’est pas une valeur. Il ne peut pas s’agir d’une règle Jump car E′_{1} ne peut pas être de la forme try E_{2}{v_{0}} with v. Chacune des règles Raise, left et Right s’applique, et le réduit est toujours raise v. Il suffit donc de prendre {} pour E′_{2}.

Sinon, il s’agit d’une réduction de la forme E′_{2}{a_{1}} ⟶ E′_{2}{a_{2}} où a_{1} ⟶ a_{2} est une réduction en tête. Comme nous l’avons vu ci-dessus a_{1} se réduit forcément sur raise v. Donc E′_{2}{a_{1}}, i.e. E′_{1}{raise v} se réduit sur E′_{2}{raise v}.

1.5 En déduire que si a ⟶^{X}_{∗} v alors a ⟶_{∗} v.

Réponse Un nouveau rédex a_{1} ⟶^{X} a_{2} ne peut s’opérer que dans un contexte de la forme E{try E′_{1}{raise v_{0}} with v} et être suivi de réductions de la forme suivante

E{try E′_{1}{raise v_{0}} with v} ⟶^{X} E{try E′_{2}{raise v_{0}} with v} ⟶^{X} …

E{try E′_{n}{raise v_{0}} with v} ⟶ E{v v_{0}}

On aurait donc pu directement dériver

E{try E′_{1}{raise v_{0}} with v} ⟶ E{v v_{0}}

1.6 ∗ En présence des règles Raise, Left, Right, peut-on remplacer la règle Jump par la règle plus faible

tryraise v_{0} with v ⟶ v v_{0}  (Failure)

sans changer l’ensemble des résultats possibles (justifier) ?

Réponse Considérons une application de la règle

try E′_{1}{raise v} with v ⟶ v v_{0}  (Jump)

Privons nous de la règle Jump. La suite de réductions “interne”

E′_{1}{raise v_{0}} ⟶ E′_{2}{raise v_{0}} ⟶ … E′_{n}{raise v_{n}} …

termine, car la taille de E′_{k+1} est toujours inférieure à celle de E′_{k}. Or, la seule façon de terminer est que le contexte E′ soit vide. On a donc E′{raise v} ⟶_{∗} raise v et on peut en déduire

try E′_{1}{raise v} with v ⟶ v v_{0}  (Failure)

Dans la suite on prendra pour sémantique des exceptions, les règles Raise, Left, Right et Failure au lieu de la règle Jump,

2 Types concrets On considère maintenant un autre langage L′ qui étend le noyau ML avec un type concret à deux constructeurs qui pourrait être défini en ML par la déclaration type ⟨α_{1} | α_{2}⟩ = Valof α_{1} | Excof α_{2}. Les expressions de L′ sont

a ::= x | v | a a | let x = v in a | Val a | Exc a | nil

            | match a withVal x → a else v | match a withExc x → a else v

v ::= λx.a | Val v | Exc v | nil

Il y a 4 nouvelles règles de réductions sont

matchVal v_{0} withVal x → a else v ⟶ a{v_{0}/x}  (Val-Val)

        matchExc v_{0} withVal x → a else v ⟶ v (Exc v_{0})  (Exc-Val)

et les 2 règles symétriques Exc-Exc et Val-Exc.

2.1 Décrire l’ensemble des contextes d’évaluation.

Réponse

          E ::= {} | E a | v E | Val E | Exc E | match E withVal→ a else v
              | match E withExc→ a else v

La constante nil ne peut jamais être réduite. Elle est utilisée pour “fermer” la construction match. L’expression ML match a_{0} withVal x_{1} → a_{1} | Exc x_{2} → a_{2} peut se voir comme une abréviation pour

       match a_{0} withVal x_{1} → a_{1} else λz.(match z withExc x_{2} → a_{2} elsenil)

On prendra pour expressions de types τ ::= α | τ → τ | ⟨τ | τ⟩ et on donne les règles de typage suivantes :

\frac{A ⊢ a : τ_{1}}{A ⊢ Val a : ⟨τ_{1} | τ_{2}⟩} (Val) \frac{A ⊢ a : τ_{2}}{A ⊢ Exc a : ⟨τ_{1} | τ_{2}⟩} (Exc)

2.2 Donner la règle de typage de la construction match a_{0} withVal x_{1} → a_{1} | Exc x_{2} → a_{2}. Réponse

(Match)

\frac{A ⊢ a_{0} : ⟨τ_{1} | τ_{2}⟩ A, x_{1} : τ_{1} ⊢ a_{1} : τ A, x_{2} : τ_{2} ⊢ a_{2} : τ}{A ⊢ match a_{0} withVal x → a | Exc x_{2} → a_{2} : τ}

2.3 À quelle expression ML correspond l’expression match a_{0} withVal x → a else nil ? Comment cette expression est-elle typée en ML. Quel problème pose son évaluation ? En déduire que l’on ne peut pas simultanément typer match a_{0} withVal x → a else v et nil tout en préservant la correction de l’évaluation.

Réponse L’expression ML correspondante est match a_{0} withVal x → a ou encore letVal x = a_{0} in a. Sa règle de typage est

\frac{A ⊢ a_{0} : ⟨τ_{1} | τ_{2}⟩ A, x : τ_{1} ⊢ a : τ}{A ⊢ match a_{0} withVal x → a : τ}

Son évaluation peut se bloquer (ou lancer une exception “Match failure”). Si l’on pouvait typer simultanément match a_{0} withVal x → a else v et nil, alors nil un type de la forme ⟨τ_{1} | τ_{2}⟩ → τ. Mais alors on pourrait appliquer nil à une valeur de type τ, expression dont l’évaluation est bloquée (il n’y a pas de règle pour réduire nil).

3 Typage avec des variantes polymorphes On reprend le typage mais

en considérant le type concret comme une variante polymorphe. :

τ ::= α | τ → τ | ⟨ρ | ρ⟩ ρ ::= α | Pre τ | Abs

3.1 Proposer de nouvelles règles de typage pour les expressions Val a, Exc a et match

a withVal x → a else v.

Réponse

(Val)

\frac{A ⊢ a : τ_{1}}{A ⊢ Val a : ⟨Pre τ_{1} | τ_{2}⟩}

(Exc)

\frac{A ⊢ a : τ_{2}}{A ⊢ Val a : ⟨τ_{1} | Pre τ_{2}⟩}

(Match)

\frac{\begin{matrix}A ⊢ a_{0} : ⟨Pre τ_{1} | τ_{2}⟩ \\ A, x : τ_{1} ⊢ a : τ A ⊢ v : ⟨τ′ | τ_{2}⟩ → τ \end{matrix}}{A ⊢ match a_{0} withVal x → a else v : τ}

3.2 On donne le type ∀ α. ⟨Abs | Abs⟩ → α à nil. Que faut-il vérifier pour que la correction soit préservée ? (énoncer la propriété sans la démontrer)

Réponse Il faut qu’il n’existe pas de valeur v de type ⟨Abs | Abs⟩.

3.3 Vérifier que l’expression a égale à match (λx.Val x) (λy.y) withVal z → z else nil est bien typée. En admettant la correction du typage vis à vis de l’évaluation, que peut-on en déduire sur le programme (λx.Val x) (λy.y) ?

Réponse On a la dérivation

\frac{⊢ (λx.Val x) (λy.y) : ⟨Pre (α → α) | Abs⟩ z : (α → α) ⊢ z : (α → α)}{match (λx.Val x) (λy.y) withVal z → z elsenil: α → α}

L’expression a ne peut pas s’évaluer sur Exc v, sinon l’évaluation de a serait bloquée, ce qui ne peut arriver que si a est mal typé.

3.4 Montrer que si v est de type ⟨τ | Abs⟩ alors v n’est pas de la forme Exc v. Retrouver le résultat précédent sur a uniquement à partir du typage de a. Généraliser.

Réponse Une dérivation de typage de Exc v ne peut que se terminer par la règle Exc. Elle ne peut donc dériver qu’un type de la forme ⟨τ_{1} | Pre τ_{2}⟩ qui est incompatible avec un type de la forme ⟨τ | Abs⟩.

L’expression a a pour type ⟨Pre (α → α) | Abs⟩ donc son évaluation sur une valeur a le même type et ne peut pas être de la forme Exc v. Cela se généralise à toute expression a telle que ⊢ a : ⟨τ_{1} | Abs⟩.

4 Simulation des exceptions avec des types concrets On définit la

traduction suivante des expressions de L en expressions de L′ (typo \underline{x} corrigée) :

[[let x = v in a]] = match [[v]] withVal y → let x = y in [[a]] else λz.z

[[a_{1} a_{2}]] =

           match [[a_{1}]] with

                 Val x → (match [[a_{2}]] withVal y → x y else λz.z)

               else λz.z

[[try a_{1} with v]] = match [[a_{1}]] withExc x → [[v]] \underline{x} else λz.z

       [[raise a]] = match [[a]] withVal x → Exc x else λz.z

[[λx.a]] = Val (λx.[[a]]) [[x]] = Val x

4.1 Montrer que si [[a_{1}]] ⟶ Val v_{1} et [[a_{2}]] ⟶ Val v_{2} alors [[a_{1} a_{2}]] ⟶ v_{1} v_{2}

Réponse Par définition, [[a_{1} a_{2}]] vaut match [[a_{1}]] withVal→ a else λz.z où a vaut λx.(match [[a_{1}]] withVal→ λy. x else λz.z). Le tout se réduit en match v_{1} withVal→ a else λz.z, puis a v_{1}, et sucessivement (match [[a_{2}]] withVal→ λy.v_{1} y else λz.z), puis (match v_{2} with Val→ λy.v_{1} y else λz.z) et finalement (λy.v_{1} y)v_{2}, puis v_{1} v_{2}.

On considère la relation de réduction formée par l’application de la règle Val-Val dans un contexte d’évaluation E quelconque. Remarquer que cette réduction termine. On note a^{V} la forme normale de a par ⟶^{V}.

On étend la traduction aux contextes en ajoutant [[{}]] = {}. On remarquera que [[E]]^{V} est un contexte d’évaluation ([[E]] n’en est pas nécessairement un). D’autre part [[E{a}]]^{V} est égal à [[E]]^{V} {[[a]]^{V} }.

4.2 ∗ On admet que si a_{1} ⟶ a_{2} est un β-rédex dans L, alors [[a_{1}]]^{V} ⟶ [[a_{2}]]^{V} dans L′. Vérifier la propriété pour les autres rédex de L (i.e. Raise, Left, Right et Failure).

Réponse Une valeur v dans L est une fonction λx.a. On note ⟨⟨v⟩⟩ pour λx.[[a]]. On a donc [[v]] égal à Val ⟨⟨v⟩⟩.

Cas raise (raise v) ⟶ raise v: [[raise v]]^{V} vaut Exc ⟨⟨v⟩⟩. [[a_{1}]] vaut match Exc ⟨⟨v⟩⟩ withVal→ λx.Exc x else λz.z et se réduit en Exc ⟨⟨v⟩⟩.

Cas (raise v) a ⟶ raise v: [[a_{1}]]^{V} vaut matchExc ⟨⟨v⟩⟩ withVal→ λx.[[a]] else λz.z et se réduit sur Exc ⟨⟨v⟩⟩.

Cas v_{0}(raise v) ⟶ raise v: [[a_{1}]]^{V} vaut match Exc ⟨⟨v⟩⟩ withVal→ λy.v_{0} y else λz.z et se réduit sur [[a_{1}]]^{V}.

Cas try raise v_{0} with v ⟶ v v_{0} : [[a_{1}]]^{V} vaut match Exc ⟨⟨v⟩⟩_{0} withExc y → [[v]] \underline{y} else λz.z et se réduit sur ⟨⟨v⟩⟩ ⟨⟨v⟩⟩_{0} (on trouverait [[v]] si on l’on n’avait pas ajouté \underline{y}), qui est aussi égal à [[v v_{0}]].

4.3 ∗ En déduire que si a_{1} ⟶ a_{2} alors [[a_{1}]]^{V} ⟶ [[a_{2}]]^{V}.

Réponse Comme [[E{a}]] est égal à [[E]]{[[a]]} et [[E]] est un contexte d’évaluation, à une réduction dans L de la forme E{a_{1}} ⟶ E{a_{2}}, correspond une évaluation

[[E]]^{V} {[[a_{1}]]^{V} } ⟶ [[E]]^{V} {[[a_{2}]]^{V} } i.e. [[E{a_{1}}]]^{V} ⟶ [[E{a_{2}}]]^{V}

5 Typage des exceptions

5.1 On considère le programme a égal à tryraise v_{0} with λz.z. En supposant que v_{0} est une valeur de type τ_{0}, quel est le type de [[a]] (on ne demande pas la dérivation) ? En déduire que le programme a ne se bloque pas sur une exception.

Plus généralement, quelle condition sur le type de [[a]] pour que a ne se bloque pas sur une exception ?

Réponse [[a]] a le type ⟨Val τ_{0} | τ⟩ pour tout type τ, en particulier pour τ égal à Abs ; [[a]] ne peut donc pas s’évaluer vers une valeur de la forme Exc. Par conséquent, le programme a ne bloque pas sur une exception, sinon il on aurait a ⟶ raise v et donc [[a]]^{V} ⟶ Exc ⟨⟨v⟩⟩.

De façon générale, si [[a]] a un type de la forme ⟨τ | Abs⟩, alors a ne peut pas se bloquer sur une exception.

5.2 Vérifier que la fonction λx.raise x ne soulève pas d’exception. Quel est son type ?

Vérifier que son utilisation peut soulever une exception. Comment peut-on lire cette information sur son type ?

Réponse L’expression [[λx.raise x]] vau Val (λx.[[raise x]]) c’est donc une valeur. Son type est ⟨α → ⟨α′ | Pre α⟩ | α′′⟩.

Appliquée à une expression v elle produit une exception. Cela se voit parce que le type du résultat de cette application est ⟨α′ | Pre α⟩ et n’est donc pas de la forme ⟨τ′ | Abs⟩.

5.3 Montrer que si l’on retire la primitive nil, on peut se restreindre à des types de la forme ⟨Pre τ_{1} | τ_{2}⟩ (i.e. ré-écrire les nouvelles règles de typage Val, Exc et Match) Réponse

(Val)

\frac{A ⊢ a : τ_{1}}{A ⊢ Val a : ⟨Pre τ_{1} | τ_{2}⟩}

(Exc)

\frac{A ⊢ a : τ_{2}}{A ⊢ Val a : ⟨Pre τ_{1} | Pre τ_{2}⟩}

(Match)

\frac{\begin{matrix}A ⊢ a_{0} : ⟨Pre τ_{1} | τ_{2}⟩ \\ A, x : τ_{1} ⊢ a : τ A ⊢ v : ⟨Pre τ′ | τ_{2}⟩ → τ \end{matrix}}{A ⊢ match a_{0} withVal x → a else v : τ}

On voudrait maintenant un système de typage primitif sur le langage L permettant de détecter les exceptions qui peuvent s’échapper. On se propose d’écrire des jugements de la forme A ⊢ a : τ, ρ où τ est le type ordinaire, et ρ indique si une exception peut être soulevée ou pas. On écrira τ \underrightarrow{ρ} τ au lieu de τ → ⟨Pre τ | ρ⟩.

5.4 En maintenant l’équivalence entre A ⊢ a : τ, ρ et A ⊢ [[a]] : ⟨Pre τ | ρ⟩, proposer de nouvelles règles de typage pour le jugement A ⊢ a : τ, ρ dans L (on ommetra la règle Let).

Réponse

\frac{x : τ ∈ A}{A ⊢ x : τ, ρ}  \frac{A ⊢ a_{1} : τ_{2} \underrightarrow{ρ} τ_{1}, ρ A ⊢ a_{2} : τ_{2}, ρ}{A ⊢ a_{1} a_{2} : τ_{1}, ρ}  \frac{A, x : τ_{1} ⊢ a : τ_{2}, ρ}{A ⊢ a : τ_{1} \underrightarrow{ρ} τ_{2}}

\frac{A, x : σ ⊢ a : τ, ρ}{A ⊢ a : τ_{1} \underrightarrow{ρ} τ_{2}}  \frac{A ⊢ a : τ, Pre τ}{A ⊢ raise a : τ′, Pre τ}  \frac{A ⊢ a : τ, Pre τ′ A ⊢ v : τ′ \underrightarrow{ρ} τ}{A ⊢ try a with v : τ, ρ}

5.5 Comment traiter le cas des exceptions multiples ?

Réponse Les exceptions multiples sont équivalentes à une exception simple dont la valeur est un type somme. On pourra en particulier choisir un type variante, comme nous l’avons fait dans le langage L′. L’extension ne pose donc pas de problème.