Gradual Typing and the Dynamic Boundary

Proof. Induct on $A$. The base cases are C-Bool and C-Nat; at $?$ use either unknown rule. If $A=A_1\to A_2$, apply the two induction hypotheses to C-Arr. ◻

Proof. Induct on the displayed consistency derivation. The cases C-UnkL and C-UnkR exchange rules. The Boolean and natural cases reproduce the same rule. In C-Arr, apply the two induction hypotheses and rebuild C-Arr. These are all consistency rules. ◻

Proof. Induct on the syntax of $e$. Constants and variables have the unique types shown in their rules. A lambda’s domain is written in the term, and the induction hypothesis fixes its codomain. For an application, the induction hypothesis fixes the type $C$ of the function position. The partial function $\mathsf{fun}$ has at most one result, so its codomain $B$ is fixed. The consistency premise checks the argument but does not choose the result. ◻

Proof. Use proposition 23.4 and induct on that source typing derivation. The first four cases are homomorphic. The application premises include $$\mathsf{fun}(C)=A_0\to B\text{and}D{\sim }_{\mathsf{c}}{A}_0.$$ Lemma 23.2 gives $C{\sim }_{\mathsf{c}}{A}_0\to B$: it is equality when $C$ is an arrow, and follows from C-UnkL when $C=?$. Hence T-Cast types the function cast at $A_0\to B$ and the argument cast at $A_0$; target application yields $B$. All choices were fixed by the source derivation and the fresh-label convention. ◻

Proof. Induct on the typing derivation of $a$. Variable and binder cases use the usual capture-avoiding renaming. In the cast case, apply the induction hypothesis to the operand and retain the same consistency premise and label. Blame contains no variables. The application case uses the two induction hypotheses and reconstructs the exact target application rule. ◻

Proof. Inspect the value grammar and invert its typing. A Boolean or numeral has its declared base type. A lambda has an arrow type. A wrapper is typed at its target arrow, and an injection is typed at $?$. No other value form exists. ◻

Proof. Analyze $A$ and $B$. If both are the same base type, use E-IdBase; if both are $?$, use E-IdUnk. If $A$ and $B$ are arrows, the term is a wrapper value. If $B=?$ and $A$ is ground, it is an injection value; if $A$ is a non-ground arrow, use E-Ground. It remains that $A=?$ and $B\ne ?$. If $B$ is non-ground, use E-Expand. If $B=G_2$ is ground, canonical forms writes $v=⟨?\Leftarrow G_1{⟩}^{q}w$. Exactly one of $G_1=G_2$ and $G_1\ne G_2$ holds, so exactly one of E-Project and E-Mismatch applies. Consistency excludes all remaining base–base and base–arrow pairs. ◻

Proof. Induct through the evaluation context and then inspect the contracted redex. Rule E-Beta is lemma 23.11. Identity and matching projection remove casts whose operand already has the target type. For E-Mismatch, rule T-Blame assigns the surrounding result type.

For E-Ground, consistency gives $A{\sim }_{\mathsf{c}}\mathsf{gnd}(A)$ and $\mathsf{gnd}(A){\sim }_{\mathsf{c}}?$. Two applications of T-Cast therefore yield the target type $?$. The dual argument handles E-Expand.

For the load-bearing wrapper case, inversion gives $$v:A_1\to B_1,w:A_2,A_1{\sim }_{\mathsf{c}}{A}_2,B_1{\sim }_{\mathsf{c}}{B}_2.$$ The domain cast labeled $\overline{p}$ has type $A_1$, so $v(⟨A_1\Leftarrow A_2{⟩}^{\overline{p}}w):B_1$. The cast is well formed because lemma 23.3 changes $A_1{\sim }_{\mathsf{c}}{A}_2$ into $A_2{\sim }_{\mathsf{c}}{A}_1$. The result cast labeled $p$ then has type $B_2$, the type of the original application. Context closure replaces a subterm by another of the same type. Blame propagation is typed by T-Blame at the context’s result type. ◻

Proof. Induct on the target typing derivation. Constants and lambdas are values; blame is the second alternative. In an application, first use the induction hypotheses in left-to-right order. If either subterm is blame, E-Blame applies. When both are values, lemma 23.12(3) writes the function as a lambda or wrapper, so E-Beta or E-WrapApp applies. In a cast, first progress its operand; when the operand is a value, apply lemma 23.13. For uniqueness, an application with a nonvalue operator has only the $[]a$ frame; once the operator is a value, a nonvalue argument has only the $v[]$ frame; once both are values, canonical forms selects exactly one of E-Beta and E-WrapApp. A cast with a nonvalue operand has only its cast frame; at a value operand, lemma 23.13 selects one root, using the decidable equality test for two ground tags. Finally E-Blame crosses the unique surrounding frame. Thus no term has two successors. ◻

Proof. By proposition 23.9, the elaborated target has type $A$. Apply preservation along the finite reduction and then theorem 23.15 to its endpoint. The three alternatives there are exactly a value, labeled blame, or a unique next step, so no fourth stuck form is possible. ◻

Proof. Use a structural checker for every rule except N-GroundUnk. For a negative goal ending in $?$, try the finite set $G\in \{\mathbf{2},\mathbb{N},?\to ?\}$ and then call the structural checker with N-GroundUnk disabled. Every auxiliary call recurses on a proper type component. Termination is lexicographic: the exceptional call changes the phase from ground selection to structural checking, and every call within the structural phase decreases total type size. The rule list is syntax directed in that phase, while the finite ground trial enumerates every possible last use of N-GroundUnk; hence the checker is sound and complete. ◻

Proof. Proceed simultaneously by induction on $A$. The base cases are P-Bool, N-Bool, P-Nat, and N-Nat. At $?$ use P-Unk and N-Unk. For $A=A_1\to A_2$, apply P-Arr to the negative induction hypothesis on $A_1$ and the positive hypothesis on $A_2$; apply N-Arr to the positive hypothesis on $A_1$ and the negative hypothesis on $A_2$. ◻

Proof. If $A$ is a base type, then $\mathsf{gnd}(A)=A$. Clauses 1 and 3 are therefore polar reflexivity followed or preceded by P-Unk or N-Unk. Clause 2 assumes that $A$ is not ground, so it has no base case.

Let $A=A_1\to A_2$. Then $\mathsf{gnd}(A)=?\to ?$. For clause 1, P-Arr uses $$?{⪯}^{-}{A}_1,A_2{⪯}^{+}?,$$ from N-Unk and P-Unk; another P-Unk relates the ground arrow to $?$. For clause 2, inversion of N-GroundUnk gives $A{⪯}^{-}G$. Arrow inversion and groundness force $G=?\to ?=\mathsf{gnd}(A)$; polar reflexivity and N-GroundUnk give the second judgment. For clause 3, N-Unk gives $?{⪯}^{-}\mathsf{gnd}(A)$, and N-Arr uses $A_1{⪯}^{+}?$ and $?{⪯}^{-}{A}_2$ for the remaining judgment. ◻

Proof. Beta reduction may duplicate existing casts, but it does not change their endpoints or labels. The other noncast reductions retain or discard existing labels. The ground and expansion cases use the applicable clause of lemma 23.20 to justify the two new casts with the old label. The remaining expansion case is vacuous: it would require $?{⪯}^{+}A$ for non-ground $A$, and no rule derives that judgment.

For E-WrapApp, first suppose its label is $q$. Positive safety of $$A_1\to B_1{⪯}^{+}{A}_2\to B_2$$ inverts to $A_2{⪯}^{-}{A}_1$ and $B_1{⪯}^{+}{B}_2$. These are exactly the safety obligations for the new domain cast labeled $\overline{q}$ and result cast labeled $q$. If the wrapper label is $\overline{q}$, negative safety inverts to $A_2{⪯}^{+}{A}_1$ and $B_1{⪯}^{-}{B}_2$, again exactly matching the swapped labels.

Only E-Mismatch creates blame directly. A mismatch that produced ${\mathsf{blame}}_q$ would have outer cast $⟨G\Leftarrow ?{⟩}^q$. But $?{⪯}^{+}G$ has no derivation for ground $G$; this contradicts $q$-safety. A mismatch labeled $\overline{q}$ may instead create ${\mathsf{blame}}_{\overline{q}}$, which is not excluded. A $q$-safe term contains no ${\mathsf{blame}}_q$, so E-Blame can propagate only an unrelated or complementary blame. Context closure preserves these observations. ◻

Proof. For the first sentence, induct on the length of a purported reduction to ${\mathsf{blame}}_q$. Length zero is excluded by the definition of $q$-safety. At positive length, repeated use of lemma 23.22 says every predecessor is $q$-safe, but the lemma excludes the final contraction that first creates ${\mathsf{blame}}_q$. Blame propagation cannot be first: its premise already contains that blame.

For clause 1, the only $p$-labeled cast has positive-safe endpoints and there is no $\overline{p}$-labeled cast initially, so $a$ is $p$-safe. For clause 2, instantiate the first sentence with $q:=\overline{p}$. Since $\bar{\overline{p}}=p$, the original $p$-labeled cast is exactly a cast carrying $\overline{q}$; its negative-safe endpoints satisfy the definition of $\overline{p}$-safety for $a$. Apply the first sentence. ◻

Proof. Rule P-Unk gives $A{⪯}^{+}?$ in the first clause, so theorem 23.23 excludes ${\mathsf{blame}}_p$. Rule N-Unk gives $?{⪯}^{-}A$ in the second clause, so the same theorem excludes ${\mathsf{blame}}_{\overline{p}}$. The freshness hypothesis ensures the corresponding label-safety premise in each case. ◻

Proof. For the forward implication, induct on $A{⊑}_{\mathsf{ty}}B$. At $B=?$ the two judgments are P-Unk and N-Unk. The two base cases use the corresponding reflexive polar rules. At arrows, apply the two component induction hypotheses: P-Arr uses the negative domain judgment and positive codomain judgment, while N-Arr uses the other two.

Conversely, induct on $B$. If $B=?$, conclude by Pr-Unk. If $B$ is a base type, inversion of $A{⪯}^{+}B$ forces the same base type, so use Pr-Bool or Pr-Nat. If $B=B_1\to B_2$, inversion of the positive judgment forces $A=A_1\to A_2$. Inverting both polar judgments gives $$A_1{⪯}^{+}{B}_1,B_1{⪯}^{-}{A}_1,A_2{⪯}^{+}{B}_2,B_2{⪯}^{-}{A}_2.$$ The induction hypotheses and Pr-Arr finish the proof. ◻

Proof. First invert precision. If $A^{\prime }$ is an arrow, its two component premises give the result. If $A^{\prime }=?$, then $\mathsf{fun}(A^{\prime })=?\to ?$, and both components of the precise arrow are more precise than $?$. No other $A^{\prime }$ is possible because a matchable precise type cannot become a different base type.

For the consistency claim, use the auxiliary statement by induction on the derivation of $D{\sim }_{\mathsf{c}}B$: if $D{⊑}_{\mathsf{ty}}{D}^{\prime }$ and $B{⊑}_{\mathsf{ty}}{B}^{\prime }$, then $D^{\prime }{\sim }_{\mathsf{c}}{B}^{\prime }$. For C-UnkL, precision from $?$ forces $D^{\prime }=?$, so C-UnkL applies; C-UnkR is symmetric. For C-Bool and C-Nat, each less-precise endpoint is either the same base or $?$, and the corresponding base or unknown rule applies. For C-Arr, either successor is $?$, closing by an unknown rule, or both successors are arrows; invert the two precision derivations, apply the induction hypotheses to domain and codomain, and use C-Arr. Since matching has established $\mathsf{fun}(A^{\prime })=B^{\prime }\to C^{\prime }$, applying the auxiliary statement to $D{\sim }_{\mathsf{c}}B$, $D{⊑}_{\mathsf{ty}}{D}^{\prime }$, and $B{⊑}_{\mathsf{ty}}{B}^{\prime }$ derives $D^{\prime }{\sim }_{\mathsf{c}}{B}^{\prime }$. ◻

Proof. Induct on the derivation of $e{⊑}_{\mathsf{src}}{e}^{\prime }$ while inverting the typing of $e$. Constants are unchanged. The variable case uses context precision. For lambdas, the written domain precision and the induction hypothesis for the body give G-Lam and Pr-Arr.

For applications, write the precise premises as $$\mathrm{\Gamma }⊢e_1:C,\mathsf{fun}(C)=B\to A,\mathrm{\Gamma }⊢e_2:D,D{\sim }_{\mathsf{c}}B.$$ The two induction hypotheses give $C{⊑}_{\mathsf{ty}}{C}^{\prime }$ and $D{⊑}_{\mathsf{ty}}{D}^{\prime }$ together with typings of the less precise subterms. Apply lemma 23.28 with its variables $(A,A^{\prime },B,C,D,D^{\prime })$ instantiated as $(C,C^{\prime },B,A,D,D^{\prime })$. The lemma gives $\mathsf{fun}(C^{\prime })=B^{\prime }\to A^{\prime }$ with $B{⊑}_{\mathsf{ty}}{B}^{\prime }$ and $A{⊑}_{\mathsf{ty}}{A}^{\prime }$, as well as $D^{\prime }{\sim }_{\mathsf{c}}{B}^{\prime }$. Rule G-App therefore types the less precise application at $A^{\prime }$. ◻