A function that reads an 𝑥 coordinate should accept both of the following values: 𝑝={𝑥=0},𝑐={𝑥=0,𝖼𝗈𝗅𝗈𝗋=𝗍𝗋𝗎𝖾}. Their record types are not equal. Requiring equality would force every caller to rebuild 𝑐 as a one-field record before calling the function. Allowing every type mismatch, on the other hand, would let a function ask for a field that is absent. We add records, top, bottom, and bounded universals to a simply typed term language. The judgment 𝐴<:𝐵 means that an 𝐴-value may be used wherever a 𝐵-value is required; in that case, 𝐴 is a subtype of 𝐵.
The operational base is the call-by-value simply typed calculus of section 2.1, section 2.5, section 2.6: functions and Booleans, then products, sums, and 𝖴𝗇𝗂𝗍 with their typing and reduction rules. We also use the primitive natural numbers 𝖭𝖺𝗍, 0, and 𝗌𝗎𝖼. Relative to the inherited term and value grammars, the syntax delta is 𝑡::=⋯∣0∣𝗌𝗎𝖼(𝑡)∣𝗇𝖺𝗍𝗋𝖾𝖼(𝑡;𝑡0;𝑥.𝑦.𝑡𝑠),𝑣::=⋯∣0∣𝗌𝗎𝖼(𝑣). Their eliminator is 𝗇𝖺𝗍𝗋𝖾𝖼(𝑡;𝑡0;𝑥.𝑦.𝑡𝑠), with predecessor 𝑥 and recursive result 𝑦 bound in 𝑡𝑠. The complete delta is 𝑋Γ⊢0:𝖭𝖺𝗍T−Zero,Γ⊢𝑡:𝖭𝖺𝗍Γ⊢𝗌𝗎𝖼(𝑡):𝖭𝖺𝗍T−Suc,Γ⊢𝑡:𝖭𝖺𝗍Γ⊢𝑡0:𝐴Γ,𝑥:𝖭𝖺𝗍,𝑦:𝐴⊢𝑡𝑠:𝐴Γ⊢𝗇𝖺𝗍𝗋𝖾𝖼(𝑡;𝑡0;𝑥.𝑦.𝑡𝑠):𝐴T−NatRec. Call-by-value evaluation is completed by the following congruence and root rules. The metavariable 𝑣 in E-NatSuc already ranges over values, so the recursive equation cannot fire before the successor argument is a value. Its right-hand side uses simultaneous capture-avoiding substitution, so neither replacement is substituted into the other.
Thus (𝑣1,𝑣2) and its projections are the term notation of chapter 2; they are not the constructor-level pairs and two-context judgments of chapter 9. Here T-Var, T-Lam, T-App, and T-Pair denote the Var, Lam, App, and Pair rules of chapter 2. We retain that chapter’s names Unit-I, Inl, Inr, Case, Fst, and Snd for the other inherited introduction and elimination rules.
First-order term contexts are generated by 𝑋⋅𝖼𝗍𝗑C−Empty,Γ𝖼𝗍𝗑Γ⊢𝐴𝗍𝗒𝗉𝖾𝑥∉dom(Γ)Γ,𝑥:𝐴𝖼𝗍𝗑C−Term.
Every type has kind 𝖳𝗒, so type formation is written Γ⊢𝐴𝗍𝗒𝗉𝖾. Records are immutable finite maps.
Forgetting information safely
Fix a countable set of labels with a total order. A record type is a finite map from labels to types, and a record term is a finite map from labels to terms: {ℓ𝑖:𝐴𝑖}𝑖∈𝐼,{ℓ𝑖=𝑡𝑖}𝑖∈𝐼. The labels in a display are distinct. Reordering a display does not change the map; thus {𝑥:𝖭𝖺𝗍,𝖼𝗈𝗅𝗈𝗋:𝖡𝗈𝗈𝗅} and {𝖼𝗈𝗅𝗈𝗋:𝖡𝗈𝗈𝗅,𝑥:𝖭𝖺𝗍} are literally the same type, not merely isomorphic types. The fixed order of labels is used only to choose a deterministic evaluation order for record fields.
The formation judgment used throughout the first-order development is generated by the following complete rule sheet, together with the inherited base types 𝐾∈{𝖴𝗇𝗂𝗍,𝖡𝗈𝗈𝗅,𝖭𝖺𝗍}:
The types added to the inherited simple types are 𝐴,𝐵::=𝖳𝗈𝗉∣𝖡𝗈𝗍∣{ℓ𝑖:𝐴𝑖}𝑖∈𝐼. Here 𝖳𝗈𝗉 forgets all usable information. By contrast, 𝖡𝗈𝗍 is below every type and has no introduction form in this calculus. In a language with nonreturning constructs it could also be the result type of an operation such as throw; no such operation is added here. The judgment Γ⊢𝐴<:𝐵 is generated by the following rules. The context contains term variables only in this section.
Γ⊢𝐴𝗍𝗒𝗉𝖾
Γ⊢𝐴<:𝐴
S-Refl
Γ⊢𝐴<:𝐵Γ⊢𝐵<:𝐶
Γ⊢𝐴<:𝐶
S-Trans
Γ⊢𝐴𝗍𝗒𝗉𝖾
Γ⊢𝐴<:𝖳𝗈𝗉
S-Top
Γ⊢𝐴𝗍𝗒𝗉𝖾
Γ⊢𝖡𝗈𝗍<:𝐴
S-Bot
Γ⊢𝐵1<:𝐴1Γ⊢𝐴2<:𝐵2
Γ⊢𝐴1→𝐴2<:𝐵1→𝐵2
S-Arr
Γ⊢𝐴1<:𝐵1Γ⊢𝐴2<:𝐵2
Γ⊢𝐴1×𝐴2<:𝐵1×𝐵2
S-Prod
Γ⊢𝐴1<:𝐵1Γ⊢𝐴2<:𝐵2
Γ⊢𝐴1+𝐴2<:𝐵1+𝐵2
S-Sum
𝐽⊆𝐼Γ⊢𝐴𝑗<:𝐵𝑗forevery𝑗∈𝐽
Γ⊢{ℓ𝑖:𝐴𝑖}𝑖∈𝐼<:{ℓ𝑗:𝐵𝑗}𝑗∈𝐽
S-Rcd
Each subtyping rule presupposes formation of every type in its conclusion; later rule displays omit these formation premises.
Structural subtyping gives 𝖳𝗈𝗉 the role of a universal interface without introducing classes.
The record rule performs three jobs. Taking 𝐽⊆𝐼 forgets fields; this is width subtyping. Comparing 𝐴𝑗<:𝐵𝑗 changes a retained field to a less informative type; this is depth subtyping. Treating the components as a finite map gives permutation invariance: reordering fields changes no record type. These are consequences of one representation and one rule, not three independent axioms.
Put 𝖯𝗈𝗂𝗇𝗍:={𝑥:𝖭𝖺𝗍},𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍:={𝑥:𝖭𝖺𝗍,𝖼𝗈𝗅𝗈𝗋:𝖡𝗈𝗈𝗅}. Here S-Refl discharges the sole depth premise 𝖭𝖺𝗍<:𝖭𝖺𝗍, and S-Rcd then derives ⋅⊢𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍<:𝖯𝗈𝗂𝗇𝗍. The reverse judgment cannot be derived: its record-rule instance would need 𝖼𝗈𝗅𝗈𝗋 in the domain of 𝖯𝗈𝗂𝗇𝗍.
Let 𝐴={𝑥:𝖭𝖺𝗍,𝑞:𝖡𝗈𝗍,𝖼𝗈𝗅𝗈𝗋:𝖡𝗈𝗈𝗅},𝐵={𝑞:𝖭𝖺𝗍,𝑥:𝖳𝗈𝗉}. The target labels are both present in 𝐴. The two depth premises are 𝖡𝗈𝗍<:𝖭𝖺𝗍 and 𝖭𝖺𝗍<:𝖳𝗈𝗉. Hence 𝑋𝖡𝗈𝗍<:𝖭𝖺𝗍S−Bot𝑋𝖭𝖺𝗍<:𝖳𝗈𝗉S−Top𝐴<:𝐵S−Rcd. The field order in the conclusion has no mathematical role.
The calculus has no in-place update rule. If one hypothetically added the usual shared assignment rule while retaining covariant record depth, the following calculation would destroy preservation. Suppose a mutable record is shared through two aliases. Its precise alias has type {𝑞:𝖭𝖺𝗍}: 𝑟={𝑞=0}:{𝑞:𝖭𝖺𝗍}. Depth subtyping also exposes the same object through an alias of type {𝑞:𝖳𝗈𝗉}. If update were allowed through that alias, the assignment 𝑟.𝑞:=𝗎𝗇𝗂𝗍 would be accepted because 𝗎𝗇𝗂𝗍:𝖳𝗈𝗉. Reading 𝑟.𝑞 through the original alias would still be assigned 𝖭𝖺𝗍 but would now return 𝗎𝗇𝗂𝗍. The records used below cannot perform this update: evaluation reconstructs immutable values and projection only observes a stored field.
The same aliasing mechanism explains why Java’s covariant mutable arrays need a dynamic ArrayStoreException: the runtime check compensates for a covariance rule that the immutable record calculus can validate statically.
The four nonrecord rules have direct behavioral readings. Every value can be handed to a function that promises to use it only at 𝖳𝗈𝗉; no closed value can be handed out at 𝖡𝗈𝗍. Products preserve the order in each component because their consumers are the two projections. Sums also preserve the order: case analysis retains the injection tag and applies the appropriate branch to the enclosed value. For example, 𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍×𝖭𝖺𝗍<:𝖯𝗈𝗂𝗇𝗍×𝖳𝗈𝗉,𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍+𝖭𝖺𝗍<:𝖯𝗈𝗂𝗇𝗍+𝖳𝗈𝗉, by one use of S-Prod or S-Sum, followed by the already derived record judgment and S-Top. Projection or case analysis can use exactly the information promised on the right. No value-introduction rule concludes 𝖡𝗈𝗍, so subsumption from bottom does not itself manufacture a closed source value.
Arrows have two directions. A value of type 𝐴1→𝐴2 may stand in for a value of type 𝐵1→𝐵2 only when it accepts every 𝐵1 input and produces an acceptable 𝐵2 output. Thus 𝐵1<:𝐴1 but 𝐴2<:𝐵2. The words covariant and contravariant name only these directions: a covariant premise follows source to target, while a contravariant premise reverses it.
Proof of Proposition 8.3 — Why arrow domains reverse
Proof. The false covariant rule and 𝖭𝖺𝗍<:𝖳𝗈𝗉 would give 𝖭𝖺𝗍→𝖭𝖺𝗍<:𝖳𝗈𝗉→𝖭𝖺𝗍. Therefore the identity 𝜆𝑛:𝖭𝖺𝗍.𝑛 could be used at 𝖳𝗈𝗉→𝖭𝖺𝗍. Since 𝗎𝗇𝗂𝗍:𝖳𝗈𝗉, the application (𝜆𝑛:𝖭𝖺𝗍.𝑛)𝗎𝗇𝗂𝗍 would have type 𝖭𝖺𝗍. It takes one beta step to 𝗎𝗇𝗂𝗍, which has no type below 𝖭𝖺𝗍. A well-typed term would reduce to a term without its alleged type. ◻
This counterexample constructs the failure rather than attaching the word “contravariant” to the rule. The domain premise reverses precisely to stop the construction. In nominal languages the same constraint appears when a method override is forbidden from narrowing the type of an accepted parameter: callers are entitled to supply every argument admitted by the supertype interface.
The corresponding coercion makes the reversal mechanical. To turn 𝑓:𝐴1→𝐴2 into a function 𝐵1→𝐵2, first convert the incoming 𝐵1 value in the reversed direction, apply 𝑓, and convert the result in the forward direction: 𝑐𝐴1→𝐴2,𝐵1→𝐵2(𝑓)=𝜆𝑥:𝐵1.𝑐𝐴2,𝐵2(𝑓(𝑐𝐵1,𝐴1(𝑥))). This calculation is an explanation of S-Arr, not an additional subtyping rule. Order-theoretically, the domain conversion is precomposition: 𝑓 is first composed with 𝑐𝐵1,𝐴1:𝐵1→𝐴1. Precomposition reverses the order of its input interface, whereas postcomposition with 𝑐𝐴2,𝐵2:𝐴2→𝐵2 preserves the order of the output interface. This is the mathematical content of contravariance and covariance in S-Arr; the callback example below is one operational consequence.
The same failure appears in an ordinary callback interface. Let 𝖤𝗏𝖾𝗇𝗍={𝗍𝖺𝗀:𝖭𝖺𝗍},𝖢𝗅𝗂𝖼𝗄={𝗍𝖺𝗀:𝖭𝖺𝗍,𝑥:𝖭𝖺𝗍}. A callback registry that accepts a handler of type 𝖤𝗏𝖾𝗇𝗍→𝖭𝖺𝗍 may invoke it on {𝗍𝖺𝗀=0}. The click-only handler 𝜆𝑒:𝖢𝗅𝗂𝖼𝗄.𝑒.𝑥 must therefore not be accepted by that registry. Covariant arrow domains would accept it because 𝖢𝗅𝗂𝖼𝗄<:𝖤𝗏𝖾𝗇𝗍; the eventual call reduces to the missing projection {𝗍𝖺𝗀=0}.𝑥. This is the programming-language form of the formal preservation counterexample, not a second variance principle.
★☆☆ For each ordered pair among {𝑥:𝖭𝖺𝗍},{𝑥:𝖳𝗈𝗉},{𝑥:𝖭𝖺𝗍,𝖼𝗈𝗅𝗈𝗋:𝖡𝗈𝗈𝗅}, derive the subtype judgment or identify the first premise of S-Rcd that fails. Draw every successful rule tree.
Subtyping becomes a property of programs through one typing rule.
Γ⊢𝑡:𝐴Γ⊢𝐴<:𝐵
Γ⊢𝑡:𝐵
T-Sub
Γ⊢𝑡𝑖:𝐴𝑖forevery𝑖∈𝐼
Γ⊢{ℓ𝑖=𝑡𝑖}𝑖∈𝐼:{ℓ𝑖:𝐴𝑖}𝑖∈𝐼
T-Rcd
Γ⊢𝑡:{ℓ𝑖:𝐴𝑖}𝑖∈𝐼𝑘∈𝐼
Γ⊢𝑡.ℓ𝑘:𝐴𝑘
T-Proj
Rule T-Sub is subsumption: once a term has a more informative type, it may be checked at any supertype.
For example, define 𝗑𝖮𝖿:=𝜆𝑝:𝖯𝗈𝗂𝗇𝗍.𝑝.𝑥. Then ⋅⊢𝑐:𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍,⋅⊢𝑐:𝖯𝗈𝗂𝗇𝗍,⋅⊢𝗑𝖮𝖿𝑐:𝖭𝖺𝗍. The middle judgment is the only new step. Evaluation still projects from the original two-field value and returns 0.
Record evaluation is left to right in the fixed label order. A record is a value when all its fields are values. In addition to the inherited congruence rules, we use
𝑡𝑘⟶𝑡′𝑘𝑡𝑖isavalueforeveryℓ𝑖<ℓ𝑘
{…,ℓ𝑘=𝑡𝑘,…}⟶{…,ℓ𝑘=𝑡′𝑘,…}
E-Rcd
𝑘∈𝐼
{ℓ𝑖=𝑣𝑖}𝑖∈𝐼.ℓ𝑘⟶𝑣𝑘
E-Proj
𝑡⟶𝑡′
𝑡.ℓ𝑘⟶𝑡′.ℓ𝑘
E-ProjCong
There is no reduction rule for subsumption. It is evidence used by the type system, not a wrapper present in the term.
Subsumption leaves the source term unchanged. A syntax-directed subtype derivation can instead elaborate to a function 𝑐𝐴,𝐵:𝐴→𝐵 in the same explicitly typed lambda calculus with records. For width subtyping, one possible coercion is 𝑐𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍,𝖯𝗈𝗂𝗇𝗍(𝑟)={𝑥=𝑟.𝑥}. For an arrow derivation with 𝐵1<:𝐴1 and 𝐴2<:𝐵2, the coercion is exactly (18.1). For the opening application, coercion insertion gives 𝗑𝖮𝖿𝑐⇝(𝜆𝑝:𝖯𝗈𝗂𝗇𝗍.𝑝.𝑥)(𝑐𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍,𝖯𝗈𝗂𝗇𝗍𝑐)⟶∗(𝜆𝑝:𝖯𝗈𝗂𝗇𝗍.𝑝.𝑥){𝑥=0}⟶0. The declarative typing relation retains subsumption. No coherence theorem is claimed for two elaborations of the same declarative judgment.
The safety proof must account for derivations ending in T-Sub. Ordinary typing inversion is no longer strong enough: from Γ⊢𝑣:𝐵 we cannot infer the last introduction rule for 𝐵. We first recover the outer shape hidden by subtyping.
Proof of Lemma 18.6 — Top is maximal in the first-order calculus
Proof. Induct on the derivation. Reflexivity and S-Top give the conclusion directly. In a transitivity case, the induction hypotheses give 𝐵=𝖳𝗈𝗉 and then 𝐶=𝖳𝗈𝗉. No first-order rule has 𝖳𝗈𝗉 as its source. ◻
Proof. First prove Bot-Down by induction on a derivation 𝐴<:𝖡𝗈𝗍. Reflexivity gives 𝐴=𝖡𝗈𝗍. In a transitivity case 𝐴<:𝐶<:𝖡𝗈𝗍, the induction hypothesis for the second premise gives 𝐶=𝖡𝗈𝗍, and the induction hypothesis for the first premise then gives 𝐴=𝖡𝗈𝗍. No other rule has bottom as its target.
Induct simultaneously on the remaining subtype-shape claims. A last structural rule fixes the outer constructor and gives its component comparisons. For example, S-Arr concludes 𝐴1→𝐴2<:𝐵1→𝐵2 from 𝐵1<:𝐴1 and 𝐴2<:𝐵2. The downward and upward clauses select the corresponding side of this conclusion. Rule S-Bot gives the exceptional source 𝖡𝗈𝗍, S-Top gives the exceptional target 𝖳𝗈𝗉, and S-Refl gives equality of the two outer types.
Only transitivity can hide the fieldwise information. Consider {ℓ𝑖:𝐴𝑖}𝑖∈𝐼<:𝐶<:{ℓ𝑘:𝐷𝑘}𝑘∈𝐾. The upward induction hypothesis for the first premise says that 𝐶 is 𝖳𝗈𝗉 or a record. The first alternative is impossible: substituting 𝐶=𝖳𝗈𝗉 into the second premise gives 𝖳𝗈𝗉<:{ℓ𝑘:𝐷𝑘}𝑘∈𝐾, while lemma 18.6 would force that record type to equal 𝖳𝗈𝗉. Thus 𝐶={ℓ𝑗:𝐵𝑗}𝑗∈𝐽 with 𝐽⊆𝐼 and 𝐴𝑗<:𝐵𝑗. The downward induction hypothesis for the second premise gives 𝐾⊆𝐽 and 𝐵𝑘<:𝐷𝑘. Hence 𝐾⊆𝐽⊆𝐼,𝐴𝑘<:𝐵𝑘<:𝐷𝑘(𝑘∈𝐾), and one use of S-Trans per retained field proves the record clause. The downward record clause is the same calculation with the two induction hypotheses read in the opposite order; if the intermediate type is bottom, Bot-Down forces the original source to be bottom.
For arrows, if the intermediate is 𝖡𝗈𝗍, Bot-Down makes the original source bottom; if it is 𝖳𝗈𝗉, the second premise can target an arrow only by contradicting lemma 18.6. The remaining transitivity case factors as 𝐴1→𝐴2<:𝐶1→𝐶2<:𝐵1→𝐵2. The two induction hypotheses give 𝐵1<:𝐶1<:𝐴1,𝐴2<:𝐶2<:𝐵2, which are composed in their displayed directions. The same two exceptional intermediates are disposed of before the product and sum calculations. For products they give 𝐴1<:𝐶1<:𝐵1 and 𝐴2<:𝐶2<:𝐵2; for sums they give those same two covariant chains. These calculations prove both the downward and upward product and sum clauses. No remaining last rule has one of the indicated source or target shapes. The three base-type claims use the same induction: only reflexivity, bottom, top, and transitivity can occur, and transitivity composes the two displayed alternatives. ◻
Projection preservation requires a term-level consequence of subtype inversion: a literal record typed through subsumption still contains every field demanded by its record type.
Proof of Lemma 8.6 — Literal-record inversion through subsumption
Proof. Prove the two clauses simultaneously by induction on the typing derivation of the fixed literal 𝑟. If the last rule is T-Rcd, clause (a) is impossible, while clause (b) has 𝐽=𝐼: take the field types from the premises and use S-Refl for each comparison.
Suppose the last rule is T-Sub, with premises Γ⊢𝑟:𝐶 and Γ⊢𝐶<:𝐷. If 𝐷=𝖡𝗈𝗍, Bot-Down in lemma 8.5 gives 𝐶=𝖡𝗈𝗍, contrary to the first induction hypothesis. If 𝐷={ℓ𝑗:𝐵𝑗}𝑗∈𝐽, the downward record clause of lemma 8.5 says that 𝐶 is bottom or 𝐶={ℓ𝑘:𝐶𝑘}𝑘∈𝐾, with 𝐽⊆𝐾 and 𝐶𝑗<:𝐵𝑗. The bottom alternative is again excluded by the first induction hypothesis. Apply the second induction hypothesis to the typing premise Γ⊢𝑟:𝐶. It yields, for every 𝑗∈𝐽⊆𝐾, a type 𝐴𝑗 with Γ⊢𝑣𝑗:𝐴𝑗,𝐴𝑗<:𝐶𝑗<:𝐵𝑗. Compose the last two judgments by S-Trans. No other typing rule can conclude a judgment for the literal syntax 𝑟. ◻
Proof of Lemma 8.7 — Introduction inversion through subsumption
Proof. Induct on the typing derivation of the fixed value. Its introduction rule gives the required component typings with reflexive subtypings. The remaining case ends in Γ⊢𝑣:𝐸Γ⊢𝐸<:𝐹Γ⊢𝑣:𝐹T−Sub. For a lambda 𝜆𝑥:𝐶0.𝑡 with 𝐹=𝐴→𝐵, the downward arrow clause gives 𝐸=𝖡𝗈𝗍 or 𝐸=𝐶1→𝐶2 with 𝐴<:𝐶1 and 𝐶2<:𝐵. Clause (a) excludes the first alternative; in the second, the induction hypothesis gives Γ,𝑥:𝐶0⊢𝑡:𝐷, 𝐶1<:𝐶0, and 𝐷<:𝐶2. Transitivity yields 𝐴<:𝐶0 and 𝐷<:𝐵.
For a pair with 𝐹=𝐴1×𝐴2, the product clause gives 𝐸=𝐶1×𝐶2 after excluding bottom. The induction hypothesis gives types 𝐷𝑖 with Γ⊢𝑣𝑖:𝐷𝑖, 𝐷𝑖<:𝐶𝑖, and the subtype premise gives 𝐶𝑖<:𝐴𝑖; transitivity gives 𝐷𝑖<:𝐴𝑖. For an injection, the sum clause gives the corresponding payload chain 𝐷<:𝐶𝑖<:𝐴𝑖. For 𝗌𝗎𝖼(𝑣) at 𝖭𝖺𝗍, Base-Both leaves 𝐸=𝖭𝖺𝗍 after bottom is excluded, and the induction hypothesis gives Γ⊢𝑣:𝖭𝖺𝗍. Finally, if 𝐹=𝖡𝗈𝗍, Bot-Down gives 𝐸=𝖡𝗈𝗍, contradicting clause (a). ◻
Proof of Lemma 8.8 — Canonical forms through subsumption
Proof. Induct simultaneously on the typing derivation for the eight conclusions. An introduction rule fixes the value constructor; in the record case, lemma 8.6 also gives the field judgments. Suppose the last rule is T-Sub, with ⋅⊢𝑣:𝐸 and 𝐸<:𝐴. If 𝐴=𝐴1→𝐴2, downward arrow shape gives 𝐸=𝖡𝗈𝗍 or 𝐸=𝐶1→𝐶2. The first alternative contradicts clause (a); the induction hypothesis for the second shows that 𝑣 is a lambda. Downward product and sum shape give the same conclusion for pairs and injections. Downward record shape, followed by lemma 8.6, gives the literal and all retained field typings. If 𝐴 is 𝖴𝗇𝗂𝗍, 𝖡𝗈𝗈𝗅, or 𝖭𝖺𝗍, Base-Both gives 𝐸=𝖡𝗈𝗍 or 𝐸=𝐴; the first alternative is impossible and the induction hypothesis classifies the value at 𝐴.
For clause (a), an introduction rule has a nonbottom conclusion. A final subsumption to 𝖡𝗈𝗍 has source 𝖡𝗈𝗍 by Bot-Down, contradicting the induction hypothesis at the shorter derivation. ◻
If Γ⊢𝑡:𝐴, then inserting a fresh term binding into Γ preserves the judgment. If Γ,𝑥:𝐴,Δ⊢𝑡:𝐵 and Γ⊢𝑣:𝐴, then Γ,Δ⊢𝑡[𝑣/𝑥]:𝐵. The same weakening statement holds for first-order subtyping.
Proof of Lemma 8.9 — Weakening and term substitution
Proof. Weakening is an induction on the given typing derivation Γ⊢𝑡:𝐴, and the subtype variant is an induction on Γ⊢𝐴<:𝐵. For substitution, induct on the typing derivation. In the variable case, 𝑥 is replaced by the premise Γ⊢𝑣:𝐴; every other variable is recovered from the shortened context. The lambda case alpha-renames its binder before applying the induction hypothesis. In T-Rcd, apply the hypothesis separately to every finite-map entry. In T-Proj, apply it to the record premise. In T-Sub, apply it to the term premise and retain the unchanged first-order subtype derivation. The inherited application, pair, injection, case, Boolean, and natural-number cases reconstruct their last rule from the substituted premises. ◻
Proof. Induct on the typing derivation, with an inner analysis of the reduction. A final T-Sub has premise Γ⊢𝑡:𝐵 and 𝐵<:𝐴; the induction hypothesis gives Γ⊢𝑡′:𝐵, after which the same subsumption restores 𝐴. In E-Rcd, the induction hypothesis replaces the one reducing field at its declared type, and T-Rcd rebuilds the record. In E-Proj, the typing conclusion for the receiver is a record type {ℓ𝑖:𝐶𝑖}𝑖∈𝐼 containing the projected label. The receiver is a literal record value, so lemma 8.6 gives Γ⊢𝑣𝑘:𝐷𝑘,𝐷𝑘<:𝐶𝑘 for some 𝐷𝑘; T-Sub therefore gives Γ⊢𝑣𝑘:𝐶𝑘.
For beta reduction, inversion of the application rule gives Γ⊢𝜆𝑥:𝐶.𝑒:𝐴0→𝐵0 and Γ⊢𝑣:𝐴0. By lemma 8.7(b), for some 𝐷, Γ,𝑥:𝐶⊢𝑒:𝐷,𝐴0<:𝐶,𝐷<:𝐵0. Subsumption converts 𝑣:𝐴0 to 𝑣:𝐶; term substitution yields 𝑒[𝑣/𝑥]:𝐷; a final subsumption gives 𝑒[𝑣/𝑥]:𝐵0.
For 𝖿𝗌𝗍⟨𝑣1,𝑣2⟩ and 𝗌𝗇𝖽⟨𝑣1,𝑣2⟩, product inversion gives Γ⊢𝑣𝑖:𝐶𝑖 and 𝐶𝑖<:𝐴𝑖. Select the relevant premise and subsume it to the projection’s result type. For a left case contraction, sum inversion gives Γ⊢𝑣:𝐶 with 𝐶<:𝐴1; subsume the payload to 𝐴1 and substitute it into the left branch. The right contraction is symmetric. In the successor branch of natural-number elimination, lemma 8.7(e) gives Γ⊢𝑣:𝖭𝖺𝗍. Rule T-NatRec types 𝑟:=𝗇𝖺𝗍𝗋𝖾𝖼(𝑣;𝑡0;𝑥.𝑦.𝑡𝑠):𝐴. Weaken 𝑟 beneath 𝑥:𝖭𝖺𝗍, then apply lemma 8.9 first to 𝑦↦𝑟 and then to 𝑥↦𝑣. The binders are fresh for Γ, so neither replacement contains the other binder free; the result is exactly the simultaneous substitution printed in E-NatSuc, at type 𝐴. Boolean roots have no hidden payload type. Congruence cases use the induction hypothesis and rebuild their typing rule. ◻
Proof. Induct on the typing derivation. A final T-Sub uses the induction hypothesis for its term premise; changing a type cannot change whether a term is a value or can step. For a record, step its least nonvalue field; if none exists, the record is a value. For a projection, the induction hypothesis shows that the receiver steps or is a value. In the first case E-ProjCong advances the receiver. In the value case, lemma 8.8(c) shows that it is a record containing the named field, so E-Proj applies. Application uses the arrow clause of the same lemma. Products, sums, Booleans, and naturals use their corresponding clauses. There is no closed value of 𝖡𝗈𝗍 by clause (a), so the bottom rule does not create an unhandled value form. ◻
★★☆ Write the projection case of preservation as a complete rule tree for 𝑐.𝑥⟶0, including the width-subtyping and subsumption steps. Then explain why the proof needs immutability: if a retained field could be updated through two differently typed aliases, depth covariance would no longer be justified.
★★☆ Fix a closed value 𝑣 and prove, by induction on a derivation of ⋅⊢𝑣:𝐴, that 𝐴 cannot be 𝖡𝗈𝗍. Treat the possible outer value forms simultaneously. At a final subsumption, apply the appropriate clause of lemma 8.5; the typing premise of T-Sub is the strictly smaller derivation.
An 𝗂𝖿 expression needs one result type even when its branches have different record types. For this grammar the strongest possible claim holds: any two types have a least common supertype and a greatest common subtype. It holds because types are finite syntax trees and the subtype rules admit the constructor-shape inversions just proved; merely having finitely many grammar productions would not suffice. Adding recursive types, type variables with bounds, or mutable fields would require a different argument.
On closed first-order types, <: is reflexive and transitive. It is also antisymmetric: if 𝐴<:𝐵 and 𝐵<:𝐴, then 𝐴=𝐵 as finite-map types. Hence the closed types form a partial order.
Proof of Lemma 18.15 — The first-order subtype order
Proof. Reflexivity and transitivity are rules. For antisymmetry, use simultaneous induction on the combined sizes of 𝐴 and 𝐵 and apply lemma 8.5 in both directions. Top and bottom can be mutual only with themselves. Every other pair has the same outer constructor. Arrow inversion gives mutual domain and codomain comparisons (with the domain directions reversed twice); products and sums give the component comparisons directly. Mutual record width forces equal label sets, and field inversion gives mutual comparisons at every common label. The induction hypotheses give equality of every pair of corresponding components, so the two finite maps are equal. ◻
A type 𝐽 is a join of 𝐴 and 𝐵 when 𝐴<:𝐽,𝐵<:𝐽,𝐴<:𝑈and𝐵<:𝑈⟹𝐽<:𝑈. A type 𝑀 is a meet when 𝑀<:𝐴,𝑀<:𝐵,𝐿<:𝐴and𝐿<:𝐵⟹𝐿<:𝑀. These are properties, not new type constructors.
The recursive bounds𝐴⊔𝐵 and 𝐴⊓𝐵 are mutually recursive operations on closed first-order types. The equations involving top and bottom are 𝖡𝗈𝗍⊔𝐴=𝐴,𝖳𝗈𝗉⊔𝐴=𝖳𝗈𝗉,𝖡𝗈𝗍⊓𝐴=𝖡𝗈𝗍,𝖳𝗈𝗉⊓𝐴=𝐴,𝐴⊔𝖡𝗈𝗍=𝐴,𝐴⊔𝖳𝗈𝗉=𝖳𝗈𝗉,𝐴⊓𝖡𝗈𝗍=𝖡𝗈𝗍,𝐴⊓𝖳𝗈𝗉=𝐴. For 𝐾∈{𝖴𝗇𝗂𝗍,𝖡𝗈𝗈𝗅,𝖭𝖺𝗍}, put 𝐾⊔𝐾=𝐾⊓𝐾=𝐾. Matching compound constructors use (𝐴1→𝐴2)⊔(𝐵1→𝐵2)=(𝐴1⊓𝐵1)→(𝐴2⊔𝐵2),(𝐴1→𝐴2)⊓(𝐵1→𝐵2)=(𝐴1⊔𝐵1)→(𝐴2⊓𝐵2),(𝐴1×𝐴2)⊔(𝐵1×𝐵2)=(𝐴1⊔𝐵1)×(𝐴2⊔𝐵2),(𝐴1×𝐴2)⊓(𝐵1×𝐵2)=(𝐴1⊓𝐵1)×(𝐴2⊓𝐵2),(𝐴1+𝐴2)⊔(𝐵1+𝐵2)=(𝐴1⊔𝐵1)+(𝐴2⊔𝐵2),(𝐴1+𝐴2)⊓(𝐵1+𝐵2)=(𝐴1⊓𝐵1)+(𝐴2⊓𝐵2). The arrow join uses a meet in its domain for the same reason that S-Arr reverses its domain premise: a common upper function must accept every input accepted by either source function. The arrow meet reverses the same calculation. For records 𝑅={ℓ𝑖:𝐴𝑖}𝑖∈𝐼 and 𝑆={ℓ𝑗:𝐵𝑗}𝑗∈𝐽, define 𝑅⊔𝑆={ℓ𝑘:𝐴𝑘⊔𝐵𝑘}𝑘∈𝐼∩𝐽,𝑅⊓𝑆={ℓ𝑖:𝐴𝑖}𝑖∈𝐼∖𝐽∪{ℓ𝑘:𝐴𝑘⊓𝐵𝑘}𝑘∈𝐼∩𝐽∪{ℓ𝑗:𝐵𝑗}𝑗∈𝐽∖𝐼. The unions are unions of finite maps. For two remaining types whose outer constructors differ and are neither 𝖳𝗈𝗉 nor 𝖡𝗈𝗍, define the join to be 𝖳𝗈𝗉 and the meet to be 𝖡𝗈𝗍.
Disjoint labels expose a useful edge case: {𝑥:𝖭𝖺𝗍}⊔{𝑦:𝖭𝖺𝗍}={}. The empty record is the record analogue of 𝖳𝗈𝗉: every record type is below it by width, although a nonrecord type need not be. Thus it is more precise than the global 𝖳𝗈𝗉 and is the least common upper bound of these two record types.
Every recursive call in this definition is on component types whose combined syntax size is smaller. Thus the simultaneous definition terminates; it is not an appeal to the bounds it is about to construct.
Proof of Theorem 18.18 — First-order types form a lattice
Proof. Prove the upper- and lower-bound clauses and their two optimality clauses simultaneously by induction on the combined syntax size of 𝐴 and 𝐵. The top and bottom equations use S-Top and S-Bot. Equal base types use reflexivity. For distinct outer constructors covered by the fallback clause, subtype-shape inversion says that every common upper bound is 𝖳𝗈𝗉 and every common lower bound is 𝖡𝗈𝗍, so the fallback equations are optimal.
Consider the arrow join. The induction hypotheses give 𝐴1⊓𝐵1<:𝐴1,𝐵1,𝐴2,𝐵2<:𝐴2⊔𝐵2. Put 𝐽=(𝐴1⊓𝐵1)→(𝐴2⊔𝐵2). Two uses of S-Arr derive 𝐴1→𝐴2<:𝐽,𝐵1→𝐵2<:𝐽, so 𝐽 is a common upper bound. If 𝐴1→𝐴2<:𝑈 and 𝐵1→𝐵2<:𝑈, upward shape inversion shows that 𝑈 is either 𝖳𝗈𝗉 or 𝐶1→𝐶2. The top case is immediate. In the arrow case inversion gives 𝐶1<:𝐴1,𝐵1,𝐴2,𝐵2<:𝐶2. Meet optimality for the domains and join optimality for the codomains give 𝐶1<:𝐴1⊓𝐵1 and 𝐴2⊔𝐵2<:𝐶2; one final S-Arr proves leastness. For the arrow meet the same calculation reverses roles: a common lower arrow has a domain above both 𝐴1,𝐵1 and a codomain below both 𝐴2,𝐵2, so the domain join and codomain meet are forced.
Products and sums use the component induction hypotheses covariantly. For records, the join retains precisely the labels that every common upper record may require, and its field joins are least by induction. The meet contains the union of the two label sets, and its common fields use the inductively greatest field meets. Rule S-Rcd proves the four bound judgments; record shape inversion proves optimality field by field. These cases exhaust the first-order grammar. ◻
Let 𝑅={ℓ𝑖:𝐴𝑖}𝑖∈𝐼 and 𝑆={ℓ𝑗:𝐵𝑗}𝑗∈𝐽 be closed record types. Suppose that 𝐴𝑘=𝐵𝑘 for every 𝑘∈𝐼∩𝐽. Define 𝑅⊔r𝑆:={ℓ𝑘:𝐴𝑘}𝑘∈𝐼∩𝐽, and 𝑅⊓r𝑆:={ℓ𝑖:𝐴𝑖}𝑖∈𝐼∖𝐽∪{ℓ𝑘:𝐴𝑘}𝑘∈𝐼∩𝐽∪{ℓ𝑗:𝐵𝑗}𝑗∈𝐽∖𝐼, where the unions are unions of finite maps.
Proof of Proposition 8.14 — Conditional record bounds
Proof. By theorem 18.18, 𝐴𝑘⊔𝐴𝑘 is the join of 𝐴𝑘 with itself and 𝐴𝑘⊓𝐴𝑘 is the meet. Since 𝐴𝑘 itself has both universal properties by reflexivity, antisymmetry gives 𝐴𝑘⊔𝐴𝑘=𝐴𝑘=𝐴𝑘⊓𝐴𝑘. Thus the two displayed records are exactly 𝑅⊔𝑆 and 𝑅⊓𝑆 from definition 18.17. Apply theorem 18.18. ◻
For a concrete calculation, put 𝐻={𝑥:𝖭𝖺𝗍,𝗁𝗈𝗋𝗂𝗓𝗈𝗇𝗍𝖺𝗅:𝖭𝖺𝗍},𝐶={𝑥:𝖭𝖺𝗍,𝖼𝗈𝗅𝗈𝗋:𝖡𝗈𝗈𝗅}. Then 𝐻⊔r𝐶=𝖯𝗈𝗂𝗇𝗍,𝐻⊓r𝐶={𝑥:𝖭𝖺𝗍,𝗁𝗈𝗋𝗂𝗓𝗈𝗇𝗍𝖺𝗅:𝖭𝖺𝗍,𝖼𝗈𝗅𝗈𝗋:𝖡𝗈𝗈𝗅}. Consequently an 𝗂𝖿 with an 𝐻 branch and a 𝐶 branch can be checked at 𝖯𝗈𝗂𝗇𝗍 by subsuming each branch. When common field types differ, the global algorithm recursively computes their bounds instead of stopping at the identical-field abbreviation.
★★☆ Compute the record join and meet of {𝑥:𝖭𝖺𝗍,𝑞:𝖡𝗈𝗈𝗅}and{𝑞:𝖡𝗈𝗈𝗅,𝑟:𝖴𝗇𝗂𝗍}, and verify all four bound judgments by S-Rcd. Then replace the second 𝑞 type by 𝖳𝗈𝗉. Compute the resulting global record join and meet from definition 18.17, and explain why the shorter identical-field abbreviation no longer applies.
We use method records only to keep the example object-like without mutation: 𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃:={𝗀𝖾𝗍𝖷:𝖴𝗇𝗂𝗍→𝖭𝖺𝗍},𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃:={𝗀𝖾𝗍𝖷:𝖴𝗇𝗂𝗍→𝖭𝖺𝗍,𝗀𝖾𝗍𝖢𝗈𝗅𝗈𝗋:𝖴𝗇𝗂𝗍→𝖡𝗈𝗈𝗅}.
The function 𝗑𝖮𝖿 forgets extra fields in its result because its result is merely a natural number. Consider instead an operation that must return its input unchanged and also remember the coordinate it observed. If we give it the monomorphic type 𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃→𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃×𝖭𝖺𝗍, then applying it to a colored object forgets, at the type level, that the returned object still has a color method. Ordinary universal quantification ∀𝑋.𝑋→𝑋×𝖭𝖺𝗍 retains 𝑋 but provides no reason why an 𝑋 has a coordinate method. We need both facts at once: 𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.
Bounded quantification retains the type variable 𝑋 while recording the coordinate-method bound 𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.
Extend types and terms by 𝐴,𝐵::=⋯∣𝑋∣∀𝑋<:𝐴.𝐵,𝑡,𝑢::=⋯∣Λ𝑋<:𝐴.𝑡∣𝑡[𝐵]. A context is an ordered list of term declarations 𝑥:𝐴 and type bounds 𝑋<:𝐴. In Γ,𝑋<:𝐴, the type 𝐴 is formed in Γ; in particular, 𝐴 cannot mention the newly bound 𝑋. Lookup is written Γ(𝑋)=𝐴. The universal type is formed when the following two additional formation rules apply:
Γ(𝑋)=𝐴
Γ⊢𝑋𝗍𝗒𝗉𝖾
F-Var
Γ⊢𝐴𝗍𝗒𝗉𝖾Γ,𝑋<:𝐴⊢𝐵𝗍𝗒𝗉𝖾
Γ⊢∀𝑋<:𝐴.𝐵𝗍𝗒𝗉𝖾
F-All
In addition to the preceding subtype rules, Kernel 𝐹<: has
Γ(𝑋)=𝐴
Γ⊢𝑋<:𝐴
S-Var
Γ,𝑋<:𝐴⊢𝐵<:𝐶
Γ⊢∀𝑋<:𝐴.𝐵<:∀𝑋<:𝐴.𝐶
S-AllK
The two displayed bounds in S-AllK must be alpha-identical. This invariance is what the word Kernel records.
The term rules are
Γ,𝑋<:𝐴⊢𝑡:𝐵
Γ⊢Λ𝑋<:𝐴.𝑡:∀𝑋<:𝐴.𝐵
T-TAbs
Γ⊢𝑡:∀𝑋<:𝐴.𝐵Γ⊢𝐶<:𝐴
Γ⊢𝑡[𝐶]:𝐵[𝐶/𝑋]
T-TApp
with the reduction (Λ𝑋<:𝐴.𝑡)[𝐶]⟶𝑡[𝐶/𝑋]. Type abstractions are values, and evaluation first reduces the operator of a type application. Type annotations and type applications are static; the substitution rule above is nevertheless convenient for proving preservation of the typed source calculus.
Proof. Induct on the derivation. Reflexivity and S-Top give the result, and transitivity uses the two induction hypotheses. The remaining first-order rules, S-Var, and S-AllK cannot have 𝖳𝗈𝗉 as source. ◻
The bound has two logically separate uses. From a variable declaration 𝑜:𝑋 and 𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃, S-Var and T-Sub give 𝑜:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃, so 𝑜.𝗀𝖾𝗍𝖷 is available. The result may still mention 𝑋, so returning 𝑜 retains the caller’s precise type.
Define 𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷:=Λ𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.𝜆𝑜:𝑋.⟨𝑜,𝑜.𝗀𝖾𝗍𝖷𝗎𝗇𝗂𝗍⟩,𝖼𝗈𝗅𝗈𝗋𝖾𝖽:={𝗀𝖾𝗍𝖷=𝜆𝑢:𝖴𝗇𝗂𝗍.0,𝗀𝖾𝗍𝖢𝗈𝗅𝗈𝗋=𝜆𝑢:𝖴𝗇𝗂𝗍.𝗍𝗋𝗎𝖾}. Put Ω=𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃,𝑜:𝑋. The observation part is the following complete derivation; the receiver is subsumed before projection: (𝑜:𝑋)∈ΩΩ⊢𝑜:𝑋T−VarΩ(𝑋)=𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃Ω⊢𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃S−VarΩ⊢𝑜:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃T−Sub𝗀𝖾𝗍𝖷∈dom(𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃)Ω⊢𝑜.𝗀𝖾𝗍𝖷:𝖴𝗇𝗂𝗍→𝖭𝖺𝗍T−Proj𝑋Ω⊢𝗎𝗇𝗂𝗍:𝖴𝗇𝗂𝗍Unit−IΩ⊢𝑜.𝗀𝖾𝗍𝖷𝗎𝗇𝗂𝗍:𝖭𝖺𝗍T−App. Pair this conclusion with the original variable, then introduce the term and type binders: Ω⊢𝑜:𝑋Ω⊢𝑜.𝗀𝖾𝗍𝖷𝗎𝗇𝗂𝗍:𝖭𝖺𝗍Ω⊢⟨𝑜,𝑜.𝗀𝖾𝗍𝖷𝗎𝗇𝗂𝗍⟩:𝑋×𝖭𝖺𝗍T−Pair𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃⊢𝜆𝑜:𝑋.⟨𝑜,𝑜.𝗀𝖾𝗍𝖷𝗎𝗇𝗂𝗍⟩:𝑋→𝑋×𝖭𝖺𝗍T−Lam⋅⊢𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷:∀𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.𝑋→𝑋×𝖭𝖺𝗍T−TAbs. Thus 𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷:∀𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.𝑋→𝑋×𝖭𝖺𝗍. Since 𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃, write 𝐶=𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃 in the next two trees. The complete instantiation step is ⋅⊢𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷:∀𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.𝑋→𝑋×𝖭𝖺𝗍⋅⊢𝐶<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃⋅⊢𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷[𝐶]:𝐶→𝐶×𝖭𝖺𝗍T−TApp. Applying the result is a separate ordinary application step: ⋅⊢𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷[𝐶]:𝐶→𝐶×𝖭𝖺𝗍⋅⊢𝖼𝗈𝗅𝗈𝗋𝖾𝖽:𝐶⋅⊢𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷[𝐶]𝖼𝗈𝗅𝗈𝗋𝖾𝖽:𝐶×𝖭𝖺𝗍T−App. The final premise follows by T-Rcd from the two lambda typings displayed in the definition of 𝖼𝗈𝗅𝗈𝗋𝖾𝖽. Its calculation is 𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷[𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃]𝖼𝗈𝗅𝗈𝗋𝖾𝖽𝑡𝑦𝑝𝑒−𝛽⟶(𝜆𝑜:𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.⟨𝑜,𝑜.𝗀𝖾𝗍𝖷𝗎𝗇𝗂𝗍⟩)𝖼𝗈𝗅𝗈𝗋𝖾𝖽𝛽⟶⟨𝖼𝗈𝗅𝗈𝗋𝖾𝖽,𝖼𝗈𝗅𝗈𝗋𝖾𝖽.𝗀𝖾𝗍𝖷𝗎𝗇𝗂𝗍⟩𝑝𝑟𝑜𝑗𝑒𝑐𝑡𝑖𝑜𝑛𝑎𝑛𝑑𝛽⟶∗⟨𝖼𝗈𝗅𝗈𝗋𝖾𝖽,0⟩. The first component retains its color method in both the term and its type. This is the modest object encoding needed here: an immutable record of methods. The dedicated object-calculus and self-type developments own receiver recursion, self types, and state. None of those mechanisms is a premise here.
Type application need not compute. Put 𝑔:∀𝑋<:𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃.𝑋→𝑋 in the context. Rule T-TApp gives 𝑔[𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃]:𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃→𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃, but its operator is a variable, so this neutral term takes no type-beta step.
★★☆ Construct a term of type ∀𝑋<:{𝗀𝖾𝗍𝖢𝗈𝗅𝗈𝗋:𝖴𝗇𝗂𝗍→𝖡𝗈𝗈𝗅}.𝑋→𝑋×𝖡𝗈𝗈𝗅 that returns its argument and the observed Boolean. Give the complete derivation of the projection from a variable of type 𝑋, and reduce one application to a two-method record.
★★☆ Form the unbounded variant. 𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷𝖳𝗈𝗉. It replaces the bound 𝖯𝗈𝗂𝗇𝗍𝖮𝖻𝗃 by 𝖳𝗈𝗉 in the definition of 𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷. Show that it cannot be typed at ∀𝑋<:𝖳𝗈𝗉.𝑋→𝑋×𝖭𝖺𝗍. Identify the first judgment that cannot be derived; “𝑋 is abstract” is not a rule-level answer. Hint: first prove by induction that if Γ(𝑋)=𝖳𝗈𝗉 and Γ⊢𝑋<:𝐵, then 𝐵 is 𝑋 or 𝖳𝗈𝗉; the transitivity case uses lemma 18.21.
A type-variable declaration is unlike an assumption in ordinary System F. Changing 𝑋<:𝑄 to the stronger fact 𝑋<:𝑃, where 𝑃<:𝑄, must preserve every derivation in the suffix Δ. This property is narrowing: if Γ⊢𝑃<:𝑄, a derivation under Γ,𝑋<:𝑄,Δ remains derivable under Γ,𝑋<:𝑃,Δ. In the critical S-Var case, the new lookup gives 𝑋<:𝑃; weakening 𝑃<:𝑄 through the suffix and applying transitivity recovers 𝑋<:𝑄. Type substitution replaces the distinguished lookup by Γ,Δ[𝑃/𝑋]⊢𝑃<:𝑄, obtained by weakening the premise Γ⊢𝑃<:𝑄.
Write Δ[𝑃/𝑋] for pointwise capture-avoiding substitution in every type appearing in the suffix Δ of a context. Term-variable names and type-variable names are distinct. Before substitution, alpha-rename every binder that would capture a free variable of 𝑃.
Mixed-context formation retains C-Empty and C-Term from the first-order calculus and adds Γ𝖼𝗍𝗑Γ⊢𝐴𝗍𝗒𝗉𝖾𝑋∉dom(Γ)Γ,𝑋<:𝐴𝖼𝗍𝗑C−Type Thus every declaration is checked in the prefix to its left. A type variable is formed when its bound is found by lookup. We write J for any of the three judgments 𝐴𝗍𝗒𝗉𝖾,𝐴<:𝐵,𝑡:𝐴, and write J[𝑃/𝑋] for substitution in every type occurring in the judgment, including annotations in 𝑡.
For Kernel 𝐹<:, the following statements include preservation of context formation as well as preservation of judgments.
Weakening. Suppose Γ0,Γ1𝖼𝗍𝗑, Γ0⊢𝐷𝗍𝗒𝗉𝖾, and 𝑑 is a fresh declaration, either 𝑥:𝐷 or 𝑋<:𝐷. Then Γ0,𝑑,Γ1𝖼𝗍𝗑. If additionally Γ0,Γ1⊢J, then Γ0,𝑑,Γ1⊢J.
Narrowing. If Γ⊢𝑃<:𝑄 and Γ,𝑋<:𝑄,Δ𝖼𝗍𝗑, then Γ,𝑋<:𝑃,Δ𝖼𝗍𝗑. Moreover, Γ,𝑋<:𝑄,Δ⊢J⟹Γ,𝑋<:𝑃,Δ⊢J.
Type substitution. If Γ⊢𝑃<:𝑄 and Γ,𝑋<:𝑄,Δ𝖼𝗍𝗑, then Γ,Δ[𝑃/𝑋]𝖼𝗍𝗑, and Γ,𝑋<:𝑄,Δ⊢J⟹Γ,Δ[𝑃/𝑋]⊢J[𝑃/𝑋].
Term substitution. If Γ⊢𝑣:𝐴 and Γ,𝑥:𝐴,Δ𝖼𝗍𝗑, then Γ,Δ𝖼𝗍𝗑 and Γ,𝑥:𝐴,Δ⊢𝑡:𝐵⟹Γ,Δ⊢𝑡[𝑣/𝑥]:𝐵.
In (ii), types and terms in the conclusion are unchanged; only the bound in the context is stronger. In (iii), substitution acts on the term’s type annotations and type applications as well as on its result type.
Proof of Theorem 8.18 — Strengthened structural package
Proof. Weakening, narrowing, and type substitution are simultaneous inductions over context formation, type formation, subtyping, and typing. In the latter two proofs, weakening transports Γ⊢𝑃<:𝑄 through the transformed suffix.
Weakening. For context formation, induct on the length of the suffix Γ1. With an empty suffix, append 𝑑 by C-Term or C-Type. If the last declaration of the suffix is 𝑦:𝐸 or 𝑌<:𝐸, the induction hypothesis forms the prefix containing the insertion; the simultaneous judgment hypothesis weakens the old derivation of 𝐸𝗍𝗒𝗉𝖾 to that prefix. Reapply the corresponding context rule.
For the judgment component, induct on the derivation. A lookup before or after the insertion returns the same declaration. In a term abstraction, apply the induction hypothesis with its fresh term binder appended to Γ1; in type formation, S-AllK, and T-TAbs, do the same with the fresh type binder. The application and type-application rules use the hypothesis on each premise. Arrows, products, sums, and records apply the hypothesis to each component premise.
Narrowing. Context formation and preservation of judgments are simultaneous because a declaration in Δ may contain 𝑋. At an empty suffix, Γ,𝑋<:𝑃 is formed by C-Type; formation of 𝑃 follows from the well-formed subtype premise Γ⊢𝑃<:𝑄. If Δ ends in 𝑦:𝐸 or 𝑌<:𝐸, the context induction hypothesis forms the narrowed prefix, while the simultaneous formation hypothesis changes Γ,𝑋<:𝑄,Δ′⊢𝐸𝗍𝗒𝗉𝖾toΓ,𝑋<:𝑃,Δ′⊢𝐸𝗍𝗒𝗉𝖾. The appropriate context rule then restores the final declaration.
In the simultaneous induction on formation, subtyping, and typing derivations, the critical rule is S-Var. A variable declared before 𝑋 or in Δ has the same lookup after narrowing. For the distinguished variable, the new lookup gives 𝑋<:𝑃. The premise Γ⊢𝑃<:𝑄 weakens to the narrowed context: Γ⊢𝑃<:𝑄⟹Γ,𝑋<:𝑃,Δ⊢𝑃<:𝑄. Transitivity with the new lookup gives: 𝑋Γ,𝑋<:𝑃,Δ⊢𝑋<:𝑃S−VarΓ,𝑋<:𝑃,Δ⊢𝑃<:𝑄Γ,𝑋<:𝑃,Δ⊢𝑋<:𝑄S−Trans. For universal formation and S-AllK, alpha-rename the binder 𝑌 away from 𝑋 and regard 𝑌<:𝐴 as one more declaration in the suffix. The formation induction hypothesis first preserves 𝐴; the body induction hypothesis then applies under Γ,𝑋<:𝑃,Δ,𝑌<:𝐴. A lambda binder is handled identically with a term declaration. Rule T-TAbs uses the type-binder case, T-TApp uses the typing hypothesis for its operator and the subtype hypothesis for its bound check, and T-Sub uses both simultaneous hypotheses. The arrow, product, sum, and finite record rules apply the appropriate hypothesis to each component premise.
Type substitution. Induct on the suffix for context formation. The empty suffix removes 𝑋<:𝑄 and leaves Γ. Suppose the final declaration is 𝑦:𝐸. The simultaneous formation induction gives Γ,Δ′[𝑃/𝑋]⊢𝐸[𝑃/𝑋]𝗍𝗒𝗉𝖾, so C-Term forms the substituted declaration 𝑦:𝐸[𝑃/𝑋]; C-Type gives the identical argument for 𝑌<:𝐸. This proves Γ,Δ[𝑃/𝑋]𝖼𝗍𝗑.
For judgments, induct simultaneously on their derivations. Type-variable formation and S-Var each have three lookup cases. If the variable is the distinguished 𝑋, then its old bound 𝑄 was formed in Γ and hence does not contain 𝑋. The substituted conclusion is 𝑃<:𝑄 in the transformed context, obtained by weakening the assumption through the substituted suffix: Γ⊢𝑃<:𝑄⟹Γ,Δ[𝑃/𝑋]⊢𝑃<:𝑄. The formation case for this occurrence uses weakening: Γ⊢𝑃𝗍𝗒𝗉𝖾⟹Γ,Δ[𝑃/𝑋]⊢𝑃𝗍𝗒𝗉𝖾. A variable declared before 𝑋 is unchanged. A declaration 𝑌<:𝑅 in Δ becomes 𝑌<:𝑅[𝑃/𝑋] in Δ[𝑃/𝑋], so lookup gives 𝑌<:𝑅[𝑃/𝑋]. A term-variable lookup has two positions: a declaration before 𝑋 is unchanged, while the type attached to a declaration in Δ is substituted.
For a universal representative ∀𝑌0<:𝐴.𝐵, choose a new binder name 𝑌 so that 𝑌∉{𝑋,𝑌0}∪FV(Γ)∪FV(Δ)∪FV(𝑃)∪FV(𝐴)∪FV(𝐵), and alpha-rename 𝑌0 and its bound occurrences to 𝑌. In the T-TApp case choose 𝑌 additionally outside FV(𝐶). The formation hypothesis gives 𝐴[𝑃/𝑋]𝗍𝗒𝗉𝖾, and the body hypothesis is applied with 𝑌<:𝐴 appended to the old suffix. It yields a body under 𝑌<:𝐴[𝑃/𝑋], establishing (∀𝑌<:𝐴.𝐵)[𝑃/𝑋]=∀𝑌<:𝐴[𝑃/𝑋].𝐵[𝑃/𝑋]. The same suffix argument proves the binder cases of S-AllK and T-TAbs; in particular, the two Kernel bounds remain alpha-identical. A term abstraction appends 𝑦:𝐴 to the suffix and uses the corresponding term-binder argument. In T-TApp, the simultaneous hypotheses give Γ,Δ[𝑃/𝑋]⊢𝑡[𝑃/𝑋]:∀𝑌<:𝐴[𝑃/𝑋].𝐵[𝑃/𝑋],Γ,Δ[𝑃/𝑋]⊢𝐶[𝑃/𝑋]<:𝐴[𝑃/𝑋]. Put 𝐶𝑃:=𝐶[𝑃/𝑋]. Rebuilding T-TApp derives Γ,Δ[𝑃/𝑋]⊢(𝑡[𝑃/𝑋])[𝐶𝑃]:𝐵[𝑃/𝑋][𝐶𝑃/𝑌]. Its result type satisfies 𝐵[𝑃/𝑋][𝐶𝑃/𝑌]=𝐵[𝐶/𝑌][𝑃/𝑋], where 𝑌≠𝑋 and 𝑌∉FV(𝑃) justify the substitution-commutation equality. Thus this derivation has the required type 𝐵[𝐶/𝑌][𝑃/𝑋]. For T-Sub, substitute in both the typing and subtype premises; for each finite-record rule, substitute independently in every field premise.
Term substitution. Types contain no term variables, so erasing 𝑥:𝐴 does not alter the types of declarations in Δ. Induction on that suffix therefore forms Γ,Δ. We first prove the corresponding term-declaration strengthening for type formation and subtyping: Γ,𝑥:𝐴,Δ⊢𝐶𝗍𝗒𝗉𝖾⟹Γ,Δ⊢𝐶𝗍𝗒𝗉𝖾,Γ,𝑥:𝐴,Δ⊢𝐶<:𝐷⟹Γ,Δ⊢𝐶<:𝐷. Prove both statements simultaneously by induction on their derivations. Type-variable lookup ignores term declarations; in every binder case append the freshly bound declaration to the suffix and use the induction hypothesis. Every other formation or subtype rule applies the induction hypothesis to its premises. The same induction forms the shortened suffix.
Induct on the typing derivation for the term judgment. In T-Var, an occurrence of 𝑥 is replaced by the premise Γ⊢𝑣:𝐴, weakened through Δ by clause (i); a different variable is recovered by lookup in the shortened context. A lambda alpha-renames its binder and applies the hypothesis with that declaration appended to the suffix. A type abstraction does the same with its type binder. A type application substitutes in its operator and applies term-declaration strengthening to its subtype premise. Rule T-Sub substitutes in the term premise and strengthens its subtype derivation in the same way. Applications, products, sums, records, projections, Booleans, and naturals apply their typing rule to the substituted premises. Therefore Γ,𝑥:𝐴,Δ⊢𝑡:𝐵,Γ⊢𝑣:𝐴⟹Γ,Δ⊢𝑡[𝑣/𝑥]:𝐵. ◻
The invariant-bound rule has the following two consequences.
If Γ⊢∀𝑋<:𝐴.𝐵<:𝐶, then 𝐶=𝖳𝗈𝗉 or, after alpha-renaming, 𝐶=∀𝑋<:𝐴.𝐷andΓ,𝑋<:𝐴⊢𝐵<:𝐷.
If Γ contains no type-bound declarations and Γ⊢𝐶<:∀𝑋<:𝐴.𝐵, then 𝐶=𝖡𝗈𝗍 or, after alpha-renaming, 𝐶=∀𝑋<:𝐴.𝐷andΓ,𝑋<:𝐴⊢𝐷<:𝐵.
The hypothesis in (b) follows for the contexts used by closed progress. It cannot be dropped: in a context containing 𝑌<:∀𝑋<:𝐴.𝐵, rule S-Var derives 𝑌<:∀𝑋<:𝐴.𝐵, although 𝑌 is neither bottom nor a universal type.
Proof of Lemma 8.19 — Universal subtype inversion in Kernel F_<:
Proof. Induct on subtype derivations. For (a), S-Refl, S-Top, and S-AllK give the two alternatives. In a transitivity case ∀𝑋<:𝐴.𝐵<:𝐸<:𝐶, the first induction hypothesis gives 𝐸=𝖳𝗈𝗉 or 𝐸=∀𝑋<:𝐴.𝐸0,Γ,𝑋<:𝐴⊢𝐵<:𝐸0. In the first case, lemma 18.21 gives 𝐶=𝖳𝗈𝗉. In the second, the induction hypothesis on 𝐸<:𝐶 gives 𝐶=𝖳𝗈𝗉 or 𝐶=∀𝑋<:𝐴.𝐷 with Γ,𝑋<:𝐴⊢𝐸0<:𝐷; transitivity gives Γ,𝑋<:𝐴⊢𝐵<:𝐷.
For (b), S-Bot, S-Refl, and S-AllK give the alternatives. There is no S-Var case because the context has no type-bound declaration. In transitivity, the second induction hypothesis gives a bottom intermediate or a universal intermediate with bound 𝐴. The first alternative and Bot-Down give a bottom source. In the second, the two body judgments compose under 𝑋<:𝐴. ◻
The following first-order inversion facts remain valid in every well-formed mixed Kernel context.
Upward shape inversion for records, arrows, products, sums, and the three base types holds unchanged. Moreover, a concrete type other than 𝖡𝗈𝗍 is not a subtype of 𝖡𝗈𝗍.
The literal-record conclusion of lemma 8.6 and the introduction conclusions of lemma 8.7 hold unchanged in a mixed Kernel context.
Proof of Lemma 8.20 — Concrete inversion in Kernel F_<:
Proof. For (a), repeat the simultaneous induction on the Kernel subtype derivation. The two new last rules cannot disturb a concrete source: S-Var has a type variable as its source, while S-AllK has a universal source and target. The transitivity case uses the same intermediate-shape calculation as lemma 8.5; if the intermediate is 𝖳𝗈𝗉, lemma 18.21 gives 𝐶=𝖳𝗈𝗉. Prove the last assertion in the same simultaneous induction. In the transitivity case 𝐾<:𝐸<:𝖡𝗈𝗍, upward shape for the first premise forces 𝐸 to be 𝖳𝗈𝗉 or to have the same concrete head as the non-bottom 𝐾; in particular, 𝐸 is not a variable. Maximality excludes the first alternative, and the induction hypothesis applied to 𝐸<:𝖡𝗈𝗍 excludes the second. Outside transitivity, S-Var has the wrong source and the other rules with target 𝖡𝗈𝗍 can only have source 𝖡𝗈𝗍.
For (b), compose all final T-Sub premises into Γ⊢𝑣:𝐾,Γ⊢𝐾<:𝐴, where the introduction rule fixes the concrete type 𝐾. For a lambda, 𝐾=𝐶→𝐷 and the introduction premise is Γ,𝑥:𝐶⊢𝑒:𝐷; part (a) applied to 𝐶→𝐷<:𝐴1→𝐴2 gives 𝐴1<:𝐶 and 𝐷<:𝐴2. For a record literal, 𝐾 contains every written field, and part (a) gives the retained labels and their fieldwise subtypings. Products, sums, and successors yield the component, payload, and predecessor judgments in the same way. Part (a) excludes a target 𝖡𝗈𝗍. ◻
Proof of Lemma 18.27 — Type-abstraction inversion in Kernel
Proof. Induct on the typing derivation. A final T-TAbs gives the universal alternative with 𝐵0=𝐵. Suppose the last rule is T-Sub, with typing premise at 𝐸 and subtype premise 𝐸<:𝐶. Apply the induction hypothesis to the typing premise. If 𝐸=𝖳𝗈𝗉, then lemma 18.21 forces 𝐶=𝖳𝗈𝗉. Otherwise 𝐸=∀𝑋<:𝐴.𝐷, with a body type 𝐵0 satisfying 𝐵0<:𝐷 under 𝑋<:𝐴. Clause (a) of lemma 8.19 applied to 𝐸<:𝐶 gives 𝐶=𝖳𝗈𝗉 or 𝐶=∀𝑋<:𝐴.𝐵 with 𝐷<:𝐵 under the same bound. In the latter case, transitivity gives 𝐵0<:𝐵. No other typing rule concludes a judgment for type-abstraction syntax. ◻
Proof of Corollary 8.21 — Safety of the bounded extension
Proof. For the ordinary syntax, repeat the typing inductions of theorem 8.10, theorem 8.11. Their substitution steps now use theorem 8.18(iv), and their value-root cases use lemma 8.20; no downward shape claim for a type variable is being imported. For preservation, first dispose of a typing derivation whose last rule is T-Sub: apply the induction hypothesis to its premise and restore the same target type with the same subtype derivation. Thus the type-beta case may assume that the whole redex was typed last by T-TApp.
We also strip final subsumption steps from its operator. The preceding type-abstraction inversion lemma, applied to Γ⊢Λ𝑋<:𝐴.𝑡:∀𝑋<:𝐴.𝐵 gives a type 𝐵0 such that Γ,𝑋<:𝐴⊢𝑡:𝐵0andΓ⊢∀𝑋<:𝐴.𝐵0<:∀𝑋<:𝐴.𝐵. The bounds are the same because S-AllK is invariant. More explicitly, an induction on this universal-to-universal subtype derivation strips S-Trans; its S-AllK cases compare the bodies and its transitivity case composes the resulting body judgments. Hence Γ,𝑋<:𝐴⊢𝐵0<:𝐵.
For the type-beta root (Λ𝑋<:𝐴.𝑡)[𝐶]⟶𝑡[𝐶/𝑋], whose T-TApp premise also gives Γ⊢𝐶<:𝐴. Type substitution from theorem 8.18(iii), applied once to typing and once to subtyping, gives Γ⊢𝑡[𝐶/𝑋]:𝐵0[𝐶/𝑋],Γ⊢𝐵0[𝐶/𝑋]<:𝐵[𝐶/𝑋]. One T-Sub therefore gives the reduct the result type 𝐵[𝐶/𝑋] demanded by T-TApp. If the original whole redex had then been subsumed to a further type, the first paragraph restores that target after the step. Congruence for type application follows from the induction hypothesis.
For progress the empty context has no type-bound declaration. In the type-application case, induction on the final subsumption chain, using lemma 8.19(b), shows that a closed value of universal type is Λ𝑋<:𝐴.𝑡. Therefore 𝑡[𝐶] either takes an operator congruence step or is the type-beta redex (Λ𝑋<:𝐴.𝑡0)[𝐶]. The term-application and projection cases use the arrow and record clauses of lemma 8.8; the remaining constructors take their introduction or congruence rules. ◻
★★☆ Give all three lookup subcases in the type-substitution proof for S-Var: the looked-up variable is 𝑋, occurs before 𝑋, or occurs in Δ. Write the conclusion context in each case.
★★☆ Write the narrowing proof for T-TApp in full. Your derivation must show both the narrowed type of the operator and the narrowed proof that the actual type argument satisfies its bound.
The declarative judgment answers what counts as a subtype proof, but it is not yet a program. Rule S-Trans guesses an intermediate type, and S-Refl overlaps every structural rule. The deterministic relation below removes the intermediate-type guess while preserving derivability.
Write Γ⊢a𝐴<:𝐵 when the following deterministic procedure succeeds. The tests have priority in their enumerated order, and a matching test returns without inspecting a lower-priority branch. The procedure’s input contract includes derivations of Γ𝖼𝗍𝗑, Γ⊢𝐴𝗍𝗒𝗉𝖾, and Γ⊢𝐵𝗍𝗒𝗉𝖾. An implementation validates those three conditions once at its entry point and reports an ill-formed-input diagnostic when, for example, a source variable has no declaration; that diagnostic is not the negative answer to a well-formed subtype query.
If 𝐴 and 𝐵 are alpha-identical, succeed.
Otherwise, if 𝐵=𝖳𝗈𝗉, succeed.
Otherwise, if 𝐴=𝖡𝗈𝗍, succeed.
Otherwise, if 𝐴=𝑋, look up Γ(𝑋)=𝑈 and recursively check Γ⊢a𝑈<:𝐵.
Otherwise, if both types are arrows, check their domains in reverse order and their codomains in forward order.
Otherwise, if both types are products, check both components in forward order.
Otherwise, if both types are sums, check both components in forward order.
Otherwise, if both types are records, first fail if a target label is absent from the source; if none is absent, check every target field against the source field with the same label.
Otherwise, if the types are ∀𝑋<:𝐴.𝐵 and ∀𝑋<:𝐶.𝐷, fail unless 𝐴≡𝛼𝐶; when the bounds are alpha-identical, alpha-rename them to the same 𝑋 and check Γ,𝑋<:𝐴⊢a𝐵<:𝐷.
In every other case, fail.
Thus 𝑋<:𝑋 never follows a chain of bounds, 𝑋<:𝖳𝗈𝗉 takes the top branch rather than the promotion branch, and an identical pair of structured types takes the equality branch rather than a componentwise branch.
Proof of Proposition 18.29 — Source-only promotion
Proof. Only clause 4 consults a bound, and its recursive query is 𝑈<:𝐵, with the target 𝐵 unchanged. Every other recursive clause descends through matching outer constructors. ◻
The successful branches produce proof trees with the following rules. Each side condition records that all earlier tests failed, so this rule presentation has exactly the same control as the procedure.
𝐴≡𝛼𝐵
Γ⊢a𝐴<:𝐵
A-Eq
𝐴≢𝛼𝖳𝗈𝗉
Γ⊢a𝐴<:𝖳𝗈𝗉
A-Top
𝐵≢𝛼𝖡𝗈𝗍𝐵≢𝛼𝖳𝗈𝗉
Γ⊢a𝖡𝗈𝗍<:𝐵
A-Bot
𝑋≢𝛼𝐵𝐵≢𝛼𝖳𝗈𝗉Γ(𝑋)=𝑈Γ⊢a𝑈<:𝐵
Γ⊢a𝑋<:𝐵
A-Var
𝐴1→𝐴2≢𝛼𝐵1→𝐵2Γ⊢a𝐵1<:𝐴1Γ⊢a𝐴2<:𝐵2
Γ⊢a𝐴1→𝐴2<:𝐵1→𝐵2
A-Arr
𝐴1×𝐴2≢𝛼𝐵1×𝐵2Γ⊢a𝐴1<:𝐵1Γ⊢a𝐴2<:𝐵2
Γ⊢a𝐴1×𝐴2<:𝐵1×𝐵2
A-Prod
𝐴1+𝐴2≢𝛼𝐵1+𝐵2Γ⊢a𝐴1<:𝐵1Γ⊢a𝐴2<:𝐵2
Γ⊢a𝐴1+𝐴2<:𝐵1+𝐵2
A-Sum
{ℓ𝑖:𝐴𝑖}𝑖∈𝐼≢𝛼{ℓ𝑗:𝐵𝑗}𝑗∈𝐽𝐽⊆𝐼Γ⊢a𝐴𝑗<:𝐵𝑗forevery𝑗∈𝐽
Γ⊢a{ℓ𝑖:𝐴𝑖}𝑖∈𝐼<:{ℓ𝑗:𝐵𝑗}𝑗∈𝐽
A-Rcd
∀𝑋<:𝐴.𝐵≢𝛼∀𝑋<:𝐴.𝐶Γ,𝑋<:𝐴⊢a𝐵<:𝐶
Γ⊢a∀𝑋<:𝐴.𝐵<:∀𝑋<:𝐴.𝐶
A-AllK
The absence of a universal rule with two different bounds is the failure branch in the procedure. The displayed guards make the successful root unique. Since the recursive calls are themselves evaluated by the same priority list, a successful query also has a unique algorithmic proof tree.
In the context 𝑋<:𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍, the query 𝑋<:𝖯𝗈𝗂𝗇𝗍 is not an outer-shape comparison. Clause 4 produces the following complete tree, where Γ=𝑋<:𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍: 𝑋≢𝛼𝖯𝗈𝗂𝗇𝗍𝖯𝗈𝗂𝗇𝗍≢𝛼𝖳𝗈𝗉Γ(𝑋)=𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍≢𝛼𝖯𝗈𝗂𝗇𝗍{𝑥}⊆{𝑥,𝖼𝗈𝗅𝗈𝗋}𝖭𝖺𝗍≡𝛼𝖭𝖺𝗍Γ⊢a𝖭𝖺𝗍<:𝖭𝖺𝗍A−EqΓ⊢a𝖢𝗈𝗅𝗈𝗋𝖯𝗈𝗂𝗇𝗍<:𝖯𝗈𝗂𝗇𝗍A−RcdΓ⊢a𝑋<:𝖯𝗈𝗂𝗇𝗍A−Var. The record clause checks the single 𝑥 field by the equality clause. In contrast, 𝖯𝗈𝗂𝗇𝗍<:𝑋 fails. Its target is neither 𝖳𝗈𝗉 nor a record, and the algorithm deliberately has no target-promotion clause. The bound says that every 𝑋 can be used as a point; it does not say that every point is an 𝑋.
Write 𝐽⇝𝖺𝐽′ when one algorithmic step replaces a source type variable by the bound found for it in the ordered context. This relation is on subtype queries; the term relation 𝑒⇝𝑒′ instead denotes coercion elaboration.
Because contexts are ordered, following a variable bound cannot return to the same variable. Raw syntax size is not a decreasing measure: A-Var replaces a source variable 𝑋 of size one by its bound Γ(𝑋), which may be arbitrarily larger, 𝑋<:𝐵⇝𝖺Γ(𝑋)<:𝐵. The measure must charge 𝑋 for the size of the bound it exposes. The following numerical measure turns that observation into a termination proof without recursing on an extended context. First construct a finite weight map 𝜌Γ by induction from left to right through the ordered context. Term declarations leave the map unchanged; extending a prefix Γ by 𝑋<:𝐴 records 𝜌Γ,𝑋<:𝐴(𝑋)=1+𝑤𝜌Γ(𝐴) and preserves the weights of earlier variables. Now define 𝑤𝜌 structurally on types: 𝑤𝜌(𝖳𝗈𝗉)=𝑤𝜌(𝖡𝗈𝗍)=𝑤𝜌(𝖭𝖺𝗍)=𝑤𝜌(𝖡𝗈𝗈𝗅)=𝑤𝜌(𝖴𝗇𝗂𝗍)=1,𝑤𝜌(𝑋)=𝜌(𝑋),𝑤𝜌(𝐴→𝐵)=1+𝑤𝜌(𝐴)+𝑤𝜌(𝐵), with the same sum for products and sums, 𝑤𝜌({ℓ𝑖:𝐴𝑖}𝑖∈𝐼)=1+∑𝑖∈𝐼𝑤𝜌(𝐴𝑖), and 𝑤𝜌(∀𝑋<:𝐴.𝐵)=1+𝑤𝜌(𝐴)+𝑤𝜌[𝑋↦1+𝑤𝜌(𝐴)](𝐵). Finally write 𝑤Γ(𝐴):=𝑤𝜌Γ(𝐴). The map construction is structural on the context because a bound mentions only its strict prefix; the second construction is structural on the type. In particular, the universal clause extends a finite map while recursing on the proper subterm 𝐵, rather than claiming that the context itself decreases.
Proof. Use 𝑤Γ(𝐴)+𝑤Γ(𝐵) as the recursive-call measure. By proposition 18.29, promoting a source 𝑋 replaces weight 1+𝑤Γ(Γ(𝑋)) by 𝑤Γ(Γ(𝑋)). A structural clause replaces the pair by proper components; the universal body is a proper summand measured in the extended context. Record premises are finite. Thus every recursive call strictly decreases a natural number. The priority list chooses a unique clause, finite map lookup is deterministic, and every recursive result is deterministic; induction on the measure gives the claim. ◻
The two lemmas hidden by transitivity
Soundness of each algorithmic rule is immediate except promotion, where S-Var is followed by declarative transitivity. Completeness is harder: a declarative derivation may end with S-Trans, although the algorithm has no such clause. We must prove that transitivity is admissible for the algorithm itself. Narrowing then uses it, because strengthening the bound used by A-Var replaces one recursive premise by two composable ones.
Suppose Γ0,Γ1⊢a𝐴<:𝐵 and the context obtained by inserting a fresh, well-formed declaration sequence Σ is well formed. Then Γ0,Σ,Γ1⊢a𝐴<:𝐵. The types 𝐴 and 𝐵 are unchanged.
Proof. Induct on the algorithmic proof tree. The alpha-equality and the top and bottom tests do not inspect the context. For A-Var, lookup of a variable declared in Γ0 or Γ1 returns the same textual bound after the fresh insertion; apply the induction hypothesis to its recursive comparison and rebuild A-Var. All its guards are equations between unchanged types. The arrow, product, sum, and record rules apply the induction hypothesis to each displayed recursive premise. Under A-AllK, alpha-rename the bound variable away from Σ and apply the induction hypothesis with that binder appended to Γ1: Γ0,Γ1,𝑋<:𝐶⊢a𝐷<:𝐸⟹Γ0,Σ,Γ1,𝑋<:𝐶⊢a𝐷<:𝐸. The extended conclusion context is well formed by theorem 8.18(i). Applying A-AllK to the transformed body judgment derives the required universal comparison. ◻
Proof of Lemma 8.25 — Algorithmic transitivity and narrowing
Proof. Induction on the middle type alone fails in the source-promotion case: 𝐷′1:Γ⊢a𝑈<:𝐵𝐷1:Γ⊢a𝑋<:𝐵A−Var𝐷2:Γ⊢a𝐵<:𝐶. The recursive composition of 𝐷′1 with 𝐷2 has the same middle type 𝐵. Its left derivation is, however, strictly shorter; this forces the height tiebreaker in the following lexicographic measure. Prove (a) simultaneously for every well-formed context Γ, by lexicographic induction on (𝑤Γ(𝐵),ℎ(𝐷1)), where 𝐷1 derives 𝐴<:𝐵; the height of the right derivation 𝐷2 is not a measure coordinate. In the source-promotion case the height coordinate decreases even when promotion reaches a nonvariable middle type. The case analysis below uses proposition 18.29: a bound can change the source of a query but never its target. In the universal case the induction hypothesis is therefore available at the extended context Γ,𝑋<:𝐴; its context-relative weight is strictly smaller than the enclosing universal weight.
If 𝐷1 ends in A-Eq, then 𝐴≡𝛼𝐵 and 𝐷2 is the desired derivation. If 𝐷2 ends in A-Eq, then 𝐵≡𝛼𝐶 and 𝐷1 is the desired derivation. No recursive call occurs in either case.
Suppose 𝐷1 ends in A-Var. Then 𝐴=𝑋, Γ(𝑋)=𝑈, and its recursive premise 𝐷′1 derives 𝑈<:𝐵. The induction hypothesis applies to 𝐷′1 and 𝐷2: the middle type 𝐵 is unchanged, while ℎ(𝐷′1)<ℎ(𝐷1). It gives 𝑈<:𝐶. If 𝐶=𝑋, equality gives 𝑋<:𝑋; if 𝐶=𝖳𝗈𝗉, use A-Top; in every other case rebuild A-Var to obtain 𝑋<:𝐶. This includes 𝑋<:𝖡𝗈𝗍 when Γ(𝑋)=𝖡𝗈𝗍.
For a derivation not ending in source promotion, 𝐶=𝖳𝗈𝗉 uses A-Top and 𝐴=𝖡𝗈𝗍 uses A-Bot. If the middle type 𝐵 is 𝖳𝗈𝗉, its right derivation can only conclude 𝐶=𝖳𝗈𝗉. If 𝐵=𝖡𝗈𝗍, the left derivation, which no longer ends in source promotion, forces 𝐴=𝖡𝗈𝗍. If 𝐵 is a base type or variable, a derivation 𝐷1 concluding 𝐴<:𝐵 can end only in A-Eq, A-Bot, or A-Var: structural rules have a different target shape, and target promotion does not exist. Excluding A-Var and A-Bot leaves A-Eq; hence 𝐷1 ends in A-Eq, so 𝐴=𝐵 and 𝐷2 is the desired derivation.
Let the middle type be an arrow, product, sum, record, or universal. With source promotion and the top/bottom cases separated, the two derivations have compatible outer shapes. Apply the transitivity hypothesis to corresponding components. Every component of the middle type has smaller weight than the whole middle type, so the first lexicographic coordinate decreases. Arrow domains are composed in the order 𝐶1<:𝐵1<:𝐴1, and codomains in the order 𝐴2<:𝐵2<:𝐶2. For records, every field demanded by 𝐶 is demanded by 𝐵 and therefore present in 𝐴; fieldwise transitivity rebuilds A-Rcd. Products rebuild A-Prod from their two covariant component chains, and sums rebuild A-Sum from theirs. If the reconstructed source and target happen to be alpha-identical, the procedure takes A-Eq instead; otherwise the relevant structural guard holds. For a universal middle type, the identical-bound test forces all three bounds to be the same after alpha-renaming; otherwise one of the two premises could not have succeeded. Apply transitivity to the bodies under that common bound and rebuild A-AllK. This is precisely where Kernel invariance is used.
For (b), induct on the height of the algorithmic derivation being narrowed. All clauses except source promotion apply the narrowing induction hypothesis to their strictly smaller recursive premises. If the promoted source is not 𝑋, its lookup remains available. Apply the narrowing induction hypothesis to its recursive comparison—whether the variable was declared before 𝑋 or in Δ—and then rebuild A-Var. If the source is 𝑋, the recursive premise derives 𝑄<:𝐵; the induction hypothesis gives Γ,𝑋<:𝑃,Δ⊢a𝑄<:𝐵. By lemma 8.24, the assumption Γ⊢a𝑃<:𝑄 gives Γ,𝑋<:𝑃,Δ⊢a𝑃<:𝑄. Transitivity in that context gives 𝑃<:𝐵. The A-Var guards say 𝐵≠𝑋 and 𝐵≠𝖳𝗈𝗉, so rebuild 𝑋<:𝐵 with A-Var. Under a universal binder, alpha-rename away from 𝑋 and invoke the narrowing induction hypothesis on its body. Each recursive narrowing premise has smaller derivation height. ◻
Kernel type and context formation are decidable independently of subtyping: scan an ordered context from left to right, checking each bound in its prefix, and recurse structurally through the finite type grammar. Alpha-equality is decidable by the same binder-normalization used in the algorithmic rules.
Proof of Theorem 8.26 — Soundness and completeness of algorithmic subtyping
Proof. For soundness, induct on the successful algorithmic trace. A-Eq uses S-Refl; A-Top, A-Bot, and each matching structural clause use their declarative counterparts. In the promotion clause, lookup gives 𝑋<:𝑈 by S-Var, the induction hypothesis gives 𝑈<:𝐵, and S-Trans gives 𝑋<:𝐵. The universal clause is exactly S-AllK.
For completeness, induct on the declarative derivation. Reflexivity takes A-Eq. Top and bottom take their priority branch unless equality has already succeeded. Arrows, products, sums, records, and invariant universals take A-Eq when the whole types are alpha-identical and otherwise take the corresponding guarded structural rule after applying the induction hypotheses. For S-Var with bound 𝑈, the query 𝑋<:𝑈 takes A-Top when 𝑈=𝖳𝗈𝗉; otherwise it promotes 𝑋 to 𝑈 and the recursive query succeeds by A-Eq. For S-Trans, apply the two induction hypotheses and then lemma 8.25(a). Reflexivity, top, bottom, variable promotion, arrows, products, sums, records, invariant universals, and transitivity exhaust the declarative derivation. Decidability follows from equivalence and theorem 8.23. ◻
The selected equal-bound rule is Laird’s decidable Kernel baseline [Lai23]. The local theorem extends that boundary with records and bottom and proves its own algorithmic equivalence. Laird’s Propositions 8.4–8.5 instead establish decidable type checking for a richer two-quantifier system; that result is not imported here.
Ghelli’s nameless presentation and complexity analysis concern Kernel 𝖥𝗎𝗇 at their own grammar and representation [Ghe96]. They supply a complexity boundary, not the soundness or completeness proof for the record-and-bottom extension.
The decision procedure takes a formed query Γ⊢𝐴<:𝐵 and returns whether that judgment is derivable. A bidirectional term checker may call it after synthesizing 𝐴 and obtaining an expected type 𝐵. Synthesis for a variable-headed application additionally requires an operation that promotes the variable through its bound. A conditional can instead check both branches against one expected type. To synthesize a conditional type, one must define a join for Kernel 𝐹<:; the operations ⊔ and ⊓ of definition 18.17 apply only to closed first-order types.
★★☆ Run the algorithm, listing every recursive query, on 𝑋<:{𝑥:𝖭𝖺𝗍,𝑞:𝖡𝗈𝗈𝗅}⊢a𝑋<:{𝑥:𝖳𝗈𝗉} and on the reversed query. State the decreasing weight at each source promotion.
★★☆ Fill in the record case of algorithmic transitivity. For a target label ℓ, write 𝐴ℓ, 𝐵ℓ, and 𝐶ℓ for its field types in the source, intermediate, and target records, respectively, and show exactly where the derivations of 𝐴ℓ<:𝐵ℓ and 𝐵ℓ<:𝐶ℓ enter fieldwise transitivity.
★★★ Translate the priority list into pseudocode returning either a finite algorithmic derivation tree or failure. Prove by induction on the recursive measure that every returned tree checks against the rules above. This is a mathematical specification exercise; no executable supplement is required here.
Kernel 𝐹<: compares universal bodies under the same bound. Full 𝐹<: also compares bounds contravariantly: replace S-AllK by
Γ⊢𝑇1<:𝑆1Γ,𝑋<:𝑇1⊢𝑆2<:𝑇2
Γ⊢∀𝑋<:𝑆1.𝑆2<:∀𝑋<:𝑇1.𝑇2
S-AllF
Notice the context of the second premise: occurrences of 𝑋 in both bodies are checked under the target bound 𝑇1. This rebinding is absent from Kernel 𝐹<:.
Call the calculus with grammar 𝐴::=𝑋∣𝐴→𝐴∣∀𝑋<:𝐴.𝐴∣𝖳𝗈𝗉, ordered bound contexts, reflexivity, transitivity, top, variable promotion, arrow subtyping, and S-AllFfull 𝐹<:. This name refers to that exact subtyping signature; records, products, sums, and bottom play no part in the negative theorem. No undecidability claim for an extension with those additional rules follows merely from syntactic inclusion: such a claim would also require conservativity on judgments in the displayed fragment.
All contexts, types, terms, machines, and configurations in this section are finite strings with an effective coding. “Recursive procedure” means a Turing-computable partial function on those codes; “total” means that it halts on every well-formed input. A many-one reduction below is therefore a total computable map preserving yes- and no-instances.
Proof. Induct on the derivation. Reflexivity and S-Top give the result, and transitivity uses the two induction hypotheses. Variable promotion, S-Arr, and S-AllF cannot have 𝖳𝗈𝗉 as source. ◻
The difficulty is visible before the undecidability proof, but it must not be confused with that proof. To make a comparison regenerate itself, we first need a type operation that reverses a subtype query. A bounded universal does exactly that in its bound. Keep the descriptive notation 𝖱𝖾𝗏 throughout the calculation: 𝖱𝖾𝗏𝐴:=∀𝑋<:𝐴.𝑋,∀𝑋.𝐵:=∀𝑋<:𝖳𝗈𝗉.𝐵.𝖱𝖾𝗏 is an abbreviation for reversal of the bound premise, not a Curry–Howard negation connective. Comparing 𝖱𝖾𝗏𝐴 with 𝖱𝖾𝗏𝐵 asks for 𝐵<:𝐴 in the contravariant bound premise; their bodies then compare by reflexivity.
The reversed query must rebuild the quantified target from the variable just introduced. The body 𝖱𝖾𝗏(∀𝑌<:𝑋.𝖱𝖾𝗏𝑌) was chosen for precisely that purpose: its outer 𝖱𝖾𝗏 layer reverses the comparison once, and the inner layer reverses it again after a fresh bounded variable has entered the context. Package this body under an unbounded quantifier: Θ:=∀𝑋.𝖱𝖾𝗏(∀𝑌<:𝑋.𝖱𝖾𝗏𝑌). Consider the following well-formed subtyping statement: 𝑋0<:Θ⊢𝑋0<:∀𝑋1<:𝑋0.𝖱𝖾𝗏𝑋1. Promotion first replaces 𝑋0 by its bound Θ. The first complete iteration then has two nested uses of S-AllF: alpha-renaming its binders at this iteration gives Θ=∀𝑋1.𝖱𝖾𝗏(∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2), The inner comparison is ∀𝑍<:(∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2).𝑍<:∀𝑍<:𝑋1.𝑍.Γ0⊢𝑋0<:𝖳𝗈𝗉Γ1⊢𝑋1<:∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2Γ1,𝑍<:𝑋1⊢𝑍<:𝑍Γ1⊢𝖱𝖾𝗏(∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2)<:𝖱𝖾𝗏𝑋1S−AllFΓ0⊢Θ<:∀𝑋1<:𝑋0.𝖱𝖾𝗏𝑋1S−AllF, where Γ0=𝑋0<:Θ and Γ1=Γ0,𝑋1<:𝑋0. The first premise is S-Top; the innermost body premise is S-Refl. The recursive inner bound premise is Γ1⊢𝑋1<:∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2. Its first source promotion replaces 𝑋1 by 𝑋0. Γ1⊢𝑋1<:∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2⇝𝖺Γ1⊢𝑋0<:∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2⇝𝖺Γ1⊢Θ<:∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2. The last query begins a second complete iteration: Γ1⊢𝑋1<:𝖳𝗈𝗉Γ2⊢𝑋2<:∀𝑋3<:𝑋2.𝖱𝖾𝗏𝑋3Γ2,𝑍<:𝑋2⊢𝑍<:𝑍Γ2⊢𝖱𝖾𝗏(∀𝑋3<:𝑋2.𝖱𝖾𝗏𝑋3)<:𝖱𝖾𝗏𝑋2S−AllFΓ1⊢Θ<:∀𝑋2<:𝑋1.𝖱𝖾𝗏𝑋2S−AllF, where Γ2=Γ1,𝑋2<:𝑋1. The fresh 𝑍 is the binder introduced by the inner S-AllF; it is distinct from 𝑋3, the binder already written inside the source bound. The remaining recursive premise now promotes 𝑋2 through 𝑋1 and 𝑋0 to expose Θ once more. Each iteration therefore recreates the same query shape in a context with one more bounded variable.
This calculation motivates the negative result: the full rule can manufacture unbounded computational state in contexts. It does not prove the result. Cycle detection for this one input might still leave some other total decision procedure. Undecidability requires a reduction from two-counter-machine halting.
A bound context Γ=𝑋1<:𝐴1,…,𝑋𝑛<:𝐴𝑛 is closed when the variables are distinct and FV(𝐴𝑖)⊆{𝑋1,…,𝑋𝑖−1}(1≤𝑖≤𝑛). A statement Γ⊢𝑆<:𝑇 is closed when Γ is closed and every free variable of 𝑆 and 𝑇 is declared in Γ. Thus a closed statement may have a nonempty context; “closed” does not mean Γ=⋅.
A two-counter machine is a finite labeled program together with two nonnegative integer counters. An instruction either halts, increments one counter and jumps, or tests one counter: at zero it jumps to one label, and otherwise it decrements that counter and jumps to another. A configuration is a program label and the two counter values. From a supplied initial configuration, write 𝑐𝑛 for the configuration reached after 𝑛 deterministic steps, when it is defined. The halting problem asks whether there is an 𝑛∈ℕ for which 𝑐𝑛 is defined and its program label is a halt instruction; this problem is undecidable [Pie92].
Pierce’s rowing machine is the conservative deterministic intermediate calculus used by the reduction. At a fixed width 𝑤, a row has grammar 𝜌::=𝑥𝑖∣𝖧𝖺𝗅𝗍∣𝜆𝑥1,…,𝑥𝑤.⟨𝜌1,…,𝜌𝑤⟩,1≤𝑖≤𝑤. A machine state is a vector of 𝑤 closed rows. When its first row is an abstraction, one step simultaneously substitutes the current 𝑤 rows for 𝑥1,…,𝑥𝑤 in the displayed output vector. A state halts when its first row is 𝖧𝖺𝗅𝗍. The point of this intermediate syntax is that one rowing step is substitution, the operation that bounded-variable promotion and S-AllF can reproduce in subtype derivations.
At width two, put 𝑟=𝜆𝑥1,𝑥2.⟨𝑥2,𝑥1⟩. One rowing step is the visible simultaneous substitution step(⟨𝑟,𝖧𝖺𝗅𝗍⟩)=⟨𝖧𝖺𝗅𝗍,𝑟⟩. In the subtype encoding, an occurrence of 𝑥2 becomes the second bounded variable; S-Var promotes it to the type encoding the second current row, and the surrounding S-AllF reconstructs the two-component successor. Thus the substitution in this concrete row step is exactly the promotion-under-binder operation repeated by the reduction.
There is no total recursive procedure which, given a closed statement Γ⊢𝑆<:𝑇 in the sense of definition 8.28, decides its derivability for the full-𝐹<: grammar and rules fixed in section 8.7.
Proof of Theorem 8.29 — Undecidability of full F_<: subtyping; exact import
Source import. Pierce’s Theorem 10.7 proves exactly this statement. His Definition 2.2 gives the grammar 𝑋, arrow, bounded universal, and 𝖳𝗈𝗉; Figure 2 gives the six rules corresponding to reflexivity, transitivity, top, variable promotion, arrows, and S-AllF. Let R(𝑀) be his rowing-machine encoding of a two-counter-machine instance 𝑀, and let J(𝑅) be the closed full-𝐹<: statement obtained from a rowing machine after the conservative deterministic intermediate calculus is embedded into the full-𝐹<: rules of section 8.7. Sections 5–10 establish the two reductions 𝑀halts⟺R(𝑀)halts,𝑅halts⟺J(𝑅)isderivable. Their composition maps 𝑀 to J(R(𝑀)). Therefore a total subtyping decider would decide two-counter-machine halting. This is the terminal imported reduction; no stronger claim about records, bottom, inference, or implementation behavior is used here. [Pie92] ◻
Proof. By lemma 18.36, Γ⊢𝖳𝗈𝗉<:𝐶 forces 𝐶=𝖳𝗈𝗉 in the full system as well.
Induct on the given derivation. Reflexivity gives 𝐶=𝐴1→𝐴2. Rule S-Top gives the first alternative, and S-Arr gives the second with exactly its two premises. Source-variable promotion and S-AllF cannot have an arrow source. In the transitivity case, write the intermediate type as 𝑈. The induction hypothesis for 𝐴1→𝐴2<:𝑈 shows that 𝑈 is either 𝖳𝗈𝗉 or an arrow. In the first case the preliminary observation applied to 𝑈<:𝐶 gives 𝐶=𝖳𝗈𝗉. In the second, say 𝑈=𝐷1→𝐷2 with 𝐷1<:𝐴1 and 𝐴2<:𝐷2. Apply the induction hypothesis to the proper premise 𝐷1→𝐷2<:𝐶. If it gives 𝐶=𝖳𝗈𝗉, the first alternative holds. Otherwise 𝐶=𝐶1→𝐶2 with premises 𝐶1<:𝐷1 and 𝐷2<:𝐶2; two uses of transitivity give 𝐶1<:𝐴1 and 𝐴2<:𝐶2. ◻
For the term-level consequence, fix the annotated arrow fragment over full 𝐹<:. Its terms are 𝑡::=𝑥∣𝜆𝑥:𝐴.𝑡∣𝑡𝑡, its types and ordered type-bound contexts are exactly those of section 8.7, and its typing rules are T-Var, T-Lam, T-App, and T-Sub. A typechecking input is a formed type-bound context Γ, an annotated term 𝑡, and a formed target type 𝐴; the question is whether Γ⊢𝑡:𝐴 is derivable.
Proof of Lemma 18.41 — Lambda inversion in the full- arrow fragment
Proof. Prove the following stronger claim by induction on the typing derivation: if Γ,Δ⊢𝜆𝑥:𝐴.𝑡:𝐷, then either 𝐷=𝖳𝗈𝗉 or 𝐷=𝐷1→𝐷2 and some 𝐶 satisfies Γ,Δ,𝑥:𝐴⊢𝑡:𝐶,Γ⊢𝐷1<:𝐴,Γ⊢𝐶<:𝐷2. A final T-Lam gives the arrow alternative by reflexivity. In a final T-Sub, let 𝐸 be the type of its typing premise and apply the induction hypothesis there. If 𝐸=𝖳𝗈𝗉, lemma 18.36 forces the target 𝐷 to be 𝖳𝗈𝗉. Otherwise 𝐸=𝐸1→𝐸2. By lemma 18.40, the subtype premise 𝐸1→𝐸2<:𝐷 makes 𝐷 top or an arrow 𝐷1→𝐷2 with 𝐷1<:𝐸1 and 𝐸2<:𝐷2. In the arrow branch, compose these judgments with the two induction-hypothesis judgments. No other rule concludes a judgment for lambda syntax. Instantiate the stronger claim at 𝐷=𝐵1→𝐵2; the top alternative is syntactically impossible. ◻
Proof of Corollary 8.30 — Undecidability of full-F_<: typechecking
Proof. Given a well-formed subtyping statement Γ⊢𝑆<:𝑇, where 𝑆 and 𝑇 are closed relative to the supplied bound context Γ, form 𝜆𝑓:𝑇→𝖳𝗈𝗉.𝜆𝑎:𝑆.𝑓𝑎. Check this term under the type-bound context Γ and the empty term context. It has type (𝑇→𝖳𝗈𝗉)→𝑆→𝖳𝗈𝗉 exactly when the application 𝑓𝑎 can use 𝑎:𝑆 where 𝑇 is required, equivalently when Γ⊢𝑆<:𝑇. Thus a typechecker accepting an input bound context would decide subtyping. This is the reduction stated in Pierce’s Section 11. For the reverse implication, apply lemma 18.41 to the two abstractions and then invert the application, collecting any intervening subsumption chains. The function variable begins at 𝑇→𝖳𝗈𝗉; by lemma 18.40, every non-Top type at which it can be applied still has an arrow domain below 𝑇. The argument variable begins at 𝑆, so application plus transitivity yields 𝑆<:𝑇. Thus the term has type (𝑇→𝖳𝗈𝗉)→𝑆→𝖳𝗈𝗉 exactly when the original subtype statement holds. The term has no free term variables, but it may contain the type variables bound by Γ; we do not call it closed without that qualification. ◻
The Kernel measure fails at the full universal rule for a visible reason. For ∀𝑋<:𝑆1.𝑆2<:∀𝑋<:𝑇1.𝑇2,S-AllF checks the bodies under 𝑋<:𝑇1. Occurrences of 𝑋 in the source body are therefore reweighted from 1+𝑤Γ(𝑆1) to 1+𝑤Γ(𝑇1). Although the other premise gives 𝑇1<:𝑆1, the syntactic weight 𝑤Γ(𝑇1) may be arbitrarily larger than 𝑤Γ(𝑆1). Hence the body call need not decrease the Kernel query measure.
We have reached a sharp rule-level boundary. With identical quantifier bounds, the context-relative weight decreases and the Kernel procedure terminates. With contravariantly comparable bounds and rebinding by the target bound, full 𝐹<: subtyping is undecidable. This does not make bounded abstraction unusable: 𝗋𝖾𝗆𝖾𝗆𝖻𝖾𝗋𝖷 needed only the decidable Kernel rule.
It does determine what an implementation may promise. A checker can restrict itself to Kernel and return a Boolean answer; it can run a complete search for derivable full-𝐹<: judgments that may diverge on a negative query; or it can impose fuel and return a third result, unknown, when the fuel is exhausted. Treating exhaustion as “not a subtype” would turn an incomplete search into an unsound decision procedure. The optional artifact follows the third policy; its resource diagnostic is deliberately distinct from rejection.
The complete search just mentioned is a semidecision procedure: enumerate finite labeled rule trees by size and mechanically check their formation, context, and inference-rule obligations. It halts exactly on derivable queries. If the complement were also semidecidable, dovetailing the two enumerations would decide full 𝐹<:, contradicting theorem 8.29.
Sources.
Cardelli and Wegner give record/function subtyping in Section 6.1, bounded quantification in Section 6.2, and a rule appendix [CW85]. The finite-map presentation, bottom, safety proof, and Kernel algorithm above are local. Pierce fixes the minimal full-𝐹<: grammar in Definition 2.2 and Figure 2, then gives the trace (crediting the example to Giorgio Ghelli), undecidability theorem, and typechecking reduction in Example 4.1, Theorem 10.7, and Section 11 [Pie92].
Suggested first pass.
None of these problems is a prerequisite for later chapters. Begin with exercise 8.13, exercise 8.14; then use the starred problem to reconstruct the typechecking reduction in full.
★☆☆ Continue the trace for two iterations, displaying both S-AllF premises at every step. Explain why the fresh alpha-renamed binders make the contexts strictly grow.
★★☆ Use the two if-and-only-if propositions displayed in the source import. Assuming a total subtyping decider, write the three-step decision procedure for two-counter-machine halting on input 𝑀: construct R(𝑀), construct J(R(𝑀)), and invoke the decider. Justify both answers from the biconditionals, and explain why one divergent subtype search alone could not establish this undecidability result.
★★★ Given a derivable closed statement Γ⊢𝑆<:𝑇 in the sense of definition 8.28, derive Γ⊢𝜆𝑓:𝑇→𝖳𝗈𝗉.𝜆𝑎:𝑆.𝑓𝑎:(𝑇→𝖳𝗈𝗉)→𝑆→𝖳𝗈𝗉. Here Γ is the supplied mixed context, containing only type bounds in this instance; there is no second term-context zone. Mark the direct subsumption step using 𝑆<:𝑇. Conversely, recover this subtyping statement from the displayed typing by applying lemma 18.40 while inverting the application and its subsumption chains. Reconstruct the lemma’s transitivity case without looking back at its proof, and state the term’s exact closure relative to Γ.
★★★Practical project.bounded-subtyping-worklist Implement the finite Kernel worklist in artifacts/ch18-subtyping/corpus.kp. Preserve alpha-fresh universal binders and the invariant that every recursive obligation is equivalent to its source query. The accepted run must print the seven named PASS cases and All 7 subtyping corpus cases passed.; the audit must be empty. Run the four commands
kappa check artifacts/ch18-subtyping/corpus.kp
kappa test artifacts/ch18-subtyping/corpus.kp
kappa run artifacts/ch18-subtyping/corpus.kp
kappa audit artifacts/ch18-subtyping/corpus.kp
then replay the three mutations in artifacts/ch18-subtyping/README.md for arrow variance, source-bound promotion, and universal freshening. Each mutant must still typecheck and must fail the stdout oracle. The final Full-𝐹<: case is a boundary test, not a claimed decider.