Dynamic testing of down casts as explained in TAPL

Question

On page 195 of Pierce's TAPL book, he states that one can replace a down-cast operator by some sort of dynamic type test. Then he gives the following rules:

T-Typetest:

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

E-Typetest1:

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

E-Typetest2:

$\dfrac{\nvdash v_1:T}{\text{if } v_1 \text{ in } T \text{ then } x \to t_2 \text{ else } t_3 \to t_3}$

There is no further explanation and I'm unaware of how to interpret these rules. Reviewing them, I realize that the first is a typing rule and the second and third are evaluation rules. However, the syntax is a bit strange. What are the arrows in each branch of the if? Why the if includes the insyntax?

Answer 1

The first rule T-Typetest is a type-checking rule. Let's read it together. Firstly, $\Gamma$ is not important (on a first reading at least). We have the following premises:

1. $t_1$ has type $S$
2. if $x$ has type $T$ then $T_2$ has type $U$
3. $t_3$ has type $U$

The conclusions is, that we get an expression of type $U$ (I think your transcription should have "$: U$" instead of $\to t_3$ the conclusion): $$\mathrm{if}\; t_1 \;\mathrm{in}\; T \;\mathrm{then}\; x \to t_2 \;\mathrm{else}\; t_3 \tag{1}$$ The meaning of this expression can be undrstood by looking at the other two rules, which are small-step operational semantics. Here is an incorrect explanation, which we will make correct in a moment:

1. If $t_1$ has type $T$ then (1) evaluates to $t_2$ with $x$ replaced by $t_1$. This is the case of "downcast", i.e., $t_1$ is downcast from $S$ to $T$, the downcast value is bound to $x$ and then $t_2$ is executed.

2. If $t_2$ does not have type $T$ then (1) evaluates to $t_3$. This is the "default" which we use when the downcast is not possible.

The above explanation is incorrect because we should use $v_1$ instead of $t_1$, by which the author is telling you: first evaluate $t_1$ to $v_1$, and then perform the downcast.

In an imaginary OO language the same thing might be written somewhat like this:

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