1
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Dec 28 '19 at 18:15
  • $\begingroup$ @AndrejBauer I wrote out the formulas. I would appreciate essentially and explanation on what is the meaning of the rules... $\endgroup$ – Rodrigo Dec 29 '19 at 11:41
  • $\begingroup$ Thanks. Did you make a mistake in the conclusion of the first rule? Should it not end with "$: U$"? $\endgroup$ – Andrej Bauer Dec 30 '19 at 9:17
1
$\begingroup$

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;
}
| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.