Return to 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}$

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?

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?

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 figure:

There is no further explanation and I'm unaware of how to interpret these rules. Why $\Gamma$ is missing from the second and third? Where does $x$ or $t_i$ come from? What does it mean $in$?...

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

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?