# Dynamic testing of down casts as explained in TAPL

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?

• Do not post pictures of formulas because they cannot be edited or searched. I can answer the question, but will wait until you change the image to proper formulas. Dec 28 '19 at 18:15
• @AndrejBauer I wrote out the formulas. I would appreciate essentially and explanation on what is the meaning of the rules... Dec 29 '19 at 11:41
• Thanks. Did you make a mistake in the conclusion of the first rule? Should it not end with "$: U$"? Dec 30 '19 at 9:17

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