Test dynamique des lancers vers le bas comme expliqué dans TAPL

Question

À la page 195 du livre TAPL de Pierce, il déclare que l'on peut remplacer un opérateur down-cast par une sorte de test de type dynamique.Puis il donne les règles suivantes :

Test de type T :

$\dfrac{\Gamma \vdash t_1:S \;\;\Gamma,x:T \vdash t_2:U \;\;\Gamma \vdash t_3:U}{\Gamma \vdash ext{if } t_1 ext{ in } T ext{ then } x o t_2 ext{ else } t_3 o t_3 :U}$

Test de type E1 :

$\dfrac{\vdash v_1:T}{ ext{if } v_1 ext{ in } T ext{ then } x o t_2 ext{ else } t_3 o [x \mapsto v_1]t_2}$

E-Typetest2 :

$\dfrac{ vdash v_1:T}{ ext{if } v_1 ext{ in } T ext{ then } x o t_2 ext{ else } t_3 o t_3}$

Il n'y a pas d'autre explication et je ne sais pas comment interpréter ces règles.En les examinant, je me rends compte que la première est une règle de frappe et que les deuxième et troisième sont des règles d'évaluation.Cependant, la syntaxe est un peu étrange.Quelles sont les flèches dans chaque branche du if ?Pourquoi le if inclut le insyntaxe?

Answer 1

La première règle T-Typetest est une règle de vérification de type.Lisons-le ensemble.Premièrement, $\Gamma$ n'est pas important (en première lecture du moins).Nous disposons des locaux suivants :

1. $t_1$ a du type $S$
2. si $x$ a du type $T$ alors $T_2$ a du type $U$
3. $t_3$ a du type $U$

La conclusion est que nous obtenons une expression de type $U$ (Je pense que votre transcription devrait avoir "$ :$EU" au lieu de $\à t_3$ la conclusion):$$\mathrm{if}\;t_1 \;\mathrm{in}\;T \;\mathrm{puis}\;x o t_2 \;\mathrm{else}\;t_3 ag{1}$$La signification de cette expression peut être comprise en examinant les deux autres règles, qui sont une sémantique opérationnelle à petits pas.Voici une explication incorrecte, que nous corrigerons dans un instant :

1. Si $t_1$ a du type $T$ alors (1) évalue à $t_2$ avec $x$ remplacé par $t_1$.C'est le cas du "downcast", c'est-à-dire $t_1$ est abattu de $S$ à $T$, la valeur diminuée est liée à $x$ et puis $t_2$ est exécuté.

2. Si $t_2$ n'a pas de type $T$ alors (1) évalue à $t_3$.C'est le "par défaut" que nous utilisons lorsque le downcast n'est pas possible.

L'explication ci-dessus est incorrecte car nous devrions utiliser $v_1$ au lieu de $t_1$, par lequel l'auteur vous dit :évaluer d'abord $t_1$ à $v_1$, puis effectuez le downcast.

Dans un langage OO imaginaire, la même chose pourrait s'écrire un peu comme ceci :

S t1 = ...;
...
if (t1 instanceof T) {
  T x = (T)t1;
  t2;
} else {
  t3;
}