OO Self Types, F-Bounds, and Matching

The type of a method may mention the type of its receiver. This is harmless until the object is extended. Then two demands pull in opposite directions. The old code should be inherited without being rechecked, while every occurrence of the receiver type in that code should now denote the extended object. Ordinary recursive subtyping can satisfy the demand when all those occurrences are covariant. A binary method puts the receiver type in an argument position and exposes the obstruction. Heuristically, a covariant recursive record body can preserve a subtype comparison through one unfolding, whereas an antitone occurrence reverses the comparison and blocks the argument. The Point/ColorPoint pair below makes that obstruction concrete in the recursive target calculus of chapter 13.

Where the receiver type changes sign

Let the functional record operators describe the two interfaces. Define $$\mathsf{Point}=\mu X.\mathsf{PointF}(X),\mathsf{ColorPoint}=\mu X.\mathsf{ColorPointF}(X).$$ Unlike the invariant primitive object components of chapter 13, these are immutable covariant records. The Point/ColorPoint comparison therefore succeeds here; the binary-method case below is the obstruction that remains. This opening calculation takes place specifically in the target calculus of definition 15.16; it is not a derivation in any of the three calculi defined later in this chapter. Its recursive-subtyping premise is the Amber-style premise, checked under . Record width and arrow covariance in the result give and hence the desired . At the more precise static type, $\mathit{move}$ returns $\mathsf{ColorPoint}$, and so does $\mathit{clone}$ applied to unit. After subsumption to $\mathsf{Point}$, they return only $\mathsf{Point}$. This loss is safe: the shorter view no longer promises color. The premise that drives proposition 15.12 is absent here: that counterexample overrides a method retained through a shorter view, while this record grammar contains no update term. Subsumption therefore changes only the static view of an immutable record.

Now add an equality-like binary method: The recursive-subtyping attempt reaches Arrow subtyping asks for , exactly the premise we do not have. Declaring the comparison covariant would be unsound. Code in the colored method may inspect its argument’s $\mathit{color}$ component, while a context that sees the receiver merely as an equality point may pass an uncolored point.

A functional calculus with hidden Self

Put the changing receiver type inside the object while hiding its exact representation from clients. The calculus is intentionally functional: records never change in place, and no store occurs in its safety theorem.

Positive families and the two Self operations

For a distinguished variable $X$, define positive and negative occurrence simultaneously. An $X$-free type has both polarities; $X$ itself is positive; records preserve polarity componentwise; and an arrow reverses it in the domain and preserves it in the codomain. Thus $X$ and $\mathsf{Nat}\to X$ are positive, whereas $X\to \mathsf{Bool}$ is negative. We do not permit a free occurrence of the distinguished $X$ beneath a nested Self binder.

Proof of Lemma 16.3 — Polarity is monotonicity

Proof. Induct on the type, proving the positive and negative statements simultaneously. The $X$ case is the given subtyping; an $X$-free type gives reflexivity. Records use fieldwise covariance. For an arrow $A(X)\to B(X)$, the induction hypothesis for the domain has the reversed orientation and the hypothesis for the codomain has the direct orientation. Arrow subtyping combines exactly those two comparisons. The negative case exchanges the two induction hypotheses. ◻

The notation in equation 16.1 does not assert equi-recursive equality. Rule T-PackSelf combines bounded-existential packaging with fold; T-UseSelf combines opening with unfold. Thus the public type $S$, hidden witness $C$, and payload type $R_S(C)$ remain distinct.

For $a:S$ and ${\ell }_j:B_j(X)$ in $R_S(X)$, define selection by where the body is subsumed from $B_j(X)$ to $B_j(S)$. This last step exists by lemma 16.3 and . The result type does not contain $X$, so the escape condition is satisfied. This is the exact point at which the positive-family condition performs work. Selection therefore has a one-line root behavior: $$(\mathsf{packSelf}C\mathsf{with}v\mathsf{as}{S}_0)\mathbf{\cdot }{\ell }_j⟼v.{\ell }_j,$$ where the step abbreviates expansion by equation 16.2 followed by (UseSelf); an ordinary projection step follows when $v$ is a record value.

Point and ColorPoint are complete packages

Define Every family is positive. Under , immutable-record width gives ; therefore S-Self derives .

The following are closed terms: For $p_0$, the recursion assumption $p:P$ types the payload at $$\mathsf{PointF}(P)=\{x:\mathsf{Nat},\mathit{clone}:\mathsf{Unit}\to P,\mathit{move}:\mathsf{Nat}\to P\}.$$ By reflexivity, , so T-PackSelf gives the body type $P$ and the recursion rule gives $p_0:P$. The derivation for $c_0:C$ has the same five steps with the additional Boolean field. It follows both that $c_0\mathbf{\cdot }\mathit{clone}:\mathsf{Unit}\to C$ and, after subsuming the receiver, that $(c_0:P)\mathbf{\cdot }\mathit{clone}:\mathsf{Unit}\to P$. Here and below $(a:A)$ is a displayed elaboration cue: it means that the term $a$ is first used at type $A$ by T-Sub. It is not an additional term constructor or reduction rule.

Put $$r_0=\{x=0,\mathit{clone}=\lambda u:\mathsf{Unit}.p_0,\mathit{move}=\lambda d:\mathsf{Nat}.p_0\}.$$ For a readable trace, abbreviate the opened clone body by Expanding the derived selection and taking one recursion step gives The (UseSelf) step substitutes the witness type $P$ for the type binder $X$, then the payload for the term binder $z$. It does not substitute the recursive term $p_0$ for $X$. The last step unfolds the returned fixpoint once; its result is a package value. Stopping at $p_0$ is useful when naming the recursive object but is not a complete call-by-value reduction.

Safety

The Self redex can be opened at a supertype of the package annotation. The proof must therefore recover the relation between the actual and expected families; merely observing that a package is present is insufficient.

Proof of Lemma 16.6 — Structural properties of Self_+

Proof. For item 1, weakening is induction on derivations after alpha-renaming every binder away from the appended declarations. For bound narrowing, the distinguished S-Bound conclusion is recovered from by transitivity; every other rule applies the induction hypotheses to its premises and restores the same rule.

For item 2, use simultaneous induction on formation, subtyping, and typing. The distinguished S-Bound case is the premise . Records apply the hypotheses fieldwise; arrows apply them contravariantly to the domain and covariantly to the codomain. In S-Self, alpha-rename the inner Self variable away from $C$, substitute in the family comparison, and restore the rule. For T-PackSelf, the required family identity is $$(R_S(D))[C/X]{=}_{\alpha }{R}_{S[C/X]}(D[C/X]),$$ after freshening the Self binder. The T-UseSelf case uses the same identity, substitutes in the scrutinee and body, and preserves the escape condition because the bound variable was chosen fresh.

For item 3, induct on typing. The distinguished variable case uses the assumed typing of the substituend; every other variable retains its declaration. Alpha-rename lambda and recursion binders away from the substituend. In T-PackSelf, substitute in the payload. In T-UseSelf, substitute independently in the scrutinee and, after freshening both binders, in the body; its result type and escape condition are unchanged. Records, applications, and conditionals apply the induction hypotheses to their immediate premises. These cases exhaust the term grammar. ◻

Proof of Lemma 27.6 — Outer-shape inversion

Proof. Prove both statements simultaneously by rule induction. Reflexivity is immediate. The arrow, record, and Self rules preserve their displayed outer constructors. Rule S-Top cannot end at any of the three target shapes. Rule S-Bound has a type variable on the left and therefore cannot be the last rule for the stated $C$.

For transitivity, write . Both premises have smaller derivation height, so both simultaneous induction hypotheses are available. For the outer-shape claim, split on whether $D$ is a type variable. If it is, the no-nonvariable-below-variable hypothesis applied to contradicts the assumption that $C$ is not a variable. If it is not, the outer-shape hypothesis applied to gives $D$ the outer constructor of $A$; applying it once more to gives $C$ that constructor.

For the no-nonvariable-below-variable claim, the target is a variable $X$. Again split on $D$. If $D$ is a variable, the hypothesis for is a contradiction. If $D$ is not a variable, the hypothesis for is a contradiction. These two splits also cover $D=\mathsf{Top}$, which lies in the nonvariable branch; no unproved outer-shape assertion about the intermediate is required. ◻

Proof of Lemma 16.7 — Self-subtyping inversion

Proof. Induct on the subtyping derivation. Reflexivity gives , and S-Self has the required family comparison as its premise. In a transitive derivation with Self type at both ends, the shape claim gives $C{=}_{\alpha }\mathsf{Self}X.R_1(X)$. The two induction hypotheses give and under ; transitivity gives the required comparison. Lemma 27.6 excludes a type-variable intermediate and gives the Self outer shape directly; in particular, no derivation can return from $\mathsf{Top}$, an arrow, or a record to a Self type. ◻

Proof of Lemma 16.8 — Canonical forms

Proof. Strip final subsumption rules. The remaining value-introduction type is not a type variable, so lemma 27.6 applies to the accumulated subtype chain. At arrow type it forces an arrow introduction; the only such value rule is T-Abs, and inversion returns $v=\lambda x:C.a$. At record type it forces T-Record, which returns a record value with one typed field for every label in the conclusion. At Self type it forces T-PackSelf; lemma 16.7 gives , and inversion of T-PackSelf gives and $w:R_0(C)$. ◻

Proof of Theorem 16.9 — Preservation

Proof. Induct on the reduction derivation. Compatible cases rebuild their typing rule after applying the induction hypothesis to the active subterm. Beta and recursion use term substitution. Record projection and the ground roots follow by inversion.

It remains to prove the generalized (UseSelf) root. Suppose the actual package annotation is $S_0=\mathsf{Self}X.R_0(X)$, while the use is checked at $S=\mathsf{Self}X.R(X)$. Typing inversion through final subsumption is an induction on the typing derivation: T-PackSelf gives the witness and payload judgments, and each T-Sub composes one more subtype step. Hence By lemma 16.7, . Type substitution with the well-formed type $C$ gives , so subsumption yields $v:R(C)$. The body premise is Since , type substitution gives $\mathrm{\Delta };\mathrm{\Gamma },x:R(C)⊢b[C/X]:D$. Term substitution then gives $\mathrm{\Delta };\mathrm{\Gamma }⊢b[C/X][v/x]:D$, precisely the reduct. Thus the actual hidden witness, not the public annotation, controls the contraction. ◻

Proof of Theorem 16.10 — Progress and functional safety

Proof. Induct on typing after removing final subsumption. Variables are impossible in the empty term context. Introduction forms are values after their left-to-right subterms become values. For application, the function steps, the argument steps, or lemma 16.8 proves that the function is a lambda and beta applies. The conditional and projection cases use the Boolean and record canonical forms. A recursion term always unfolds.

For $\mathsf{useSelf}a\mathsf{as}\cdots$, the induction hypothesis says that $a$ steps or is a value. In the latter case, the Self canonical form proves that $a$ is an actual package, so (UseSelf) applies even when its annotation is a proper subtype of the type expected by the use. These cases exhaust the grammar. Preservation keeps the same type along every finite reduction sequence, and progress applies to its last term. ◻

Why negative Self is rejected

The family $$\mathsf{BadEq}(X)=\{x:\mathsf{Nat},\mathit{eq}:X\to \mathsf{Bool}\}$$ does not form a ${\mathsf{Self}}_{+}$ type. To see the operational reason, consider the hypothetical calculus obtained by deleting only the positivity check. Put The record-family premise of S-Self would indeed compare the two same-parameter fields ; width would then give . That pointwise width calculation is not the error. The error is using the hidden bound at selection time to turn $X\to \mathsf{Bool}$ into $P_E\to \mathsf{Bool}$. Arrow subtyping gives the opposite comparison, and supplies no such coercion.

If the bad coercion is inserted, the closed term $$e_E:=((c_E:P_E)\mathbf{\cdot }\mathit{eq})p_E:\mathsf{Bool}$$ has the following reduction. Expanding the first derived selection and opening the colored package yields The last term is neither a value nor a redex. The displayed packages show that the failure is not merely a failed proof of preservation. Rejecting the negative occurrence rules this stuck program out; admitting it would type the program just reduced.

Primitive covariant Self therefore handles clone-like and other self-returning methods. It does not handle a binary method whose argument was obtained independently of the receiver. Inside one open package, a method can consume another value of the same hidden witness if one is available; two separately opened packages need not choose the same witness. Matching addresses inheritance of such code by changing the relation on the one-step record families, not by weakening this safety condition.

F-bounds describe fluent code

The failed subtype judgment does not prevent us from writing one piece of code for every type that supports the same chain of methods returning that type; this is the sense of fluent used here. The bound must mention the type being bounded. This section changes calculi. Its recursive types are equi-recursive comparison types, not the iso-recursive package expansion of equation 16.1. Here equi-recursive means that a recursive type and its one-step unfolding are definitionally equal. No term-level fold or unfold is required; iso-recursive types instead keep the two types distinct and cross between them with explicit terms, as in chapter 12.

The calculus validates formation, typing of the displayed clients, and preservation of the type-application root. Equality and subtyping of its equi-recursive types are declarative here.

Call a type $C$ a post-fixpoint of $F$ when . Equi-recursive conversion proves concrete inequalities , and an F-bound says which of them may instantiate a given client. Neither choice adds a primitive Self package.

Put Under , subsumption gives $p:\mathsf{PointF}(X)$, hence $p.\mathit{move}:\mathsf{Nat}\to X$. Thus Any type $C$ satisfying may instantiate this term, and the result remains $C$. This is the fluent use of an F-bound.

Here is a concrete legal instantiation. Define $${\mathsf{Point}}_{\mathrm{eq}}:=\mu X.\mathsf{PointF}(X).$$ The two separate judgments needed are then available: Therefore F-Elim derives $$\mathit{moveAll}[{\mathsf{Point}}_{\mathrm{eq}}]:{\mathsf{Point}}_{\mathrm{eq}}\to \mathsf{Nat}\to {\mathsf{Point}}_{\mathrm{eq}}.$$ This derivation would be incomplete in an iso-recursive calculus: there an explicit term fold cannot be replaced by a subtype premise. The familiar Java pattern $T\mathsf{extends}\mathsf{Comparable}⟨T⟩$ has the same F-bound shape: the client chooses one $T$, and the bound mentions that very $T$ in its protocol.

Proof of Lemma 16.12 — F-bound instantiation

Proof. Induct simultaneously on formation, subtyping, and typing. The distinguished bound-variable case is exactly the assumption . In an arrow, record, or application rule, substitute in every premise and restore the same rule. At a nested type binder, alpha-rename it away from $C$, apply the induction hypothesis, and restore the binder. The term-variable cases merely substitute in their declared types.

For equi-recursive conversion, choose the recursive binder $Y$ distinct from $X$ and fresh for $C$. Substitution commutes with unfolding by the composition equation $$(A[\mu Y.A/Y])[C/X]{=}_{\alpha }A[C/X][\mu Y.A[C/X]/Y],$$ same binder-fresh induction as lemma 24.2. The induction is rerun for the ${\mathsf{F}}_{\mathrm{eq}}$ grammar: records, bounded quantifiers, and their term annotations add componentwise congruence cases. Thus a converted premise remains definitionally equal to the substituted conclusion; the congruence cases commute homomorphically with substitution. Applying the result to the premise of F-Intro gives the type of $a[C/X]$, which is the reduct. ◻

F-bounds can also type a homogeneous binary operation. With $$\mathsf{EqF}(X):=\{x:\mathsf{Nat},\mathit{eq}:X\to \mathsf{Bool}\},$$ the term has type . The two arguments have one chosen type $X$, so the contravariant occurrence causes no coercion. What F-bounded quantification does not prove is substitutability between the recursive binary-method types Unfolding a proposed subtype comparison reverses the equality-method domain and asks for , which record width cannot supply. F-bounds parameterize the client; they do not turn protocol extension into subsumption.

What an F-bound forgets about a Self package

For this comparison, let $R$ range only over the positive families generated by the common grammar Only $X$ may occur free. There is no primitive Self, recursive type, or bounded quantifier inside an $L$. The outer record makes $R$ contractive, so the same $R$ is legal in ${\mathsf{Self}}_{+}$ and beneath $\mu$ in ${\mathsf{F}}_{\mathrm{eq}}$.

The two calculi agree on one construction and part company on another. For such a family $R$, form $$S=\mathsf{Self}X.R(X),\hat{S}=\mu X.R(X)\text{in }{\mathsf{F}}_{\mathrm{eq}}.$$ On the F-bounded side, a record at the public witness $\hat{S}$ has payload type $R(\hat{S})=\hat{S}$, so it is a legal post-fixpoint. An F-bounded client may therefore be instantiated at $\hat{S}$. This is the public-witness fragment of primitive Self.

The general T-PackSelf premise is different: Erasing this package to $\hat{S}$ would require a term of $R(\hat{S})$. The payload premise has type $R(C)$, not $R(\hat{S})$; moreover the package deliberately hides $C$. Revealing that witness, or replacing it everywhere by $\hat{S}$, destroys the representation abstraction implemented by the bounded existential. Thus the public-witness construction is not a rulewise translation of primitive Self.

The converse comparison loses a different property. An F-bounded client may quantify over the negative family $\mathsf{EqF}$, because it assumes one homogeneous type $X$ and performs no coercion between distinct post-fixpoints. Primitive ${\mathsf{Self}}_{+}$ admits first-class packages and covariant package subsumption, but rejects that negative family. Hence neither presentation contains the other: F-bounds lose hidden-witness packaging, while the positive Self calculus deliberately gives up binary Self selection.

Proof of Proposition 21.12 — Boundary of the public-witness comparison

Proof. The first assertion is equation 21.3 followed by reflexivity and F-Elim. For the second, take the legal package of example 27.13, with hidden witness . Its only payload judgment is $c:R(C)$. Positivity can transport a payload along a proved subtype , but the package premise is , where $S$ is a ${\mathsf{Self}}_{+}$ type and $\hat{S}$ is an ${\mathsf{F}}_{\mathrm{eq}}$ type. No judgment form of either calculus contains types from both grammars, so no rule relates these two types. Consequently the required transport is absent. Adding it would expose precisely the representation relation that the existential hides. ◻

Matching is protocol extension, not subtyping

Matching compares object types by their protocols before the recursive knot is tied. We make that sentence literal in a small higher-order target. The target is fixed here because a translation into an unnamed higher-kinded language would not be a theorem.

The ordinary target rules have an immediate complete use before the operator translation begins. Put $R=\{n:\mathsf{Nat}\}$. Under $x:\mathsf{Nat}$, its lines are Match abstraction uses T-AllOp-I, bounded instantiation uses T-AllOp-E, and exposure of a recursive protocol uses T-Unfold.

The translation has exactly the following source domain. Source protocols and their target images use the same Self-free family grammar Every $R$ is contractive in $Z$. The remaining source grammar is Source contexts are $$\mathrm{\Xi }::=\cdot \mid \mathrm{\Xi },X\mathrm{\#}O,\mathrm{\Gamma }::=\cdot \mid \mathrm{\Gamma },x:D.$$ In $X\mathrm{\#}O$, the binder $X$ ranges over types whose protocols extend the protocol of $O$; instantiation substitutes only for this match-bound variable. The recursive binder of a concrete protocol remains the separate variable $Z$ in $\mu Z.R(Z)$. The matching assumption does not assert . The judgment $\mathrm{\Xi };\mathrm{\Gamma }⊢t:D$ is generated by

$x:D\in \mathrm{\Gamma }$

$\mathrm{\Xi };\mathrm{\Gamma }⊢x:D$

$\mathrm{\Xi };\mathrm{\Gamma },x:D⊢t:E$

$\mathrm{\Xi };\mathrm{\Gamma }⊢\lambda x:D.t:D\to E$

$\mathrm{\Xi };\mathrm{\Gamma }⊢t:D\to E$$\mathrm{\Xi };\mathrm{\Gamma }⊢u:D$

$\mathrm{\Xi };\mathrm{\Gamma }⊢tu:E$

$\mathrm{\Xi },X\mathrm{\#}O;\mathrm{\Gamma }⊢t:D$

$\mathrm{\Xi };\mathrm{\Gamma }⊢\mathrm{\Lambda }X\mathrm{\#}O.t:\mathrm{\forall }X\mathrm{\#}O.D$

$\mathrm{\Xi };\mathrm{\Gamma }⊢t:\mathrm{\forall }X\mathrm{\#}O.D$$\mathrm{\Xi }⊢C\mathrm{\#}O$

$\mathrm{\Xi };\mathrm{\Gamma }⊢t[C]:D[C/X]$

$X\mathrm{\#}\mu Z.R(Z)\in \mathrm{\Xi }$$x:X\in \mathrm{\Gamma }$$R(X)(\ell )=D$

$\mathrm{\Xi };\mathrm{\Gamma }⊢x.\ell :D$

Here $R(X)(\ell )=D$ means that the record protocol $R(X)$ contains the field $\ell :D$. Thus selection is admitted only when the receiver is a match-bound variable and the bound protocol displays the label. The source fragment has no object constructor, so theorem 16.15 covers protocol-polymorphic client code only. The target fold below constructs an example target object; it is not the translation of any source literal.

Proof of Proposition 16.14 — Reflexivity and transitivity of matching

Proof. The translated operators have kind $\ast \Rightarrow \ast$. Operator reflexivity gives $\mathrm{Oper}(A)⪯\mathrm{Oper}(A)$, including the case $A=X$, where this is ${\mathrm{\Phi }}_X⪯{\mathrm{\Phi }}_X$. For transitivity, compose the two translated operator judgments using transitivity in ${\mathsf{H}}_{\mu }$. No value-typing judgment occurs in either proof. ◻

Consider the source types Their translated operators are The target fold rule now constructs an actual object. Put $$r_{max}=\{n=0,\mathit{max}=\lambda q:\mu \mathsf{MaxOp}.q\}.$$ The annotated lambda has type $\mu \mathsf{MaxOp}\to \mu \mathsf{MaxOp}$, hence $$r_{max}:\mathsf{MaxOp}(\mu \mathsf{MaxOp}),m_{max}:={\mathsf{fold}}_{\mathsf{MaxOp}}(r_{max}):\mu \mathsf{MaxOp}.$$ Since $r_{max}$ is a value, the explicit destructor computes: $${\mathsf{unfold}}_{\mathsf{MaxOp}}(m_{max})⟼r_{max}.$$ For arbitrary $Z:\ast$, record width gives Thus S-OpPoint derives $\mathsf{MinMaxOp}⪯\mathsf{MaxOp}$, and hence $\mathsf{MinMax}\mathrm{\#}\mathsf{Max}$. Recursive subtyping would instead compare $X\to X$ with $Y\to Y$ under only , and fail at the contravariant premise.

Now suppose ${\mathrm{\Phi }}_X⪯\mathsf{MaxOp}$ and put $X^{†}=\mu {\mathrm{\Phi }}_X$, consistently with definition 16.13. The field derivation keeps typing and subtyping as separate judgments: Consequently the translated client is It can be instantiated with $\mathsf{MaxOp}$ or $\mathsf{MinMaxOp}$. In the second case both arguments and the result have type $\mu \mathsf{MinMaxOp}$; no value is coerced to $\mu \mathsf{MaxOp}$. For an end-to-end target calculation, instantiate at $\mathsf{MaxOp}$ and use the object constructed above: Inside the first multistep, the translated client unfolds its first argument, selects $\mathit{max}$, and applies $\lambda q.q$ to the second argument. Thus the protocol-polymorphic client and the target object compute together, not merely in separate typing derivations.

Proof of Theorem 16.15 — Soundness of the operator reading

Proof. For item 1, induct on $O$. A variable uses its translated context declaration. For $\mu Z.R(Z)$, translate each field type under $Z:\ast$, apply K-OpAbs, use the source contractiveness condition, and apply K-Mu. A bound extends the context only after the operator on its right has been checked, so bounded operator formation applies from left to right.

For item 2, match abstraction translates to T-AllOp-I. If $C\mathrm{\#}O$, the definition of matching gives $\mathrm{Oper}(C)⪯\mathrm{Oper}(O)$, exactly the second subtyping premise of T-AllOp-E; item 1 proves that both operators have kind $\ast \Rightarrow \ast$ and are contractive. Finally, if the source bound exposes a field $\ell :L(X)$, T-Unfold gives the payload type ${\mathrm{\Phi }}_X(\mu {\mathrm{\Phi }}_X)$; S-OpApp instantiates the operator bound at $\mu {\mathrm{\Phi }}_X$; term subsumption gives the protocol record; projection gives $L^{†}(\mu {\mathrm{\Phi }}_X)$. These are precisely the four judgments displayed above for $\mathit{max}$. No source subsumption rule has been used. ◻

The two interpretations do not coincide

In the equi-recursive comparison calculus, the tempting first-order reading is It explains the $\mathit{moveAll}$ and homogeneous $\mathit{preMax}$ examples. It does not translate a cascading bound $\mathrm{\forall }X\mathrm{\#}A.\mathrm{\forall }Y\mathrm{\#}X.D$, because an ordinary type variable $X$ has no syntactically determined $\mathrm{Oper}(X)$. Worse, its induced relation is not transitive in general. For example, with use the following abbreviations for the one-step body and matching test: This is meta-level substitution inside ${\mathsf{F}}_{\mathrm{eq}}$, not the matching translation $\mathrm{Oper}(-)$ of definition 16.13. The three calculations are The first holds after unfolding $A$ and dropping $q$; the second holds after unfolding $B$. The third would require , hence , but unfolded $B$ lacks $q$. It therefore fails. More sharply, equi-recursive conversion gives $$D=\{p:B\to \mathsf{Nat}\}=B.$$ Thus ${\mathrm{\#}}_{\mathrm{eq}}$ is not even well defined on equi-recursive types: replacing $B$ by the definitionally equal $D$ changes the answer. On fixed presentations the preceding calculations also exhibit the attempted transitivity failure. Neither defect is a failure of ordinary subtype transitivity.

The higher-order reading instead translates $$\mathrm{\forall }X\mathrm{\#}A.D(X)\text{to}\mathrm{\forall }{\mathrm{\Phi }}_X⪯\mathrm{Oper}(A).D(\mu {\mathrm{\Phi }}_X).$$ It retains the protocol as an operator, so a second bound may compare a new operator with ${\mathrm{\Phi }}_X$. Reflexivity and transitivity are then inherited from pointwise operator subtyping. The price is explicit higher-kinded abstraction and explicit fold/unfold at terms. The source paper discusses a broader interpretation, but theorem 16.15 proves only the displayed restricted fragment; no end-to-end theorem is imported.

Finer boundary: mutation needs a store theorem

Theorem 16.9, Theorem 16.10 quantify over the heap-free ${\mathsf{Self}}_{+}$ dynamics, so it has no alias invariant. To state the mutation boundary, extend ${\mathsf{Self}}_{+}$ with $\mathsf{Ref}A$, location values $\ell$, and terms $\mathsf{ref}a$, $!a$, and $a:=b$. Reference types are invariant: the only subtyping between $\mathsf{Ref}A$ and $\mathsf{Ref}B$ comes from $A=B$. Extend the polarity grammar by declaring $\mathsf{Ref}A$ positive or negative in $X$ only when $X\notin \mathsf{FV}(A)$. Correspondingly, extend the value grammar by $v::=\cdots \mid \ell$. The typing rules are

$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢a:A$

$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢\mathsf{ref}a:\mathsf{Ref}A$

$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢a:\mathsf{Ref}A$

$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢!a:A$

$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢a:\mathsf{Ref}A$$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢b:A$

$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢a:=b:\mathsf{Unit}$

$\mathrm{\Sigma }(\ell )=A$

$\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢\ell :\mathsf{Ref}A$

The uniform judgment is $\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢a:A$: $\mathrm{\Delta }$ contains type-variable bounds, $\mathrm{\Sigma }$ assigns closed types to locations, and $\mathrm{\Gamma }$ assigns types to term variables. Every functional rule is lifted by carrying the same $\mathrm{\Sigma }$ through its premises.

A store $\sigma$ maps locations to closed values. Its invariant is $$\mathrm{\Sigma }\vDash \sigma ⟺\mathrm{dom}(\mathrm{\Sigma })=\mathrm{dom}(\sigma )\text{and}\cdot ;\mathrm{\Sigma };\cdot ⊢\sigma (\ell ):\mathrm{\Sigma }(\ell )\text{for every }\ell .$$ Later the chapter also writes $\sigma {\vDash }_{n}W$ for semantic heap satisfaction and $\gamma {\vDash }_{\theta ,W}^n\mathrm{\Gamma }$ for semantic environment satisfaction. The three source macros $\vDash$, $\vDash$, and $\vDash$ deliberately print the same relation glyph, but their arguments identify the judgment: store typing has $\mathrm{\Sigma }$ on the left and $\sigma$ on the right; heap satisfaction has $\sigma$ on the left and carries an index; environment satisfaction has $\gamma$ on the left and carries both closing data and an index. Configuration reduction adds the roots Besides the contexts of definition 16.5, configuration reduction uses $$E::=\cdots \mid \mathsf{ref}E\mid !E\mid E:=a\mid \ell :=E.$$ Thus the location and then the assigned value are evaluated before assignment contracts.

Proof of Lemma 27.19 — Store-typing weakening

Proof. The typing statement is induction on the derivation. Rule T-Loc uses preservation of old bindings; every other rule restores its conclusion after applying the induction hypotheses. For the store statement, the new domains agree, the fresh cell has the assumed type, and the old cells retain their types by the typing statement. ◻

Proof of Theorem 21.17 — Configuration preservation

Proof. Induct on the configuration reduction. For allocation, inversion gives $v:A_0$. Choose fresh $\ell$, set ${\mathrm{\Sigma }}^{\prime }=\mathrm{\Sigma },\ell :A_0$, and use T-Loc for the result. The new store clause and all old clauses follow from lemma 27.19.

For dereference, typing and reference canonical forms give $\mathrm{\Sigma }(\ell )=A_0$. The store invariant gives $\cdot ;\mathrm{\Sigma };\cdot ⊢\sigma (\ell ):A_0$, which is the type of the reduct. For assignment, inversion gives $v:A_0$ at the same invariant cell type $\mathrm{\Sigma }(\ell )=A_0$. Replacing only $\sigma (\ell )$ therefore preserves every clause of equation 16.3; the result is unit.

In a context step, the induction hypothesis gives ${\mathrm{\Sigma }}^{\prime }\supseteq \mathrm{\Sigma }$. Lemma 27.19 retypes the inactive subterms and the context’s typing rule is rebuilt. This covers $\mathsf{ref}E$, $!E$, $E:=a$, $\ell :=E$, and every functional context in definition 16.5.

The functional roots leave the store fixed. Beta and recursion use term substitution. Projection and ground computation use typing inversion. For a generalized Self-open root, write the runtime annotation as $S_0=\mathsf{Self}X.R_0(X)$ and the expected annotation as $S=\mathsf{Self}X.R(X)$. Inversion gives Self-subtyping inversion and type substitution give ; subsumption gives $v:R(C)$. Substituting $C$ for the escaping-free $X$, then $v$ for $x$, types $b[C/X][v/x]:D$. Thus the store theorem contains its own Self-open case rather than importing the functional conclusion. ◻

Proof of Theorem 21.18 — Configuration progress

Proof. Induct on typing after stripping final subsumption. The functional cases follow the same canonical-form analysis as theorem 16.10: a function value is a lambda, a record value has the projected field, a Self value is a package, and a fixpoint always unfolds. These facts are reproved under $\mathrm{\Sigma }$ by induction on value typing; locations add no inhabitant of an arrow, record, or Self type.

For $\mathsf{ref}a$, either $a$ steps in the allocation context or it is a value and the fresh-location root applies. For $!a$, either $a$ steps or reference canonical forms give a location $\ell$. Its typing says $\ell \in \mathrm{dom}(\mathrm{\Sigma })$, and the store invariant equates the domains, so the dereference root applies. Assignment first steps its left term, then its right term; when both are values, the left is a location in the store and the assignment root applies. These cases exhaust the extended grammar. ◻

Proof of Corollary 21.19 — Syntactic state safety

Proof. Iterate theorem 21.17; apply theorem 21.18 to the last configuration. ◻

For a small aliasing calculation, put $$K=\mathsf{Self}X.\{\mathit{contents}:\mathsf{Ref}\mathsf{Nat},\mathit{set}:\mathsf{Nat}\to X\}.$$ After allocating $r=\mathsf{ref}0$, define The family is positive in $X$, and $\mathsf{Ref}\mathsf{Nat}$ is independent of $X$. The following trace is a concrete instance of the preservation and progress theorems. Allocation gives $$⟨\cdot ,\mathsf{ref}0⟩⟼⟨\{\ell \mapsto 0\},\ell ⟩,{\mathrm{\Sigma }}_1=\{\ell :\mathsf{Nat}\},{\mathrm{\Sigma }}_1\vDash \{\ell \mapsto 0\}.$$ Write $k_{\ell }$ for the displayed package with $r=\ell$. We write that same package twice, $a_1:=k_{\ell }$ and $a_2:=k_{\ell }$, only to mark its two use sites; both aliases contain the same location $\ell$. The term $$B_2:=\lambda u:K.!(a_2\mathbf{\cdot }\mathit{contents}):K\to \mathsf{Nat},e_{12}:=B_2((a_1\mathbf{\cdot }\mathit{set})7):\mathsf{Nat}.$$ has the configuration trace The first multi-step opens $a_1$ and selects $\mathit{set}$. The first displayed root is assignment; then beta returns the exact receiver. The outer beta deliberately discards its parameter $u$; opening $a_2$ selects the same location, and dereference reads $7$. Both stores satisfy ${\mathrm{\Sigma }}_1$ because their sole contents have type $\mathsf{Nat}$. An attempted update $\ell :=\mathsf{true}$ is rejected by T-Assign before reduction.

A field $\mathsf{Ref}X$ would be invariant in $X$, not positive, and is therefore outside S-Self. The fragment therefore models objects that share cells of receiver-independent data, such as counters, flags, and handles. It cannot directly model a mutable linked structure whose cell stores another value of the exact receiver type; that requires a richer invariant or guarded treatment of $\mathsf{Ref}X$.

A step-indexed model for Self with references

The unindexed semantic-world attempt is circular. If a world stores the semantic promise at each location, $$W(\ell )=\mathcal{V}[[A{]]}_{\theta }(W),$$ then defining the value relation already quantifies over worlds whose entries are instances of that same, not-yet-defined relation. There is no smaller type or world on the recursive call. Two repairs break the cycle: worlds store closed syntactic types rather than predicates, and interpreting a stored type may appeal only at a strictly smaller natural-number index.

The syntactic theorem tracks a type at each location. The semantic model tracks the behavior promised by that type at every smaller number of future steps. This second proof is independent of the functional proof and of the equi-recursive comparison calculus.

A step index $n$ is a natural-number budget: a claim at $n$ may appeal recursively only to claims at smaller budgets. A world records the closed type promised by every allocated location, and a later world may add locations without changing old promises. A logical relation interprets each type as the values and expressions that honor those promises; heap satisfaction says that the current store realizes its world’s promises. The strict decrease in $n$ breaks the circularity among recursive Self values, references, and heaps. The earlier syntactic theorem already proves no-stuck safety for closed programs. This second theorem is not needed to repeat that conclusion; it additionally validates the open-term substitution principle and the recursive semantic interpretation used for aliasing.

Proof of Lemma 21.22 — Closing substitution and semantic subtyping

Proof. The first judgment is simultaneous closing substitution on formation and subtyping. In the distinguished bound case, it is exactly the premise in the definition of a respecting substitution. Arrow, record, and Self rules apply the induction hypotheses; binders are alpha-renamed before substitution.

For the semantic inclusion, induct on subtyping. The ground cases are reflexive and $\mathsf{Top}$ contains every closed value. Records discard fields. Arrows reverse the domain inclusion and preserve the codomain inclusion. References have no nonreflexive structural subtyping. In the Self case, a package admitted on the left has a closed annotation ; closing the rule premise gives . Transitivity gives , so the same witness and smaller-index payload satisfy equation 21.6 on the right. The expression inclusion replaces the last value membership in equation Term. Downward closure is induction in the lexicographic measure $(n,|A|,\rho )$ of definition 21.21; record clauses use the smaller type, arrow and Self clauses use the smaller index, and the expression clause uses the smaller phase when its residual index is unchanged. World monotonicity is proved in the same induction and uses exact agreement on old syntactic bindings, especially in equation 21.5. ◻

Proof of Lemma 27.26 — Expression anti-reduction

Proof. Take a test at $j\le n+1$. The reducible term $a$ cannot satisfy the irreducibility premise in zero steps. Every terminating test therefore first takes the displayed root and has at most $j-1\le n$ steps left. Downward closure places $a^{\prime }$ at index $j-1$; applying its expression clause to the residual trace yields heap satisfaction and value membership at exactly the required residual index. ◻

Proof of Lemma 27.27 — Compatibility of the reference forms

Proof. Fix a future-world and heap test. For allocation, the premise runs the initializer to a related value $v$. Extend the world and heap by a fresh $\ell \mapsto A\theta$ and $\ell \mapsto v$. Downward closure supplies the cell invariant at every smaller residual index, and equation 21.5 relates the returned location.

For dereference, the premise runs to a location $\ell$. Its reference clause gives $W(\ell )=A\theta$, and heap satisfaction supplies the stored value at every smaller index consumed by the dereference root. For assignment, run the left expression to such an $\ell$, then the right expression to a related value. Replacing the cell preserves every other heap clause and the exact type at $\ell$; the root returns $\mathsf{unit}$. In each case the sum of the premise steps and the one root step is the tested budget, so the residual index in equation Term is unchanged. ◻

Proof of Theorem 21.23 — Fundamental theorem for the imperative Self fragment

Proof. Base forms. Use outer induction on $n$, and inside it induction on the typing derivation. At index zero the expression relation has no test. Variables use the expression-related $\gamma$. Records, projection, conditionals, and ground operations use their displayed value clauses. Subsumption uses lemma 21.22.

Functions. For abstraction, take , a future world $W^{\prime }⪰W$, and an argument $v\in \mathcal{V}[[A{]]}_{\theta }(W^{\prime },j)$. Downward closure and world monotonicity give $\gamma {\vDash }_{\theta ,W^{\prime }}^j\mathrm{\Gamma }$; a related value is also a related expression, so extending by $x\mapsto v$ satisfies $\mathrm{\Gamma },x:A$ there. Moreover, future-world stability gives $W^{\prime }⊩\mathrm{\Sigma }\theta$. Apply the outer index hypothesis at $j$ to the body derivation. This is not the inner derivation hypothesis at index $n$. Its conclusion is the arrow-clause obligation. Application composes the arrow and expression clauses.

Recursion. The recursion case is the reason for the order of induction. Let $f=\mathsf{fix}x:A\theta .a\theta \gamma$. To prove $f\in \mathcal{E}[[A{]]}_{\theta }(W,n)$, consider a test at $j\le n$. The term $f$ is reducible, and its first step is $$f⟼(a\theta \gamma )[f/x].$$ At the smaller index , the outer induction hypothesis applied to the T-Fix derivation gives $f\in \mathcal{E}[[A{]]}_{\theta }(W^{\prime },j-1)$. Hence $\gamma [x\mapsto f]$ satisfies the body context at that index. Apply the outer hypothesis again, now to the body derivation $\mathrm{\Gamma },x:A⊢a:A$. Its conclusion relates the displayed reduct, and lemma 27.26 absorbs the initial step. This proves fix compatibility without assuming the result at the same index.

Self packages. For T-PackSelf, closing substitution first gives . The inner induction hypothesis places the payload expression in $\mathcal{E}[[R(C){]]}_{\theta }(W,n)$, where $R(C)\theta =R\theta (C\theta )$. Consider any irreducible trace of the whole package. The evaluation context $\mathsf{packSelf}C\theta \mathsf{with}E\mathsf{as}S\theta$ runs the payload to a value $v$; a package with a reducible payload is not irreducible. The payload expression clause supplies $$v\in \mathcal{V}[[R\theta (C\theta ){]]}_{\cdot }(W^{\prime },q)$$ at the residual index $q$. Downward closure supplies the same membership at every . Hence the resulting package value, annotated by the closed type $S\theta$, satisfies equation 21.6 by reflexivity and the closed witness premise. This proves expression membership for the package; it does not treat a reducible payload as a value-related one.

Self opening. For T-UseSelf, fix a test at index $j$ and run the related scrutinee for $r$ steps until it produces $$\mathsf{packSelf}C\mathsf{with}v\mathsf{as}{S}_0.$$ The Self value clause gives and $v\in \mathcal{V}[[R_0(C){]]}_{\cdot }$ at every remaining smaller index. Self-subtyping inversion, with binders alpha-renamed to agree, gives Closing this judgment by $[C/X]$ gives , so semantic subtyping relates the actual payload at the family expected by the body. Extend the closing substitution by $X\mapsto C$; it respects because . After the Self-open root the body has budget $$q=j-r-1.$$ If its residual trace has $s$ steps, the original test has The Self value clause supplies the payload at . Extend $\gamma$ by $x\mapsto v$, apply the outer index hypothesis at $q$ to the body, and use $X\notin \mathsf{FV}(D)$ to remove the extension from the result type. This is the closing type substitution performed by the operational Self-open root.

References and worlds. The allocation, dereference, and assignment cases apply the three clauses of lemma 27.27 to their induction hypotheses. The construction in that lemma extends $W$ only for allocation, so it also preserves $W⊩\mathrm{\Sigma }\theta$.

Representative compatible contexts. For application, split a terminating trace into $r_1$ steps evaluating the function to a related lambda, $r_2$ steps evaluating the argument to a related value, one beta step, and $r_3$ body steps. If the test starts at $j$, put $q=j-r_1$ and $s=q-r_2$. From the displayed inequality and the definitions of $q,s$ give . The arrow value clause may therefore be instantiated at $s-1$ in the current future world; its expression conclusion handles the $r_3$-step body trace and returns index $j-(r_1+r_2+1+r_3)$.

For projection, split $r$ receiver steps from the one projection root. The record value clause relates the selected field at index $j-r$; downward closure places it at $j-r-1$, the index left by the root. For record construction, induct on the ordered field list. If the active field consumes $r_i$ steps, subtract $r_i$ from the current budget, use its expression hypothesis at that residual index, and use downward closure for every already evaluated field; the list induction preserves the invariant that the sum of the consumed field budgets plus the remaining budget is $j$. For a conditional, split $r$ guard steps from its one branch-selection root. Canonical forms makes the guard either $\mathsf{true}$ or $\mathsf{false}$; choose exactly the corresponding branch hypothesis at index $j-r-1$, leaving the unchosen branch unused. Self-package and Self-open contexts use the explicit arguments above. The reference contexts are precisely lemma 27.27. These are all evaluation contexts in the grammar, so the future-world quantifier composes the induction hypotheses without an unexamined context case. ◻

Proof of Corollary 21.24 — Semantic state safety

Proof. Apply theorem 21.23 with empty substitutions at index $k+1$, and use equation Term with the given heap. It produces an extending world $W^{\prime }$ for which $a^{\prime }\in \mathcal{V}[[A{]]}_{\cdot }(W^{\prime },1)$. Every defining clause of $\mathcal{V}[[A{]]}_{\cdot }$ contains only syntactic values: ground constants, lambdas, record values, locations, or Self packages with value payloads. Hence $a^{\prime }$ is a value. ◻

The boundaries between the three self mechanisms

Sources.

The expansion , its pack/use operations, the covariance derivation, the covariant-method-family condition, and the moving point and binary-method boundary are in Abadi and Cardelli, A Theory of Primitive Objects: Second-Order Systems, Sections 3.4 and 4.1–4.2, author-preprint PDF pp. 9–16, especially the rules on printed pp. 10–14. Its semantics is functional; the recoup invariant and the limit on overriding Self-returning methods are on printed pp. 17–19 [AC95]. The Point/ColorPoint argument-specialization failure and the distinction between binary-method typing and privileged representation access are developed in Bruce et al., On Binary Methods, file-PDF pp. 4–7. Its matching treatment is at file-PDF pp. 10–13; the archive cover precedes the article [BCC^+95].

The definition of matching, the statement that it grants no subsumption, and the $\mathsf{Max}/\mathsf{MinMax}$ derivation occur in Abadi and Cardelli, On Subtyping and Matching, printed pp. 6–10. F-bounded quantification and its post-fixpoint interpretation are on printed pp. 12–13. The F-bounded failures of cascading bounds, reflexivity, and transitivity are on printed pp. 16–18. The higher-order translation, its reflexivity and transitivity, and its fold/unfold field derivation are on printed pp. 18–21. That source promises a rigorous full translation but gives no end-to-end proof [AC96a]; theorem 16.15 is restricted to the displayed clauses. Definition 21.20, Definition 21.21 instead give a local step-indexed model and safety proof for this reference-and-Self fragment.

Suggested first pass.

Begin with exercise 16.10, exercise 16.11, exercise 16.12; then use the remaining problems to reconstruct the two safety boundaries.

Exercise 16.10¶

★☆☆ For each occurrence of $X$ in compute its polarity from the outside inward. Determine the largest ${\mathsf{Self}}_{+}$ subrecord and give the failed monotonicity premise for each removed field.

Referenced from 4 locations

• OO Self Types, F-Bounds, and Matching
• ch:oo-self-types: ch:oo-self-types

Exercise 16.11¶

★★☆ Define a positive Self type with natural and Boolean fields and $\mathit{toggle}:\mathsf{Unit}\to X$. Type a closed recursive package and one toggle reduction; then omit the natural field by width and repeat the generalized (UseSelf) preservation calculation.

Referenced from 4 locations

• OO Self Types, F-Bounds, and Matching
• ch:oo-self-types: ch:oo-self-types

Exercise 16.12¶

★★★ Let Prove that the recursive types match. Give the explicit higher-order fold/unfold typing of a match-polymorphic homogeneous comparison and its F-bound analogue. Then state the subsumption judgment that would be required to use a named ordered object where an ordered object is expected, and show by arrow-domain and record-width inversion which premise prevents its derivation.

Referenced from 4 locations

• OO Self Types, F-Bounds, and Matching
• ch:oo-self-types: ch:oo-self-types

Exercise 16.13¶

★★☆ Reconstruct the single generalized (UseSelf) preservation case when the runtime package annotation is a subtype of the expected public Self type. State exactly where Self-subtyping inversion, hidden-witness type substitution, payload subsumption, and payload substitution are used. Then give the corresponding progress argument when the scrutinee is already a closed package value.

Referenced from 3 locations

• OO Self Types, F-Bounds, and Matching
• ch:oo-self-types: ch:oo-self-types

Exercise 16.14¶

★★★ Extend the cell with $\mathit{bump}:\mathsf{Unit}\to X$, which increments the shared reference and returns the exact receiver. Type its package, including the annotated lambda and $\mathsf{succ}(!r)$. With two aliases, fully type the trace bump unit through the first, read through the second, recording the store typing before and after allocation, assignment, and dereference. Replace the field by $\mathsf{Ref}X$; identify the failed positivity and subtyping rules.

Referenced from 3 locations

• OO Self Types, F-Bounds, and Matching
• ch:oo-self-types: ch:oo-self-types

Exercise 21.15¶

★★★ Practical project.matching-package-checker Implement four finite checks for the types in this chapter: positivity, protocol matching, package introduction, and package opening. Preserve two invariants: references containing Self are invariant rather than positive, and (UseSelf) substitutes the same hidden witness into both payload and result. The seven cases must include $\mathsf{NamedOrdered}$ matching $\mathsf{Ordered}$, rejection of $\mathsf{Ref}X$, and the absence of matching-based subsumption. The audit is empty, and the run ends with $$\mathtt{\text{All 7 self/matching corpus cases passed.}}$$ Construct three deliberately incorrect checkers by reversing arrow polarity, treating references as covariant, and substituting a different witness in the result. Each variant must remain executable and fail at least one named case. These are finite boundary checks, not a proof of the step-indexed fundamental theorem.

Referenced from 4 locations

• OO Self Types, F-Bounds, and Matching
• Object calculus checker and evaluator
• ch:oo-self-types: ch:oo-self-types