Object Calculi and Recursive Object Types

A record can contain functions, but selecting a function does not pass it the record that was selected. Passing the record when the function is built is also insufficient. After one method has been replaced, every other method must invoke the replacement through the new receiver. A receiver binder is the variable that invocation replaces by the current object, rather than an ordinary stored argument. Equivalently, the object is a finite system of mutually recursive equations $x_i=b_i(\overline{x})$. Replacing one equation should make every other equation refer to the replacement when the system is solved again; an ordinary record of already-closed functions solves the system once and freezes those references. The receiver binder is the syntax that keeps the equations open until invocation.

A receiver that survives replacement

Ground terms are variables, natural numerals, $\mathsf{unit}$, and $\mathsf{succ}(a)$, with $$n:\mathsf{Nat},\mathsf{unit}:\mathsf{Unit},\frac{a:\mathsf{Nat}}{\mathsf{succ}(a):\mathsf{Nat}}.$$ Numerals and unit are values, $\mathsf{succ}(n)⟼n+1$, and $\mathsf{succ}(E)$ is an evaluation context. These forms let the running methods return observable numerals.

The word object here means a runtime value: one receiver together with its methods. There are no class declarations, constructors, or nominal class types in this calculus. A class, if a source language had one, would instead be a separate device for producing such objects.

For the remainder of this section, abbreviate the running point interface by $$P:=[x:\mathsf{Nat},\mathit{get}:\mathsf{Nat}]$$ and define $$p_0:=[x=\varsigma (s:P)0,\mathit{get}=\varsigma (s:P)s.x].$$ The two premises of T-Object are $$s:P⊢0:\mathsf{Nat},\frac{s:P⊢s:P}{s:P⊢s.x:\mathsf{Nat}}\mathrm{T}-\mathrm{Invoke}.$$ Thus $\cdot ⊢p_0:P$. Notice that the body of $\mathit{get}$ does not contain $p_0$; it invokes $x$ through the receiver supplied when $\mathit{get}$ is called.

Put $$p_1:=p_0.x\Leftarrow \varsigma (s:P)1.$$ The override body has type $\mathsf{Nat}$ under $s:P$, so $p_1:P$. Reduction exposes late self invocation: The second line is decisive. The old $\mathit{get}$ body receives the new object and therefore finds the replacement for $x$.

Safety before subtyping

Two facts do all the work. Substitution reconnects an invoked body with its receiver, while canonical forms guarantee that a closed receiver has the method promised by its type.

Proof of Lemma 15.3 — Structural properties of Ob_1

Proof. Weakening is induction on the typing derivation. In the object case, first alpha-rename every $s_i$ away from the added declarations. The induction hypothesis changes $\mathrm{\Gamma },s_i:C⊢b_i:B_i$ into ${\mathrm{\Gamma }}^{\prime },s_i:C⊢b_i:B_i$, and T-Object restores the conclusion. Invocation and override restore their last rules; the latter treats its receiver premise and its self-body premise separately.

For substitution, induct on the derivation of $\mathrm{\Gamma },x:A⊢b:B$. At the variable $x$, use the assumed derivation $\mathrm{\Gamma }⊢a:A$; every other variable retains its declaration. For an object, alpha-rename each $s_i$ away from $x$ and from the free variables of $a$. The induction hypothesis gives $$\mathrm{\Gamma },s_i:C⊢b_i[a/x]:B_i$$ for every method, so T-Object applies. Invocation follows by applying the induction hypothesis to its receiver. In an override, apply it once to the receiver and once under the fresh declaration $s:C$ to the new body, then restore T-Override. The ground constructors have no new binder and follow directly.

For exchange, induct on the typing derivation. A variable lookup is preserved by the adjacent permutation because source types contain no term variables. Every nonbinding rule applies the induction hypotheses to its premises. For object formation and override, alpha-rename the self binder away from $x$ and $y$, exchange the two outer declarations in each body premise, and restore the rule. Thus the permutation cannot capture a free occurrence. ◻

Proof of Lemma 15.4 — Object canonical forms

Proof. Numerals and $\mathsf{unit}$ have ground types. The only remaining value form is an object literal. Inverting T-Object equates its annotation with $[{\ell }_i:B_i{]}_{i\in I}$, its label set with $I$, and each component result type with the corresponding $B_i$. There is no subsumption rule that could hide methods or change the outer type. ◻

Proof of Theorem 15.5 — Safety of the functional object calculus

Proof. For preservation, induct on the reduction derivation. Compatible steps use the induction hypothesis and restore the typing rule for the surrounding context. There are two new root cases.

For (Invoke), inversion of the receiver’s T-Object derivation gives $$s_j:A⊢b_j:B_j,\cdot ⊢[{\ell }_i=\varsigma (s_i:A)b_i{]}_{i\in I}:A.$$ Substitution therefore types the reduct $b_j[[{\ell }_i=\varsigma (s_i:A)b_i{]}_{i\in I}/s_j]$ at $B_j$, the type assigned by T-Invoke.

For (Override), inversion gives $s:A⊢c:B_j$ and, for the retained methods, $s_i:A⊢b_i:B_i$. These are exactly the premises of T-Object for the replacement literal, so the reduct has type $A$. Ground contraction uses its ground typing premise.

For progress, induct on typing. Object literals are values. In an invocation, the receiver either steps, and the invocation context lifts that step, or is a value. In the latter case it is a literal containing the selected label by lemma 15.4, so (Invoke) applies. Override is identical up to its root rule. Ground terms use their usual progress cases. The final safety claim follows by applying preservation after every step and progress at the last term of any finite reduction. ◻

Width, invariance, and minimum types

An object with extra methods can answer every invocation understood by a smaller interface. This justifies width subtyping. It does not yet justify changing the result types of shared methods: every method body was checked under assumptions about every other method of self.

Proof of Lemma 25.8 — Top is maximal in object subtyping

Proof. Induct on the derivation in the least preorder. Reflexivity and S-Top have the stated target. Neither ground reflexivity nor S-Object can have source $\mathsf{Top}$. In a transitive derivation , the induction hypothesis for the first part makes $B=\mathsf{Top}$, and the hypothesis for the second then makes $A=\mathsf{Top}$. ◻

Proof of Lemma 25.9 — Inversion of width-invariant object subtyping

Proof. Use rule induction for the least preorder, together with the shape claim that a type below an object type is itself an object type. Reflexivity is immediate, and S-Object gives both the label inclusion and the component equalities. Neither S-Top nor a ground-type reflexivity judgment can end at an object type.

For transitivity, write . Inverting the second derivation gives $M=[{\ell }_k:D_k{]}_{k\in K}$, with $J\subseteq K$ and $D_j=C_j$ on $J$. Inverting the first gives $A^{\prime }=[{\ell }_i:B_i{]}_{i\in I}$, with $K\subseteq I$ and $B_k=D_k$ on $K$. Composing the inclusions and equalities proves the conclusion. This argument also proves the shape claim. An intermediate $\mathsf{Top}$ is excluded by lemma 25.8. ◻

For example, so $p_0$ may be passed to code that invokes only $\mathit{get}$. But when and $S\ne T$.

Subsumption destroys unique typing: $p_0$ has both displayed object types. The annotations in object formation and override nevertheless determine a minimum type for every typable term.

If an object with private methods is first viewed at a shorter interface $A$, an override annotated by $A$ has minimum type $A$, not the hidden longer type. The operation still creates a runtime object containing the private methods; the type checker does not recover an interface that the program chose to hide.

Proof of Lemma 15.8 — Narrowing the receiver

Proof. Induct on the typing derivation. In the distinguished variable case, $s:A^{\prime }$ follows by the variable rule and then T-Sub; other variables are unchanged. For object formation, alpha-rename each inner self binder away from $s$, apply the induction hypothesis to every body, and restore T-Object. Invocation and override apply the induction hypothesis to the receiver and to every premise in which the outer $s$ remains free; their own self binders are first made fresh. A final T-Sub is restored unchanged. Ground terms have no binding case. ◻

Proof of Lemma 15.9 — Source substitution with subtyping

Proof. Induct on the derivation of $\mathrm{\Gamma },x:A⊢b:B$. At $x$, use the assumed derivation $\mathrm{\Gamma }⊢a:A$; every other variable retains its declaration. For T-Object, alpha-rename each self binder away from $x$ and $\mathsf{FV}(a)$, apply the induction hypothesis to every body, and restore the same annotated object type. Invocation applies the induction hypothesis to its receiver. Override applies it once to the receiver and once to the replacement body under a freshly renamed self binder, then restores T-Override. Numerals and $\mathsf{unit}$ contain no variables, and a successor uses the induction hypothesis on its argument. If the last rule is T-Sub, apply the induction hypothesis to its term premise and restore the unchanged subtype judgment. Thus subsumption introduces no new substitution case. ◻

Proof of Theorem 15.10 — Minimum typing

Proof. For item 1, induct on the term. A variable’s type is fixed by $\mathrm{\Gamma }$, and the ground forms have fixed types. An object or override carries its result annotation $A$ in its syntax. For invocation, the induction hypothesis fixes the minimum receiver type; distinctness of labels fixes its component type. Thus no term form admits two different conclusions.

For items 2 and 3, use simultaneous induction on the minimum and declarative derivations. In M-Object, each minimum body type $B_i^{\prime }$ can be raised to $B_i$ by T-Sub; T-Object then gives the annotated type. In M-Override, raise the receiver from $A^{\prime }$ to $A$ and the new body from $B^{\prime }$ to $B_j$, then use T-Override. Invocation and ground cases are unchanged. This proves item 2.

Conversely, consider the last rule of a declarative derivation. If it is T-Sub, apply the induction hypothesis to its premise. If that premise has minimum type $A$, then for the premise type $B^{\prime }$, and transitivity with gives the required comparison.

Suppose the last rule is T-Object. The induction hypothesis gives a minimum type for each body under the annotated self context; M-Object gives the same annotated object type. Suppose it is T-Invoke. Its receiver has a minimum type $A^{\prime }$ below the displayed object type $A$. Lemma 25.9 says that $A^{\prime }$ contains every label of $A$ with exactly the same component type. The minimum invocation rule therefore returns the displayed $B_j$.

Finally suppose the last rule is T-Override, whose annotation is $A=[{\ell }_i:B_i{]}_{i\in I}$. The receiver’s minimum type $A^{\prime }$ satisfies , and the body’s minimum type $B^{\prime }$ satisfies . Rule M-Override therefore gives minimum type $A$. These cases exhaust the syntax. By item 1, any two types constructed this way are equal, so the minimum type is independent of the declarative derivation. ◻

Subtyping changes the override contraction in one small but essential way. If the runtime literal was constructed at $A^{\prime }$, the replacement body must be reannotated by $A^{\prime }$: From this point on, (Override-Sub) supersedes the earlier (Override) root whenever subsumption is present. The premise that typed the receiver implies . By lemma 15.8, a body checked with $s:A$ remains well typed with $s:A^{\prime }$. Leaving the annotation $A$ on only the new method would not form a legal object literal.

Proof of Theorem 15.11 — Safety with width-invariant subtyping

Proof. Use minimum typing to remove arbitrary final subsumption before analyzing an eliminator. For invocation, a value whose minimum type is below $[{\ell }_i:B_i{]}_{i\in I}$ is an object literal with at least those labels and the same result types. Applying lemma 15.9 to the invoked body and the actual receiver types the source reduct at $B_j$; a final subsumption restores any requested supertype.

For override, let the runtime receiver have construction type $A^{\prime }$, while the source override is annotated by $A$. Minimum typing gives . If its new body was checked at $B_j$ under $s:A$, receiver narrowing gives the same judgment under $s:A^{\prime }$. Lemma 25.9 says that the ${\ell }_j$ component of $A^{\prime }$ is exactly $B_j$. Together with the retained method premises, T-Object types the reduct of (Override-Sub) at $A^{\prime }$, and T-Sub raises it to $A$. Compatible reduction preserves typing by the induction hypothesis. These are the only additions to the preservation proof of theorem 15.5.

For progress, use minimum typing and width inversion in place of the earlier canonical-forms lemma. A closed value usable at a nonempty object type must be a literal containing every visible label. Invocation and override therefore have a root contraction after their receivers become values. The ground cases are unchanged. ◻

Two tempting record rules fail

Width subtyping is safe because a hidden method remains present and every visible method keeps the result type assumed by all bodies. Covariance would break the second fact even though override is functional.

Let For the covariance counterexample, define fresh local interfaces $$Q_c:=[m:S,n:S],P_c:=[m:T,n:S].$$ Suppose, contrary to definition 15.6, that object components were covariant. Then . Define $$s_0=[\mathit{tag}=\varsigma (s:S)\mathsf{unit}]:S,t_0=[]:T,$$ and $$q=[m=\varsigma (s:Q_c)s_0,n=\varsigma (s:Q_c)s.m]:Q_c.$$ By the proposed covariance, $q:P_c$, so the term $$r:=q.m\Leftarrow \varsigma (s:P_c)t_0$$ would have type $P_c$, and $r.n$ would have type $S$. Operationally, however, The alleged $S$-term has reduced to the empty object, and $(r.n).\mathit{tag}$ is stuck. The old body of $n$ relied on $m:S$; the new object retained that body while the replacement’s self parameter had type $T$, not the $S$ assumed by the retained body. Functional update prevented mutation of $q$, but it did not protect the other methods of $r$.

Proof of Proposition 15.12 — Covariant method components destroy preservation

Proof. The constructed term $r.n$ is typed at $S$. Its three-step reduct is $t_0=[]$, which is typed directly at $T=[]$ by T-Object. It cannot be typed at $S=[\mathit{tag}:\mathsf{Unit}]$: even the proposed covariant rule only forgets labels, so an induction on a subtype derivation shows that an object type below $S$ must contain $\mathit{tag}$, whereas $T$ contains none. Hence the reduct has no type $S$. Thus preservation fails on this closed term. ◻

A record field can be pulled out and used on its own. A self-bound method cannot, at least not at a shortened interface: its body may invoke a method that subsumption has hidden. For this failed-rule analysis only, make the conservative addition of arrows, lambda abstraction, and application with

$\mathrm{\Gamma },x:A⊢b:B$

$\mathrm{\Gamma }⊢\lambda x:A.b:A\to B$

$\mathrm{\Gamma }⊢f:A\to B\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢fa:B$

and the contraction $(\lambda x:A.b)v⟼b[v/x]$. Also add the total ground operation $\mathsf{plus}(m,n)⟼m+n$ on numerals, with left-to-right contexts $$\mathsf{plus}(E,a)\text{and}\mathsf{plus}(n,E).$$ None of these additions mentions objects, and none belongs to the source fragment translated in section 15.5.

Suppose there were an interface-annotated term $a{†}_A\ell$ with rules $$\frac{\mathrm{\Gamma }⊢a:AA=[{\ell }_i:B_i{]}_{i\in I}j\in I}{\mathrm{\Gamma }⊢a{†}_A{\ell }_j:A\to B_j}\mathrm{T}-\mathrm{Extract}$$ and, for an actual object built at $A^{\prime }$, the unambiguous contraction $$[{\ell }_i=\varsigma (s_i:A^{\prime })b_i{]}_{i\in I}{†}_A{\ell }_j⟼\lambda s:A.b_j.$$ The annotation records the interface used by the typing derivation; without it, the $A$ in the reduct would not be determined by the redex. For the extraction counterexample, define fresh local interfaces $$p=[x=\varsigma (s:P_x)1,f=\varsigma (s:P_x)1]:P_x$$ and $$a=[x=\varsigma (s:Q_x)1,y=\varsigma (s:Q_x)1,f=\varsigma (s:Q_x)\mathsf{plus}(s.x,s.y)]:Q_x.$$ Subsumption gives $a:P_x$, so extraction claims $a{†}_{P_x}f:P_x\to \mathsf{Nat}$. But $$(a{†}_{P_x}f)p⟼(\lambda s:P_x.\mathsf{plus}(s.x,s.y))p⟼\mathsf{plus}(p.x,p.y),$$ which is stuck at $p.y$. Invocation avoids this failure: it substitutes the actual object $a:Q_x$, not an arbitrary argument of the shortened type $P_x$.

A fluent object requires a recursive type

The point $p_1$ can be updated from outside, but it cannot yet offer a $\mathit{move}$ method that returns the updated point. If the point type is $R$, that method requires the equation $$R=[x:\mathsf{Nat},\mathit{get}:\mathsf{Nat},\mathit{move}:R].$$ No finite expansion closes this equation. After replacing the rightmost $R$ once, the result contains another occurrence requiring another replacement.

We use the iso-recursive rules of definition 24.1. In particular, $\mu X.A$ is not judgmentally equal to its unfolding, and the only ways to cross between them are $\mathsf{fold}$ and $\mathsf{unfold}$. The formation rule for $\mu X.A$ does not require positivity. The point equation below is in addition contractive under the definition of chapter 12, extended here by treating an object-type constructor as a guarding constructor: its occurrence of $X$ lies beneath that constructor. No algorithmic equality between recursive types is being added.

The $\mathit{move}$ body is the only non-immediate typing premise. Under $s:\mathsf{UPoint}$, invocation gives $s.x:\mathsf{Nat}$, so under the additional fresh binder $t:\mathsf{UPoint}$, $\mathsf{succ}(s.x):\mathsf{Nat}$. Override gives $$s:\mathsf{UPoint}⊢s.x\Leftarrow \varsigma (t:\mathsf{UPoint})\mathsf{succ}(s.x):\mathsf{UPoint}.$$ Folding gives the required method result $\mathsf{Point}$. The term receiver $s$ is substituted when $\mathit{move}$ is invoked; the type variable $X$ was already replaced by $\mathsf{Point}$ when the recursive type was unfolded.

Define $$\mathit{next}:=(\mathsf{unfold}\mathit{origin}).\mathit{move}.$$ Write the unfolded object created by this invocation as Then $\mathit{next}:\mathsf{Point}$, and the complete observable calculation is The retained $\mathit{get}$ body sees the replacement for $x$, exactly as in the finite point. Fold and unfold solve only the type equation. Invocation still substitutes the updated receiver $o_1$ for self in every selected method body: invoking $\mathit{get}$ contracts its body $s.x$ to $o_1.x$.

For this extension, $\mathrm{\Delta }$ is the type-variable context and $\mathrm{\Gamma }$ is the term-variable context; a judgment has the form $\mathrm{\Delta };\mathrm{\Gamma }⊢a:A$. A declaration $X$ extends only $\mathrm{\Delta }$, whereas a self declaration $s:A$ extends only $\mathrm{\Gamma }$. In contrast, chapter 8 places type bounds and term declarations in one context. Here type substitution changes $\mathrm{\Delta }$ and the type annotations in $\mathrm{\Gamma }$, whereas term substitution changes only terms under the fixed pair $\mathrm{\Delta };\mathrm{\Gamma }$.

Proof of Lemma 15.14 — The two substitutions

Proof. For item 1, induct on typing and type formation. In an object premise $\mathrm{\Delta },X;\mathrm{\Gamma },s:D⊢b:B$, the induction hypothesis gives $$\mathrm{\Delta };\mathrm{\Gamma }[C/X],s:D[C/X]⊢b[C/X]:B[C/X],$$ which is precisely the premise for the substituted object. Fold and unfold use the type-substitution composition calculation from lemma 24.3. Invocation and override restore their last rules.

For item 2, induct on typing. Alpha-rename a method’s bound self variable away from the substituted $s$, apply the induction hypothesis to its body, and restore the object or override rule. Fold and unfold bind no term variable, so their cases apply the induction hypothesis to the payload and restore the same rule. All other cases are those of lemma 15.3. ◻

Proof of Proposition 15.15 — Safety of recursive objects

Proof. The object roots still use item 2 of lemma 15.14. The new preservation root is $$\mathsf{unfold}({\mathsf{fold}}_{\mu X.A}v)⟼v,$$ whose typing derivation has $v:A[\mu X.A/X]$ as the premise of fold and the result type of unfold. For progress, the only value form at a recursive type is ${\mathsf{fold}}_{\mu X.A}v$. Therefore, if the argument of $\mathsf{unfold}$ is already a value of recursive type, it exposes exactly the root contraction displayed above; otherwise the evaluation-context rule steps its argument. The fold evaluation-context case and all object cases are unchanged. ◻

Objects as existential recursive records

The direct safety proof leaves a structural question. Can invocation, functional override, width subtyping, and late self all be reconstructed from functions, records, existentials, and recursive types? The first attempt is $$A^{\circ }=\mu X.\{{\ell }_i:X\to B_i^{\ast }{\}}_{i\in I}.$$ For width , an Amber-style comparison of the bodies assumes , but arrow contravariance asks for the reverse premise . Thus the naive record of methods cannot validate width. A second attempt stores a fixed self field $\mathsf{self}=r$ and implements override by changing only one method field. After overriding a coordinate method from $0$ to $1$, selection through the retained method still applies to the old $r$ and returns $0$, whereas source late self returns $1$. In the one-coordinate fragment, the failure is already visible in the candidate target records Functional update retains the closed body of $\mathit{get}$, so $$r_1.\mathit{get}\mathsf{unit}\stackrel{projectionandbeta}{⟶}{r}_0.\mathsf{self}.x\stackrel{projection}{⟶}{r}_0.x\stackrel{projection}{⟶}0,$$ whereas source late self gives $p_1.\mathit{get}{⟼}^{\ast }1$. The record-update notation here belongs only to the failed candidate, not to . The translation must therefore rebuild the suite on update and expose separate selection and update capabilities.

Rebuilding must hide the current receiver representation while retaining its public upper bound. The target calculus therefore combines a bounded existential package with an iso-recursive public interface.

Proof of Lemma 25.20 — Top is maximal in target subtyping

Proof. Induct on the subtype derivation. Rules S-Refl and S-Top have target $\mathsf{Top}$. The bound, arrow, record, existential, and Amber rules cannot have source $\mathsf{Top}$. In the transitive case, apply the induction hypothesis first to , obtaining $S=\mathsf{Top}$, and then to , obtaining $T=\mathsf{Top}$. ◻

The ordinary target rules already compute a complete small derivation. Put $R=\{n:\mathsf{Nat}\}$. Under $x:\mathsf{Nat}$, its lines are Target translation uses F-Pack to hide each self witness, F-Fold to form its recursive public interface, and F-Letrec to define the recursive record builder; source terms have no corresponding constructors.

The bounded package/open mechanism has a complete smaller instance. With $R=\{n:\mathsf{Nat}\}$, put The record derivation above and reflexivity of give . Inside , rule S-Bound and F-Sub type $r:R$, so F-Proj types $r.n:\mathsf{Nat}$. The result type contains no $X$; F-Open therefore gives the whole term type $\mathsf{Nat}$. This is the same hidden-witness/public-bound invariant used by the object translation.

The translation is scoped to the nonrecursive source calculus . Its target has arrows, covariant records, bounded existentials, iso-recursive types, and an unrestricted functional $\mathsf{letrec}$. Unlike the full of chapter 8, it omits bounded universals and $\mathsf{Bot}$. Unlike the kinded existentials of chapter 10, a hidden witness is known to lie below a public interface. The operation is called $\mathsf{open}$, and its result may not mention the fresh representation variable. Fold and unfold have the iso-recursive meaning fixed in chapter 12.

The target rules are used immediately. For example, $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{x:\mathsf{Nat}\in \mathrm{\Gamma }}{\mathrm{\Delta };\mathrm{\Gamma }⊢x:\mathsf{Nat}}}\mathrm{F}-\mathrm{Var}\\ \mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{unit}:\mathsf{Unit}\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\{a=x,b=\mathsf{unit}\}:\{a:\mathsf{Nat},b:\mathsf{Unit}\}}}\mathrm{F}-\mathrm{Record}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\{a=x,b=\mathsf{unit}\}.a:\mathsf{Nat}}\mathrm{F}-\mathrm{Proj}.$$ At the closed instance $x=0$, F-Proj contracts to $0$.

Proof of Lemma 15.18 — Target narrowing and substitution

Proof. The four proofs are simultaneous inductions on derivation height, with the judgment form as a secondary case split. For item 1, the distinguished bound-variable case changes into by transitivity. Other variables keep their bounds. Arrow and record subtyping apply the induction hypotheses component by component. In S-Exists, alpha-rename the existential variable, narrow the outer bound in both premises, and restore the rule. In S-Amber, make its two recursive variables fresh for $X$, narrow the body comparison, and restore the same simulation hypothesis. The typing rules merely propagate the narrowed type context.

For item 2, the distinguished term variable is typed at $R$ and then raised to $S$ by subsumption. Other variables are unchanged. Lambda, open, and letrec binders are first alpha-renamed away from $x$; the induction hypothesis applies to each premise in which the outer $x$ remains free. Pack, fold, unfold, records, projection, and application restore their last rules. This proves item 2 of lemma 15.18.

For item 3, the variable-bound case uses the premise . The arrow and record cases are componentwise. For bounded existentials, choose the bound variable fresh for $R$, apply the induction hypothesis to its bound and body, and restore S-Exists, F-Pack, or F-Open. The open escape condition is preserved because its freshly bound variable is not substituted. For S-Amber, first freshen both recursive variables; substitution then commutes with their binding, and the substituted premise restores Amber. Fold and unfold use the composition equality $$(T[\mu Y.T/Y])[R/X]{=}_{\alpha }T[R/X][\mu Y.T[R/X]/Y].$$ The letrec case substitutes in every parameter type, result type, defining term, and body before restoring F-Letrec.

For item 4, the distinguished variable case is exactly the assumed typing of $u$; every other variable retains its declaration. Alpha-renaming handles lambda, open, and letrec binders. In a package, substitute in its payload and retain the same witness and existential family; in an open term, substitute independently in the package and body and restore the escape condition. Successor, records, projection, application, fold, and unfold are homomorphic. Subsumption restores its unchanged target subtype judgment. These cases exhaust the target syntax. ◻

Proof of Lemma 25.23 — Existential inversion and the generalized open root

Proof. Prove inversion together with this shape claim: if an existential is below $C$, then $C$ is an existential or $\mathsf{Top}$. Rule induction proves the shape claim, with transitivity using it at both subderivations. Reflexivity gives $S_0=S$ and $T_0=T$. If the last rule is S-Exists, its premises are exactly and . In the transitive case the intermediate type cannot be $\mathsf{Top}$: no derivation can conclude with $C\ne \mathsf{Top}$, by lemma 25.20. Write it as . The two induction hypotheses give Narrow the last judgment from $S_1$ to $S_0$ by lemma 15.18 item 1, then compose both pairs by transitivity.

Now type a generalized open redex at $U$. Inversion of the package typing, including any final chain of F-Sub, gives This package inversion is an induction on typing: F-Pack gives the first two judgments, and every F-Sub composes one more subtype step. The outer-constructor inversion just proved ensures that each intermediate type on a path ending in an existential is again an existential.

Existential inversion gives and . Substitute $R$ for $X$ in the latter judgment by lemma 15.18 item 3 and use subsumption to obtain $\mathrm{\Delta };\mathrm{\Gamma }⊢t:T[R/X]$. The other premise of F-Open is Since , type substitution gives $\mathrm{\Delta };\mathrm{\Gamma },x:T[R/X]⊢u[R/X]:U$; the escape condition removes $X$ from the result type. Term substitution with the payload now gives $$\mathrm{\Delta };\mathrm{\Gamma }⊢u[R/X][t/x]:U,$$ which is precisely the generalized open reduct. ◻

The recursive root is well typed. Rule F-Letrec gives $r_D:F$. By substitution (item 4 of lemma 15.18), the defining judgment gives $t[r_D/f]:T$, so the lambdas give $h_D:F$. A second use of item 4 in the body judgment gives $u[h_D/f]:U$, exactly the type of the reduct.

For $A=[{\ell }_i:B_i{]}_{i\in I}$, define and Ground types and $\mathsf{Top}$ translate to their target counterparts. Selection makes $B_i^{\ast }$ occur covariantly; update makes it occur contravariantly. Their combination explains why the source component is invariant. The bound hides the object’s full interface while recording that it implements the public one.

Proof of Lemma 15.19 — Width is preserved by the type translation

Proof. Reflexivity, transitivity, and $\mathsf{Top}$ are preserved by the corresponding target rules. Consider width. Write $$A=[{\ell }_i:B_i{]}_{i\in I},B=[{\ell }_j:B_j{]}_{j\in J},J\subseteq I.$$ The shared result types are identical. For any representation variable $X$, S-Rec gives : it drops both ${\ell }^{\mathsf{sel}}$ and ${\ell }^{\mathsf{upd}}$ for every hidden label, while retaining $\mathsf{self}:X$. To apply Amber, work under . Rule S-Exists uses the latter bound and, under , the record comparison just proved. Hence Rule S-Amber now yields No component variance is used: the common selection and update field types are literally the same. ◻

For a label $\ell$ and a result type $B$, put

Proof of Lemma 15.20 — The visible-method target bound

Proof. Use S-Amber with recursive variables $Y_0,Y_L$. Work in the type context . There S-Exists reduces the desired body comparison to This is one application of covariant record width: retain the selection and self fields, and discard every update field and every field for a different label. The retained selection type is literally $X\to B^{\ast }$ because source object components are invariant. Restoring S-Exists and then S-Amber proves the displayed subtype. ◻

For a fixed object type $A=[{\ell }_i:B_i{]}_{i\in I}$, take $I=\{1,\dots ,n\}$ and write $o=[{\ell }_i=\varsigma (s_i:A)b_i{]}_{i\in I}$. First fix the recursive declaration Recall $r_{D_A}=\mathsf{letrec}{D}_A\mathsf{in}\mathit{create}$. The object translation is the application of that recursive function: $${\mathrm{tr}}_{\mathrm{\Gamma }}(o):=r_{D_A}(\lambda s_i:A^{\ast }.{\mathrm{tr}}_{\mathrm{\Gamma },s_i:A}(b_i){)}_{i\in I}.$$ If $\overline{f}=(f_i{)}_{i\in I}$, the letrec root followed by beta roots gives with the bound and existential annotation exactly as in equation 25.2. Thus the stored self and the separately translated object are literally the same term $r_{D_A}(\overline{f})$, not two letrec expressions that merely unfold to similar records. Each update calls the same recursive function with one replacement, so its stored self is the new object rather than a frozen predecessor. The occurrence of $\mathit{create}$ in the $\mathsf{self}$ field is not evaluated eagerly. The target relation is a compatible congruence, not a strategy; one letrec unfolding produces the finite term displayed above, and later reductions unfold another copy only when that occurrence is used.

For a label $\ell$, minimum typing and lemma 25.9 make its component type $B$ independent of which declarative object supertype was used to type the receiver. Put $u:=a.\ell \Leftarrow \varsigma (s:A)b$. Invocation and override translate as Variables translate to themselves. The environment translation replaces every $x:A$ by $x:A^{\ast }$. In (TUpd), the opened representation $X$ cannot escape: the update field first returns $X$, but target subsumption uses before the $\mathsf{open}$ closes, so the whole term has the public type $A^{\ast }$.

Proof of Lemma 25.26 — Translation is invariant under receiver narrowing

Proof. Induct on the source term. Variables and ground forms translate identically. For an object, its self annotations, declaration $D_A$, and generated $\mathit{create}$-parameter types are fixed by its syntax. Alpha-rename each method’s self binder away from the distinguished $s$, use item 3 of lemma 15.3 to put the outer $s$ last, and apply the induction hypothesis to the body. Thus every translated method function, and hence the application of $r_{D_A}$, is alpha-equal in the two environments.

For an invocation $r.\ell$, let $P$ and $P_0$ be the minimum types of $r$ before and after narrowing. The old minimum derivation gives $\mathrm{\Gamma },s:A⊢r:P$; source narrowing gives $\mathrm{\Gamma },s:A_0⊢r:P$. Minimum typing in the narrowed context therefore gives . If the invoked component of $P$ is $\ell :C$, lemma 25.9 says that the same component of $P_0$ is exactly $C$. Consequently both translations use $L_{\ell ,C}$, while their receiver translations are alpha-equal by induction.

For an override, the public object annotation and component type used in (TUpd) are written in the source term and hence unchanged. Apply the induction hypothesis to the receiver and, after freshening its bound self variable and using item 3 of lemma 15.3, to the replacement body. The generated open and lambda binders may then be alpha-renamed to agree. These cases exhaust the nonrecursive source syntax. ◻

Proof of Lemma 15.21 — Translation commutes with source substitution

Proof. Induct on $b$. The distinguished variable gives the displayed substituend; another variable is unchanged. For an object, alpha-rename every self binder and every generated $\mathit{create}$ parameter away from $x$ and the free variables of $a$. Apply the induction hypothesis to each method body. The declaration $D_A$ and surrounding application of $r_{D_A}$ are syntactically identical on both sides, so the translated method functions are equal up to the chosen alpha-renaming.

For invocation, suppose the receiver $r$ has minimum type $P$ in $\mathrm{\Gamma },x:A$, and its $\ell$-component is $B_{\ell }$. Minimum typing first gives $\mathrm{\Gamma },x:A⊢r:P$. Source substitution then gives $\mathrm{\Gamma }⊢r[a/x]:P$. If $P_0$ is the minimum type of the substituted receiver, the minimum-typing theorem yields . Lemma 25.9 therefore says that the $\ell$-component of $P_0$ is the same $B_{\ell }$, even though substitution may have refined the receiver minimum. The receiver translations agree by the induction hypothesis, and both sides consequently open the identical bound $L_{\ell ,B_{\ell }}$.

For override, apply the induction hypothesis to the receiver and, after making its self binder fresh, to the replacement body. The public annotation and its selected component are fixed in the source syntax, so term substitution changes neither. Variables, object literals, invocation, override, and ground constructors commute with substitution by the cases just given, exhausting the nonrecursive source term grammar. ◻

Minimum typing chooses the source shape from which the target package is built. In the invocation and override cases, target narrowing changes the opened self assumption from the public interface to the hidden witness type. For each source root, the simulation proof first performs the target administrative reductions that expose the translated method body and then uses translation-substitution on that body.

Proof of Theorem 25.28 — Scoped typing of the object translation

Proof. Let $A_0$ be the unique minimum type of $a$. Induct on its minimum-typing derivation to obtain ${\mathrm{\Gamma }}^{\ast }⊢{\mathrm{tr}}_{\mathrm{\Gamma }}(a):A_0^{\ast }$. Since , lemma 15.19 and target subsumption then give the stated type $A^{\ast }$. Variables use the translated context.

Objects. For an object, M-Object gives minimum body types . The induction hypotheses and target subsumption therefore type $\lambda s_i:A^{\ast }.\mathrm{tr}(b_i):A^{\ast }\to B_i^{\ast }$. Assume these functions as the parameters $f_i$ of $\mathit{create}$. With existential witness $X=A^{\ast }$, the selection field ${\ell }_i^{\mathsf{sel}}=f_i$ has type $A^{\ast }\to B_i^{\ast }$, and the update field ${\ell }_i^{\mathsf{upd}}=\lambda g.\mathit{create}(\overline{f}[i:=g])$ has type $(A^{\ast }\to B_i^{\ast })\to A^{\ast }$. The $\mathsf{self}$ field $\mathit{create}(\overline{f})$ also has type $A^{\ast }$. Hence the record has type $C_A(A^{\ast })$. Rule F-Pack, with witness and existential family $C_A(X)$, gives ; F-Fold then returns $A^{\ast }$. Rule F-Letrec therefore types $r_{D_A}$ at $$(A^{\ast }\to B_1^{\ast })\to \cdots \to (A^{\ast }\to B_n^{\ast })\to A^{\ast }.$$ Applying it to the translated method functions proves the object case.

Invocation. For invocation, let $A_0$ be the minimum type of the receiver. It contains $\ell :B$, so lemma 15.20 gives . Target subsumption followed by F-Unfold therefore gives an existential package whose hidden representation $X$ is below $L_{\ell ,B}$. Opening it yields $$z.{\ell }^{\mathsf{sel}}:X\to B^{\ast },z.\mathsf{self}:X,$$ so their application has type $B^{\ast }$. The result does not contain $X$, which discharges the existential escape condition.

Override. For override, let $A_0$ be the minimum receiver type. Rule M-Override gives , so lemma 15.19 permits target subsumption from $A_0^{\ast }$ to $A^{\ast }$ before unfold. Opening gives The same source rule gives a minimum body type . The induction hypothesis followed by target subsumption types its translation at $B^{\ast }$ under $s:A^{\ast }$. In the opened type context, ; target term-context narrowing, lemma 15.18 item 2, changes that assumption to $s:X$. Thus the lambda has type $X\to B^{\ast }$. The update field returns $X$, and target subsumption returns the public result type $A^{\ast }$, again free of the opened $X$. ◻

Proof of Theorem 15.22 — Scoped typing and simulation

Proof. Simulation contexts. For simulation, induct on the source reduction. The compatible-context cases require one check because the translation is type directed. Suppose a receiver step $a⟼a^{\prime }$ occurs under invocation by $\ell$. Inversion of the enclosing typing yields an interface $K$ containing $\ell :B$, together with the derivation $\mathrm{\Gamma }⊢a:K$. Source preservation gives $\mathrm{\Gamma }⊢a^{\prime }:K$. If $P$ and $P^{\prime }$ are the respective minimum receiver types, minimum typing gives and . Lemma 25.9 recovers the identical component $B$ in both minima. Thus both outer translations use exactly $L_{\ell ,B}$, and target congruence lifts the induction-hypothesis sequence from $\mathrm{tr}(a)$ to $\mathrm{tr}(a^{\prime })$.

For a receiver step under override, the public annotation, selected label, and selected component are fixed syntactically by the override term. The two outer target contexts are therefore identical, and target congruence again lifts the induction hypothesis. Ground evaluation contexts, such as $\mathsf{succ}(-)$, translate homomorphically. Weak evaluation has no context beneath a method binder. This exhausts the compatible contexts.

Invocation root. At an invocation root, write the receiver translation as $r_{D_A}(\overline{f})$. The letrec and beta roots in equation 25.4, followed by unfold and the generalized open root justified by lemma 25.23, expose its record. Projection selects $f_j$, while $\mathsf{self}$ selects the literal term $r_{D_A}(\overline{f})$. Beta reduction therefore gives $$(\lambda s_j:A^{\ast }.\mathrm{tr}(b_j))r_{D_A}(\overline{f}).$$ The argument is definitionally $\mathrm{tr}([{\ell }_i=\varsigma (s_i:A)b_i{]}_{i\in I})$, so this reduces by target substitution to the translation of the source substitution in (Invoke), by lemma 15.21.

Override root. At an override root, let the runtime receiver have construction type $A_0$ and let the override carry the public annotation $A$. As in (Override-Sub), minimum typing gives . The receiver translation therefore contains an actual package annotated , whereas (TUpd) opens it at . The generalized open root is applicable: its typing is exactly the package-subsumption case of lemma 25.23, and it substitutes the actual witness $A_0^{\ast }$ and actual record payload.

Projection selects the actual ${\ell }_j^{\mathsf{upd}}$ field. Its application and beta steps reduce to $$r_{D_{A_0}}(f_1,\dots ,f_{j-1},g_0,f_{j+1},\dots ,f_n),g_0=\lambda s:A_0^{\ast }.{\mathrm{tr}}_{\mathrm{\Gamma },s:A}(b).$$ Source receiver narrowing reannotates the replacement method by $A_0$ in the reduct. By lemma 25.26, $${\mathrm{tr}}_{\mathrm{\Gamma },s:A}(b){=}_{\alpha }{\mathrm{tr}}_{\mathrm{\Gamma },s:A_0}(b),$$ so $g_0$ is alpha-equal to the method function in the translation of that reannotated source object. Thus the displayed $r_{D_{A_0}}$-application is literally the translation of the source reduct. This proves the direct directional step $\mathrm{tr}(a){⟼}^{\ast }\mathrm{tr}(a^{\prime })$; no reverse target reduction is used. Its stored $\mathsf{self}$ is that same application, so subsequent invocations see the replacement. Ground contractions translate homomorphically. These cases prove item 2. ◻

The translation gives a semantic explanation, not a proposal for an efficient object layout. Its bounded existential hides private methods; its recursive record connects the hidden representation to the public interface; its paired selection and update components enforce invariance; and recursive creation re-ties self after every functional override. These four jobs cannot be performed by the naive recursive record alone.

The extension obstruction

The recursive point returns exactly $\mathsf{Point}$ from $\mathit{move}$. Add a color method and one expects the moved colored point to remain colored. Define the two candidate equations After unfolding, one would like width subtyping to forget $\mathit{color}$. Invariance blocks the comparison because the common $\mathit{move}$ components are $\mathsf{ColorPoint}$ and $\mathsf{Point}$, not the same type. Replacing invariance by covariance is not a remedy: proposition 15.12 shows that another retained method can rely on the more precise result and be invalidated by override through the shorter view. This is the precise contrast with covariant immutable records in chapter 8: record projection only reads a component, whereas an object method can be replaced and every retained method may invoke that replacement through self. The read/write combination forces invariance.

One may instead declare the colored point’s $\mathit{move}$ method to return $\mathsf{Point}$. That permits forgetting color after a move, but it does not express the desired fluent interface. The missing phrase is “the exact type of the present receiver, as refined by extension.” A recursively bound type variable fixes one equation; it does not vary with later extension. This is the Point/ColorPoint obstruction. No solution to it is assumed in this chapter.

The obstruction is a fixed recursive equation where extension requires a type that varies with the current receiver. F-bounded quantification and matching provide that varying type for immutable records. The reusable ingredients are late self and the shape ; covariance becomes safe once functional update is removed.

Sources.

The primitive syntax, self substitution, functional invocation and override, first-order typing, width-invariant subtyping, minimum typing, the covariance and extraction failures, and explicit recursive-object examples follow Abadi and Cardelli, A Theory of Primitive Objects: Untyped and First-Order Systems, author full version, Sections 2.1, 3.1–3.2.2, 4.1.1–4.1.2, 4.5.1–4.5.2, and 4.6–4.8. The two typed safety developments are at PDF pp. 15–17 and 21–23; the failed covariance/extraction rules and recursive objects are at PDF pp. 24–29 [AC96b]. The package/open typing and generalized contraction are in Table 1 of Abadi, Cardelli, and Viswanathan, An Interpretation of Objects and Object Types. Its target type , separate selection, update, and self fields, recursive $\mathit{create}$, and exact translation scope are in Sections 3.2–3.3, Table 2, and Theorems 3.1–3.3, PDF pp. 3–6 [ACV96]. That source proves computational adequacy but explicitly does not claim full abstraction; this chapter makes no stronger claim.

Suggested first pass.

Begin with exercise 15.8, exercise 15.9, exercise 15.13; then use the remaining problems to reconstruct safety and the translation.

Exercise 15.8¶

★★☆ Let $T=[a:\mathsf{Nat},b:\mathsf{Nat},c:\mathsf{Nat}]$ and $$t=[a=\varsigma (s:T)0,b=\varsigma (s:T)s.a,c=\varsigma (s:T)s.b].$$ Override $a$ with the constant method returning $4$, then reduce $c$ on the new object. Give the typing derivation and every invocation step, keeping the runtime receiver visible.

Referenced from 4 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.9¶

★★☆ For compute the minimum types of $b$, $b.p$, and $b.p\Leftarrow \varsigma (s:A)\mathsf{unit}$. Prove that every other declarative type of each term is a supertype of the one you give.

Referenced from 4 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.10¶

★★☆ Reprove preservation for invocation in without saying “by inversion” as a single step. Start from an arbitrary declarative derivation, extract its minimum receiver type, use width invariance to recover the selected component, display the body-substitution judgment, and restore the requested result supertype.

Referenced from 3 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.11¶

★★☆ Modify the covariance counterexample so that $Q_c$ has a third method $k:S$ whose body invokes $n$, and the final stuck term invokes $k$ before selecting $\mathit{tag}$. Give all types and show the full reduction. Explain why the extra indirection does not change the source of the failure.

Referenced from 3 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.12 — *¶

★★★ Let $A=[\ell :B]$, $\mathrm{\Gamma },s:A⊢b:B$, and $\mathrm{\Gamma },s:A⊢c:B$. Put $o=[\ell =\varsigma (s:A)b]$ and $u=o.\ell \Leftarrow \varsigma (s:A)c$. Type every field of $C_A(A^{\ast })$, its package as , and the enclosing fold. Put $o^{\prime }=[\ell =\varsigma (s:A)c]$. First show the source roots $u⟼o^{\prime }$ and $o^{\prime }.\ell ⟼c[o^{\prime }/s]$. Then use the target roots and the translation theorem to simulate $${\mathrm{tr}}_{\mathrm{\Gamma }}(u.\ell ){⟼}^{\ast }{\mathrm{tr}}_{\mathrm{\Gamma }}(o^{\prime }.\ell ){⟼}^{\ast }{\mathrm{tr}}_{\mathrm{\Gamma }}(c[o^{\prime }/s]).$$ Each arrow is a nonempty many-step target reduction; name every letrec, beta, unfold, open, and projection root it contains. Display the $r_{D_A}$-application containing the translated replacement method and use lemma 15.21 only for the final invocation beta step.

Referenced from 3 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.13¶

★★☆ Construct $\mathit{origin}$, $\mathit{next}$, and a colored analogue whose move method returns $\mathsf{ColorPoint}$. Type each object at its own recursive type. Then show that width-invariant subtyping cannot pass the colored object to a context requiring $\mathsf{Point}$, although both objects separately satisfy preservation and progress.

Referenced from 4 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.14¶

★★☆ Erase the self annotations from object literals and let $A=[\ell :[]]$, $A^{\prime }=[\ell :A]$, and $$a=[\ell =\varsigma (s)[\ell =\varsigma (t)[]]].$$ Work in with subsumption and the erased formation rule $$\frac{A=[{\ell }_i:B_i{]}_{i\in I}\mathrm{\Gamma },s_i:A⊢b_i:B_i(i\in I)}{\mathrm{\Gamma }⊢[{\ell }_i=\varsigma (s_i)b_i{]}_{i\in I}:A}\mathrm{T}-\mathrm{Object}-\mathrm{Erased}.$$ For the typing at $A$, show explicitly how width subtyping and T-Sub type the inner one-method object at the empty object result type. Give another typing of $a$ at $A^{\prime }$. Prove that $A$ and $A^{\prime }$ have no common subtype, so the unannotated calculus has no minimum type for $a$. Identify the two points at which the proof of theorem 15.10 can no longer recover a type from syntax.

Referenced from 3 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.15¶

★★☆ Consider the incorrect target scheme that recursively defines one record $r$ with selection fields ${\ell }_i^{\mathsf{sel}}$, sets $r.\mathsf{self}=r$, and implements source override by functional record update of one selection field. Translate $p_1.\mathit{get}$ with this scheme and reduce it to $0$. Then place beside it the source reduction to $1$ and locate the frozen occurrence of $r$ responsible for the discrepancy.

Referenced from 3 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 15.16¶

★★☆ Under $\mathrm{\Delta },X;\mathrm{\Gamma },s:A⊢b:B$, $\mathrm{\Delta }⊢C\mathsf{type}$, and $\mathrm{\Delta },X;\mathrm{\Gamma }⊢a:A$, freshen every binder away from the substituends and prove $b[C/X][a[C/X]/s]{=}_{\alpha }b[a/s][C/X]$. Work out the object-body and fold-payload cases. Explain why no condition $X\notin \mathsf{FV}(a)$ is needed and why a type $C$ cannot contain the term variable $s$.

Referenced from 3 locations

• Object Calculi and Recursive Object Types
• ch:object-calculi: ch:object-calculi

Exercise 25.17¶

★★★ Practical project.object-override-simulator Implement a finite object checker and evaluator for the point, override, fluent-self, and frozen-self cases. Preserve the invariant that override restores the runtime minimum annotation and every method body sees the rebuilt receiver. Include seven named observations that isolate late self, minimum typing, override reconstruction, and rejection of the frozen candidate. Then change creation to retain the old receiver, retain only the apparent annotation, and make components covariant in three independent variants; each must falsify its corresponding observation. The finite machine checks these traces, not the translation or safety theorems. Appendix E records the commands, and appendix F develops the implementation.

Referenced from 4 locations

• Object Calculi and Recursive Object Types
• Object calculus checker and evaluator
• ch:object-calculi: ch:object-calculi