ch:gradual-typing: ch:gradual-typing

Rule C-UnkR gives $\mathbf{2}{\sim }_{\mathsf{c}}?$, and C-UnkL gives $?{\sim }_{\mathsf{c}}\mathbb{N}$. In a derivation of $\mathbf{2}{\sim }_{\mathsf{c}}\mathbb{N}$, the last rule cannot be an unknown rule because neither endpoint is $?$; it cannot be a base rule because the two base constructors differ; and it cannot be C-Arr. Hence no such derivation exists. An attempted proof of transitivity has no case combining C-UnkR with C-UnkL: their middle unknown supplies no equality between the two outside constructors.

For the inner application, $g:?$ matches $?\to ?$ and $0:\mathbb{N}$ is consistent with $?$. Thus $$g:?⊢(g0{)}^{{\ell }_1}:?,\cdot ⊢\lambda g:?.(g0{)}^{{\ell }_1}:?\to ?.$$ The argument has type $\mathbb{N}\to \mathbb{N}$, which is consistent with the outer domain $?$, so the complete term has type $?$ by G-App. Replacing $n:\mathbb{N}$ by $n:\mathbf{2}$ changes the argument type to $\mathbf{2}\to \mathbf{2}$ but does not reject the program: C-UnkR still gives $\mathbf{2}\to \mathbf{2}{\sim }_{\mathsf{c}}?$. That application-consistency premise is where the comparison is postponed.

The first elaboration is $$\cdot ⊢((\lambda x:?.x)0{)}^{{\ell }_1}⇝(⟨?\to ?\Leftarrow ?\to ?{⟩}^{{\ell }_{1,f}}(\lambda x:?.x))(⟨?\Leftarrow \mathbb{N}{⟩}^{{\ell }_{1,a}}0):?.$$ For the second term put $$u:=(⟨?\to ?\Leftarrow ?\to ?{⟩}^{{\ell }_{2,f}}(\lambda y:?.y))(⟨?\Leftarrow \mathbb{N}{⟩}^{{\ell }_{2,a}}0).$$ The inner instance of I-App gives $u:?$. The outer instance gives the complete target $$(⟨\mathbf{2}\to \mathbf{2}\Leftarrow \mathbf{2}\to \mathbf{2}{⟩}^{{\ell }_{3,f}}(\lambda x:\mathbf{2}.x))(⟨\mathbf{2}\Leftarrow ?{⟩}^{{\ell }_{3,a}}u):\mathbf{2}.$$ All four casts remain present; the two arrow identities are not optimized away.

Since $\mathsf{gnd}(\mathbb{N}\to \mathbb{N})=?\to ?$, E-Ground gives $$⟨?\Leftarrow \mathbb{N}\to \mathbb{N}{⟩}^{p}v⟼⟨?\Leftarrow ?\to ?{⟩}^p(⟨?\to ?\Leftarrow \mathbb{N}\to \mathbb{N}{⟩}^{p}v).$$ The outer term is an injection tagged $?\to ?$, and its payload is the displayed function wrapper. Both forms occur in the value grammar, so no further reduction is required to obtain a value.

Direct injection of every non-unknown $A$ would require the value clause $⟨?\Leftarrow A{⟩}^{p}v$ rather than the clause restricted to $G$. Projection would likewise compare arbitrary stored and demanded type expressions: $$⟨B\Leftarrow ?{⟩}^q(⟨?\Leftarrow A{⟩}^{p}v)$$ would return $v$ when $A=B$ and blame otherwise. Canonical forms at $?$ would then expose an arbitrary syntactic type tag $A$, not one of the three ground tags. In particular, the present proof that all dynamic functions carry the single tag $?\to ?$ would no longer apply; this mutation changes both the value invariant and the reduction table.

Inversion of the redex typing supplies $v:A_1\to B_1$, $w:A_2$, $A_1{\sim }_{\mathsf{c}}{A}_2$, and $B_1{\sim }_{\mathsf{c}}{B}_2$. The reduct has the tree Put $$u=v(⟨A_1\Leftarrow A_2{⟩}^{\overline{p}}w).$$ The two stages are $$\frac{\begin{array}{c}v:A_1\to B_1\\ {\displaystyle \frac{\begin{array}{c}w:A_2\\ A_2{\sim }_{\mathsf{c}}{A}_1\end{array}}{⟨A_1\Leftarrow A_2{⟩}^{\overline{p}}w:A_1}}\mathrm{T}-\mathrm{Cast}\end{array}}{u:B_1}\mathrm{T}-\mathrm{App}.$$ Then $$\frac{\begin{array}{c}u:B_1\\ B_1{\sim }_{\mathsf{c}}{B}_2\end{array}}{⟨B_2\Leftarrow B_1{⟩}^{p}u:B_2}\mathrm{T}-\mathrm{Cast}.$$ If the domain cast is reversed to $⟨A_2\Leftarrow A_1{⟩}^{\overline{p}}$, its operand would have to have type $A_1$, but the available premise is $w:A_2$. Thus the inner T-Cast instance, and consequently the application, cannot be formed.

For positive safety, P-Arr requires the opposite-polarity domain premise $?{⪯}^{-}\mathbb{N}$, which is N-Unk, and the codomain premise $\mathbb{N}{⪯}^{+}?$, which is P-Unk. Hence $\mathbb{N}\to \mathbb{N}{⪯}^{+}?\to ?$. For negative safety, N-Arr requires $\mathbb{N}{⪯}^{+}?$ in the domain and $?{⪯}^{-}\mathbb{N}$ in the codomain. The same two unknown rules give $?\to ?{⪯}^{-}\mathbb{N}\to \mathbb{N}$.

With the mutated wrapper rule, the first application in example 23.25 becomes $$⟨?\Leftarrow \mathbb{N}{⟩}^p(i(⟨\mathbb{N}\Leftarrow ?{⟩}^{p}d)).$$ The stored tag of $d$ is $\mathbf{2}$, so E-Mismatch produces ${\mathsf{blame}}_p$, which then propagates. The false line in the label-preservation proof is the wrapper case: inversion of $A_1\to B_1{⪯}^{+}{A}_2\to B_2$ supplies $A_2{⪯}^{-}{A}_1$ for a cast labeled $\overline{p}$. Relabelling that cast by $p$ would instead require the unsupported positive premise $A_2{⪯}^{+}{A}_1$.

Write the precise function type as $B\to C$ and its less precise type as $?$. Matching changes from $\mathsf{fun}(B\to C)=B\to C$ to $$\mathsf{fun}(?)=?\to ?.$$ The component precision goals are $B{⊑}_{\mathsf{ty}}?$ and $C{⊑}_{\mathsf{ty}}?$, both instances of Pr-Unk. If the precise argument has type $D$ with $D{\sim }_{\mathsf{c}}B$, its less precise mate has a type $D^{\prime }$ with $D{⊑}_{\mathsf{ty}}{D}^{\prime }$. The less precise application requires only $D^{\prime }{\sim }_{\mathsf{c}}?$, supplied by C-UnkR. Thus G-App gives result type $?$, and Pr-Unk relates $C$ to that result.

The lambda in $r^{\prime }$ has type $?\to ?$, matching returns the same arrow, and $\cdot ⊢\mathsf{true}:\mathbf{2}$ with $\mathbf{2}{\sim }_{\mathsf{c}}?$ by C-UnkR. Therefore G-App derives $\cdot ⊢r^{\prime }:?$.

A derivation for $r$ would type its lambda as $\mathbb{N}\to \mathbb{N}$ and matching would return $\mathbb{N}\to \mathbb{N}$. Inverting its final G-App would therefore require $\mathbf{2}{\sim }_{\mathsf{c}}\mathbb{N}$. Inversion of consistency rules shows that no rule has these two distinct base endpoints. Only the direction from a typed precise term to its less precise mate remains valid; typing $r^{\prime }$ cannot be used to infer typing of $r$.

The common inner call elaborates completely to $$u_C:=(⟨?\to ?\Leftarrow ?\to ?{⟩}^{{\ell }_{i,f}}(\lambda x:?.x))(⟨?\Leftarrow \mathbb{N}{⟩}^{{\ell }_{i,a}}0):?.$$ Keeping the two fresh labels at the outer source position, the two complete elaborations are Thus every one of the six inserted casts is shown: the common inner pair and the two outer pairs. Reducing the common subterm gives $u_C{⟼}^{\ast }z$, where $z=⟨?\Leftarrow \mathbb{N}{⟩}^{{\ell }_{i,a}}0$. The precise outer argument cast then gives $$⟨\mathbf{2}\Leftarrow ?{⟩}^{{\ell }_{o,a}}z⟼{\mathsf{blame}}_{{\ell }_{o,a}}.$$ The surrounding application propagates this blame, so $a{⟼}^{\ast }{\mathsf{blame}}_{{\ell }_{o,a}}:\mathbf{2}$. On the other side, the unknown identity casts and arrow wrapper all contract without changing the payload, so $a^{\prime }{⟼}^{\ast }z:?$. The final results are related by $$\frac{\begin{array}{c}\cdot {⊢}_{C}z:?\\ \mathbf{2}{⊑}_{\mathsf{ty}}?\end{array}}{\cdot ⊢{\mathsf{blame}}_{{\ell }_{o,a}}:\mathbf{2}{⊑}_{\mathsf{C}}z:?}\mathrm{CPr}-\mathrm{Blame}.$$ Thus equality of observations would fail, while error approximation holds.

By lemma 23.32, $i:\mathbb{N}\to \mathbb{N}{⊑}_{\mathsf{C}}i:\mathbb{N}\to \mathbb{N}$. Apply CPr-CastR using $\mathbb{N}\to \mathbb{N}{\sim }_{\mathsf{c}}?\to ?$ and $\mathbb{N}\to \mathbb{N}{⊑}_{\mathsf{ty}}?\to ?$ to obtain the required $i{⊑}_{\mathsf{C}}w$. For the argument, instantiate CPr-CastR with $S=U=\mathbb{N}$ and $V=?$: its term premise is reflexive numeral precision, while its remaining premises are $\mathbb{N}{\sim }_{\mathsf{c}}?$ and $\mathbb{N}{⊑}_{\mathsf{ty}}?$. Hence $0:\mathbb{N}{⊑}_{\mathsf{C}}z:?$.

The applications are related by CPr-App. Their right reduction is The left application $i0$ reduces to $0$. Reflexive numeral precision and CPr-CastR relate this $0:\mathbb{N}$ to the final injection at $?$.

Clause 1 begins with successful evaluation of the more precise program. Finite simulation and value catch-up cannot introduce left blame, so the less precise program must reach a related value. Clause 2 begins with success of the less precise program. The more precise program may contain a check removed on the right, so its permitted additional outcome is blame.

The false reverse clause would assert that right success always implies left success. In the displayed $e{⊑}_{\mathsf{src}}{e}^{\prime }$, the right elaboration returns the tagged natural $z$, while the left outer Boolean projection reaches ${\mathsf{blame}}_{{\ell }_{o,a}}$. Hence the blame alternative is necessary. In the actual proof, operational trichotomy also presents the possible case $a{⟼}^{\omega }$. Infinite simulation would then force $a^{\prime }{⟼}^{\omega }$, contradicting the assumed finite reduction of $a^{\prime }$ to a value. This is the exact step that replaces the false normalization claim.

Let $i=\lambda n:\mathbb{N}.n$ and $g=\lambda f:\mathbb{N}\to \mathbb{N}.(f0{)}^{{\ell }_i}$. The inner application in $g$ elaborates to $$(⟨\mathbb{N}\to \mathbb{N}\Leftarrow \mathbb{N}\to \mathbb{N}{⟩}^{{\ell }_{i,f}}f)(⟨\mathbb{N}\Leftarrow \mathbb{N}{⟩}^{{\ell }_{i,a}}0).$$ The complete outer elaboration is $$(⟨(\mathbb{N}\to \mathbb{N})\to \mathbb{N}\Leftarrow (\mathbb{N}\to \mathbb{N})\to \mathbb{N}{⟩}^{{\ell }_{o,f}}{g}_C)(⟨\mathbb{N}\to \mathbb{N}\Leftarrow \mathbb{N}\to \mathbb{N}{⟩}^{{\ell }_{o,a}}i),$$ where $g_C$ is $g$ with the displayed inner target body.

Each arrow identity is a wrapper. Applying the outer wrapper first inserts an identity arrow cast on its argument and an identity base cast on its result. Erasure removes all of these casts, so that step leaves the erased term $gi$ unchanged. The ensuing beta step erases to $(i0)$; applying the inner arrow wrapper and reducing its two base identity casts again leave that erasure unchanged; the inner beta step erases to $0$. Finally the surrounding result identity casts reduce to $0$ and erase to $0$ throughout. Thus the only non-stuttering erasure steps are $$gi⟼i0⟼0,$$ exactly the ordinary call-by-value reduction of the static source term.