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.

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.

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

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}.

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

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) ?

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.

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}.

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.

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.

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)

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) ?

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.

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}

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).

4.3 ∗ En déduire que si a_{1} ⟶ a_{2} alors [[a_{1}]]^{V} ⟶ [[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 ?

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 ?

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)

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).

5.5 Comment traiter le cas des exceptions multiples ?