ch:subtyping: ch:subtyping

Put $$R_N:=\{x:\mathsf{Nat}\},R_T:=\{x:\mathsf{Top}\},R_C:=\{x:\mathsf{Nat},\mathsf{color}:\mathsf{Bool}\}.$$ There are six successful ordered pairs. Their complete rule trees are The remaining two are For and , the target label set $\{x,\mathsf{color}\}$ is not contained in the source label set $\{x\}$. Thus the first premise of S-Rcd fails. For , label inclusion holds, but the field premise would be . Subtype-shape inversion excludes that judgment. These are the remaining three ordered pairs.

The first judgment holds. Its complete structural derivation is The first premise is reversed: the target domain $\mathsf{Nat}$ is below the source domain $\mathsf{Top}$.

The second judgment would require both for its reversed domain premise and for its covariant codomain premise. Subtype-shape inversion excludes that judgment. Operationally, an erroneous covariant use would permit $$g:=\lambda n:\mathsf{Nat}.\mathsf{unit}:\mathsf{Nat}\to \mathsf{Top}$$ to be subsumed to $\mathsf{Top}\to \mathsf{Nat}$. Then $g\mathsf{unit}$ would be assigned type $\mathsf{Nat}$ but would reduce to $\mathsf{unit}$, which is not a natural. This application is the preservation counterexample ruled out by domain contravariance.

Recall The typing of the redex, including width subtyping and subsumption, is Operationally, E-Proj gives $c.x⟶0$. The reduct has the required type by the leaf $$\frac{\phantom{X}}{\cdot ⊢0:\mathsf{Nat}}\mathrm{T}-\mathrm{Zero}.$$ Thus the field selected by reduction has exactly the type retained by the subsumed record interface.

Immutability is essential for the depth part of the argument. If writable fields were covariant, an alias of type $\{q:\mathsf{Nat}\}$ could also be used at $\{q:\mathsf{Top}\}$. A write of through the second alias would leave the first alias reading a Boolean where its type promises a natural. No such write exists for the immutable records of this chapter.

Prove simultaneously for every closed value form that a derivation $\cdot ⊢v:A$ cannot have $A=\mathsf{Bot}$, by induction on that typing derivation. A final introduction rule fixes both the outer syntax and a nonbottom result type: No one of these outer constructors is $\mathsf{Bot}$. A closed value cannot be a variable, and no elimination rule concludes the typing of one of the listed value syntaxes.

It remains to treat a derivation ending in subsumption: If $A=\mathsf{Bot}$, clause Bot-Down of lemma 8.5 forces $C=\mathsf{Bot}$. The first premise is a strictly smaller typing derivation of the same closed value at $\mathsf{Bot}$, contradicting the induction hypothesis. This also explains why all value forms are handled simultaneously: a chain of final subsumptions is peeled until an introduction rule is reached, and bottom cannot appear at either stage.

Let $$R=\{x:\mathsf{Nat},q:\mathsf{Bool}\},S=\{q:\mathsf{Bool},r:\mathsf{Unit}\}.$$ Their common label set is $\{q\}$ and their union of labels is $\{x,q,r\}$. Since the common field types are identical, $$R\bigsqcup S=\{q:\mathsf{Bool}\},R\sqcap S=\{x:\mathsf{Nat},q:\mathsf{Bool},r:\mathsf{Unit}\}.$$ The four bound judgments are the following instances of S-Rcd: For the first row, the singleton target label set is contained in the corresponding source set; for the second, the target label set is contained in $\{x,q,r\}$. Every retained field premise is for $K\in \{\mathsf{Nat},\mathsf{Bool},\mathsf{Unit}\}$ and follows by S-Refl. These inclusions and reflexive field trees are all the premises of the four S-Rcd derivations.

Now replace $S$ by $$S^{\prime }=\{q:\mathsf{Top},r:\mathsf{Unit}\}.$$ The recursive definition computes the common field bounds $$\mathsf{Bool}\bigsqcup \mathsf{Top}=\mathsf{Top},\mathsf{Bool}\sqcap \mathsf{Top}=\mathsf{Bool}.$$ Hence $$R\bigsqcup S^{\prime }=\{q:\mathsf{Top}\},R\sqcap S^{\prime }=\{x:\mathsf{Nat},q:\mathsf{Bool},r:\mathsf{Unit}\}.$$ For example, the $q$ premises of the upper-bound trees are and , while those of the lower-bound trees are and . The identical-field abbreviation does not apply because its hypothesis asks for literally equal common field types, whereas $\mathsf{Bool}\ne \mathsf{Top}$; the global recursive bound calculation is what supplies their join and meet.

Define $$\mathsf{Colorable}:=\{\mathsf{getColor}:\mathsf{Unit}\to \mathsf{Bool}\}$$ and In the context , the observation has the complete derivation Call the displayed observation derivation ${\mathcal{D}}_{\mathsf{obs}}$. For the next tree abbreviate $b_X(o)=⟨o,o.\mathsf{getColor}\mathsf{unit}⟩$. Pair the observation with the original $o:X$, then introduce the term and type binders:

Take the two-method record type and value from the chapter: $$C:=\mathsf{ColorPointObj},\mathsf{colored}:C.$$ The bound premise for instantiation is the width derivation Hence the instantiation and application rules give The requested reduction is The first component remains the original two-method record at type $C$.

The annotated body is still $$⟨o,o.\mathsf{getX}\mathsf{unit}⟩$$ but its local context is now The variable rule gives ${\mathrm{\Omega }}_{\mathsf{Top}}⊢o:X$. To use T-Proj at $\mathsf{getX}$, the derivation in the original term first subsumed $o$ to $$\mathsf{PointObj}=\{\mathsf{getX}:\mathsf{Unit}\to \mathsf{Nat}\}.$$ That step would now require the precise judgment An induction on a derivation with source $X$ proves the needed variable-source inversion: if $\mathrm{\Gamma }(X)=\mathsf{Top}$ and , then $C$ is $X$ or $\mathsf{Top}$. The S-Var case uses the declared bound; the S-Trans case applies the induction hypothesis to its left premise and then lemma 18.6 to its right premise. Structural rules have nonvariable sources. Since $\mathsf{PointObj}$ is neither $X$ nor $\mathsf{Top}$, (1) is the first underivable judgment. Equivalently, after theorem 8.26, the algorithm promotes $X$ to $\mathsf{Top}$ and has no successful clause for a record target. Without (1), the receiver cannot be typed at any record interface containing $\mathsf{getX}$, so the projection and the claimed universal typing cannot be rebuilt.

Assume and begin with a judgment under . The S-Var case of type substitution has exactly three positions for the looked-up declaration.

If the variable is $X$, its old conclusion is . The bound $Q$ was formed before $X$, so $Q[P/X]=Q$. After removing $X$ and transforming the suffix, weaken the premise through that suffix: This is precisely the substituted instance of .

If the looked-up variable $Y$ occurs before $X$, then is a declaration of $\mathrm{\Gamma }$, and $R$ cannot mention the later $X$. Lookup is unchanged: Finally, if , the transformed context is The corresponding lookup tree is These are all possible positions in the ordered context.

For narrowing, suppose the last typing rule is The simultaneous narrowing induction hypotheses give both premises in the same strengthened context: Rebuilding the rule displays both required uses of the induction hypothesis: The term and its result type are unchanged; only the declaration has been narrowed to .

Let The positive query takes source promotion, record comparison, and the top branch in that order. Including every priority guard, its tree is The complete recursive-query list is therefore Since $$w_{\mathrm{\Gamma }}(R)=3,w_{\mathrm{\Gamma }}(X)=1+w_{\mathrm{\Gamma }}(R)=4,w_{\mathrm{\Gamma }}(P)=2,$$ the sole promotion lowers the pair measure from $4+2=6$ to $3+2=5$. The record call then lowers it to $1+1=2$.

For the reversed query , equality fails, the target is not top, the source is not bottom or a variable, and the outer constructors are a record and a variable. Thus its complete guard trace is $$\begin{array}{c}P{\not\equiv }_{\alpha }X,\\ X{\not\equiv }_{\alpha }\mathsf{Top},\\ P{\not\equiv }_{\alpha }\mathsf{Bot},\\ P\text{ is not a variable},\\ (P,X)\text{ matches no common structural form}\end{array}\}⟹\mathsf{failure}.$$ There is no recursive query, no source promotion, and no algorithmic derivation tree for .

Suppose the two nontrivial record derivations have conclusions They supply $J\subseteq I$ and $K\subseteq J$. Fix a target label $\ell \in K$. The three field types named by the two derivations are Their field premises are Because $B_{\ell }$ is a proper component of the middle record, its weight is strictly smaller than the middle-record weight. The lexicographic transitivity induction therefore applies exactly here and gives Doing this for every $\ell \in K$, and composing label inclusions to obtain $K\subseteq I$, supplies all premises of A-Rcd for the desired source and target records. If those records are alpha-identical, priority chooses A-Eq; otherwise the record nonidentity guard holds and A-Rcd rebuilds the conclusion.

Define $\mathsf{sub}(\mathrm{\Gamma },A,B)$ by the following ordered cases. A recursive call returning failure makes the current case return failure; otherwise the named constructor is returned with the recursive trees as premises.

1. If $A{\equiv }_{\alpha }B$, return an A-Eq leaf.

2. If $B=\mathsf{Top}$, return an A-Top leaf.

3. If $A=\mathsf{Bot}$, return an A-Bot leaf.

4. If $A=X$, fail when lookup is undefined; otherwise, with $\mathrm{\Gamma }(X)=U$, recursively compute $D=\mathsf{sub}(\mathrm{\Gamma },U,B)$ and return $A-Var(D)$.

5. For two arrows, recursively compute the domain tree for and the codomain tree for , then return A-Arr of them.

6. For two products or two sums, recursively compare corresponding components in source-to-target order and return A-Prod or A-Sum.

7. For two records, first fail unless every target label occurs in the source. Recursively compare for each target label $j$ and return the finite A-Rcd tree.

8. For two bounded universals, first fail unless the bounds are alpha-identical. Rename the binders to a common fresh $X$, recursively compare the bodies under , and return A-AllK.

9. For every other pair of outer forms, return failure.

The order is part of the definition, so reaching each case proves the side-condition that every earlier test failed. In particular the returned A-Top, A-Bot, A-Var, and structural nodes carry exactly the guards printed in the rule table.

Prove soundness of every returned tree by induction on $$m=w_{\mathrm{\Gamma }}(A)+w_{\mathrm{\Gamma }}(B).$$ The first three branches return leaves whose conclusions and guards check directly. Promotion replaces $w_{\mathrm{\Gamma }}(X)=1+w_{\mathrm{\Gamma }}(U)$ by $w_{\mathrm{\Gamma }}(U)$, so the induction hypothesis says the recursive result is a valid tree for ; adjoining the successful lookup and guards makes a valid A-Var node. Every arrow, product, and sum call is on proper components and hence has smaller measure. Record calls are likewise on field components and there are finitely many of them; the prior label test supplies $J\subseteq I$. In the universal branch, the body is the proper summand measured under the same extended context used by the recursive call, so its measure is smaller; the prior equality test supplies the invariant bound required by A-AllK. The induction hypotheses validate all child trees, and the corresponding rule validates the returned parent. Failure returns no tree and imposes no soundness obligation. Thus every possible successful return is a finite derivation checking against the displayed algorithmic rules.

For the growing-context trace, put The chapter’s displayed iteration leaves . Source promotion reaches the next repeated query: The first requested continuation has both S-AllF premises visible at both nested uses: Its only open recursive premise promotes through every earlier declaration: The second continuation is therefore the following distinct tree: The outer rule compares the target bound $X_i$ with the unbounded source bound $\mathsf{Top}$; the inner rule reverses the bounds of the two negative abbreviations. The two continuations extend the context from ${\mathrm{\Gamma }}_1$ to ${\mathrm{\Gamma }}_2$ and then to ${\mathrm{\Gamma }}_3$. Each target quantifier supplies a fresh alpha-renamed declaration, so neither enlarged ordered context is textually equal to an earlier one.

Now let be a closed full- statement. The direct typing reduction is The displayed T-Sub is the direct derivation’s single use of the input query.

Conversely, first establish the upward arrow-shape fact required in full . Induct on a derivation of The conclusion is that $C=\mathsf{Top}$, or that $C=C_1\to C_2$ with and . Reflexivity, S-Top, and S-Arr give exactly these alternatives. The source of S-Var is a type variable, and S-AllF has a universal source, so neither can be the final rule. We use in parallel the elementary maximality fact proved by induction on its derivation; only reflexivity, top, and transitivity can occur.

In the transitivity case, write The induction hypothesis for the first premise makes $E$ top or an arrow. If $E=\mathsf{Top}$, maximality applied to the second premise makes $C=\mathsf{Top}$. Otherwise let $E=E_1\to E_2$, with and . Apply the arrow induction hypothesis to the second premise. Its top alternative again concludes $C=\mathsf{Top}$; its arrow alternative gives Compose the two chains. This treats transitivity explicitly and exhausts the full- rules.

Now peel final T-Sub steps until the two syntax-directed T-Lam introductions for the displayed annotated lambdas are exposed. Invert the typing of their body $fa$. Application inversion supplies some domain $D$ such that $f$ is usable at a function type with domain $D$ and $a:D$. Inversion of the two variable typings through their final subsumption chains gives for some result type $E$. Apply the just-proved arrow-shape induction to the first judgment: it gives (and ). Therefore The term has no free term variables. Its only possible free type variables are those declared by the supplied closed bound context $\mathrm{\Gamma }$.

Assume a total decider $D$ for derivability of closed full- subtype statements. On a two-counter-machine instance $M$, perform these three effective steps:

1. construct Pierce’s rowing machine $R=\mathcal{R}(M)$;

2. construct the closed subtype statement $J=\mathcal{J}(R)=\mathcal{J}(\mathcal{R}(M))$;

3. run $D(J)$ and answer “halts” exactly when the decider answers “derivable.”

Correctness in the accepting direction is the chain $$D(J)=\mathsf{yes}⟹J\text{ is derivable}⟺R\text{ halts}⟺M\text{ halts}.$$ Because $D$ is total and correct, a negative answer says that $J$ is not derivable. The reverse directions of the same two biconditionals give Thus $D$ would decide both answers to the undecidable machine-halting problem.

One divergent run of one subtype-search strategy proves only that this particular run or strategy fails to terminate on its input. It does not show that the queried judgment is underivable, and still less that no other total algorithm decides all judgments. The two effective reductions and both directions of their biconditionals are what turn a hypothetical total decider into a machine-halting decider; the growing divergent trace alone is not that reduction.