Teste dinâmico de down casts conforme explicado em TAPL

Question

Na página 195 do livro TAPL de Pierce, ele afirma que é possível substituir um operador down-cast por algum tipo de teste de tipo dinâmico.Então ele dá as seguintes regras:

Teste de tipo 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}$

E-Typetest1:

$\dfrac{\vdash v_1:T}{ ext{if } v_1 ext{ em } 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{ em } T ext{ then } x o t_2 ext{ else } t_3 o t_3}$

Não há mais explicações e não sei como interpretar essas regras.Revendo-as, percebo que a primeira é uma regra de digitação e a segunda e a terceira são regras de avaliação.No entanto, a sintaxe é um pouco estranha.Quais são as setas em cada ramo do if?Por que o if inclui o insintaxe?

Answer 1

A primeira regra T-Typetest é uma regra de verificação de tipo.Vamos ler juntos.Primeiramente, $\Gama$ não é importante (pelo menos numa primeira leitura).Temos as seguintes premissas:

1. $t_1$ tem tipo $S$
2. se $x$ tem tipo $T$ então $T_2$ tem tipo $U$
3. $t_3$ tem tipo $U$

A conclusão é que obtemos uma expressão do tipo $U$ (Acho que sua transcrição deveria ter "$:U$" em vez de $\para t_3$ a conclusão):$$\mathrm{se}\;t_1 \;\mathrm{in}\;T \;\mathrm{então}\;x o t_2 \;\mathrm{else}\;t_3 ag{1}$$O significado desta expressão pode ser entendido observando as outras duas regras, que são a semântica operacional de pequenos passos.Aqui está uma explicação incorreta, que corrigiremos em instantes:

1. Se $t_1$ tem tipo $T$ então (1) avalia como $t_2$ com $x$ substituído por $t_1$.É o caso do “downcast”, ou seja, $t_1$ está abatido de $S$ para $T$, o valor downcast está vinculado a $x$ e então $t_2$ É executado.

2. Se $t_2$ não tem tipo $T$ então (1) avalia como $t_3$.Este é o "padrão" que usamos quando o downcast não é possível.

A explicação acima está incorreta porque devemos usar $v_1$ em vez de $t_1$, pelo qual o autor está lhe dizendo:primeiro avalie $t_1$ para $v_1$, e, em seguida, execute o downcast.

Em uma linguagem OO imaginária, a mesma coisa pode ser escrita mais ou menos assim:

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