ch:object-calculi: ch:object-calculi

Twice applying T-Override to $p_0:P$ gives $p_2:P$. Put Compatible reduction first contracts the inner override and installs $2$: $$p_2⟼o_2.x\Leftarrow \varsigma (s:P)3⟼o_3.$$ The outer override therefore installs $3$, after which the two invocation roots give $$p_2.\mathit{get}{⟼}^{\ast }{o}_3.\mathit{get}⟼o_3.x⟼3.$$ Separately $p_0.\mathit{get}⟼p_0.x⟼0$. The unchanged old receiver still returning $0$ after $p_2$ is built is the exact functional, rather than imperative, observation.

The receiver and replacement premises are $p_0:P$ and $s:P⊢s.\mathit{get}:\mathsf{Nat}$, the latter by T-Invoke. For the reduct, its new $x$-body has exactly that derivation. Its retained body is typed by the other invocation $s:P⊢s.x:\mathsf{Nat}$. These are the two premises of T-Object, so the reduct has $P$, the type of the redex.

Rule M-Object gives $q$ minimum type $Q$; minimum invocation gives $q.x:\mathsf{Nat}$. Put $A=[x:\mathsf{Nat}]$. Since , the receiver and constant-body premises of M-Override give the last term minimum type $A$. Declaratively, subsume $q:Q$ to $q:A$, type $2$ under $s:A$, and apply T-Override; this also yields $A$.

Use the chapter’s types , $Q=[m:S,n:S]$, and $P=[m:T,n:S]$. The proposed covariant rule gives , hence $q:P$. Rule T-Override types $r=q.m\Leftarrow \varsigma (s:P)t_0:P$; invocation gives $r.n:S$, and a second invocation gives $\cdot ⊢(r.n).\mathit{tag}:\mathsf{Unit}$. The very first root, the override contraction, produces a runtime-$Q$ literal whose new $m$ body is $t_0:T$, although T-Object requires $S$. That is the first missing preservation premise. Continuing makes the defect observable: $r.n⟼r.m⟼t_0$, so tag selection is stuck.

For extraction, width is used exactly in , before T-Extract. It changes the claimed self parameter of the extracted method from $Q$, which contains $y$, to $P$, which does not. Consequently the alleged $P\to \mathsf{Nat}$ function can be applied to $p:P$, but reduces to $\mathsf{plus}(p.x,p.y)$ and is stuck at $p.y$.

Unfolding $\mathsf{Point}$ gives $\mathsf{UPoint}$, whose move component is $\mathsf{Point}$. Hence $$\mathit{origin}:\mathsf{Point},(\mathsf{unfold}\mathit{origin}).\mathit{move}:\mathsf{Point},p_2:\mathsf{Point}$$ by two uses each of T-Unfold and T-Invoke. Let $o_0$ be the runtime receiver inside origin. Abbreviate the retained move body by $$M(s)={\mathsf{fold}}_{\mathsf{Point}}(s.x\Leftarrow \varsigma (t:\mathsf{UPoint})\mathsf{succ}(s.x)).$$ The two distinct updated literals are The first unfold and move invocation gives ${\mathsf{fold}}_{\mathsf{Point}}{o}_1$; unfolding that fold and invoking the retained move gives ${\mathsf{fold}}_{\mathsf{Point}}{o}_2$. Therefore The occurrences $o_0,o_1,o_2$ make the two successive late-self substitutions visible.

Write $R(f,h)=r_{D_P}(f,h)$. Then ${\mathrm{tr}}_{\cdot }(p_0)=R(f_x,f_{\mathit{get}})$. In the translated override, the letrec root for $r_{D_P}$ and its parameter beta roots expose the folded package. The unfold root removes the fold; the generalized open root substitutes the actual witness and record; projection selects $${\ell }_x^{\mathsf{upd}}=\lambda k:P^{\ast }\to \mathsf{Nat}.R(k,f_{\mathit{get}}).$$ Its beta root yields $R(g,f_{\mathit{get}})$, literally ${\mathrm{tr}}_{\cdot }(p_1)$.

Target congruence performs those roots inside the receiver of the translated $\mathit{get}$-invocation. A second letrec/beta unfolding, followed by unfold, open, and the two projections, gives $$f_{\mathit{get}}(R(g,f_{\mathit{get}})).$$ Since $f_{\mathit{get}}=\lambda s:P^{\ast }.{\mathrm{tr}}_{s:P}(s.x)$, beta gives the translated $x$-invocation on that same $R$-term. Its letrec/beta, unfold, open, selection, self, and beta roots give $$g(R(g,f_{\mathit{get}}))⟼1.$$ No reverse step or frozen record identity is used.

One unfold exposes equal $x$ and $\mathit{get}$ components, but the shared $\mathit{move}$ components are respectively $\mathsf{Point}$ and $\mathsf{ColorPoint}$. Invariance blocks both directions there (and width also blocks Point-to-ColorPoint). Changing the colored result to Point recovers the width judgment ColorPoint-to-Point, so point clients may invoke move, but the result has type Point and color cannot be invoked afterward.

Under $s:T$, the three bodies have the judgments $$0:\mathsf{Nat},s.a:\mathsf{Nat},s.b:\mathsf{Nat}.$$ Thus T-Object gives $t:T$. Also $s:T⊢4:\mathsf{Nat}$, so T-Override and then T-Invoke give $$(t.a\Leftarrow \varsigma (s:T)4).c:\mathsf{Nat}.$$ The concrete updated receiver is $$t_4=[a=\varsigma (s:T)4,b=\varsigma (s:T)s.a,c=\varsigma (s:T)s.b].$$ Compatible reduction first contracts the override in receiver position. Every remaining arrow is an invocation root whose displayed receiver is substituted for the method’s self binder: The two retained bodies therefore consult $b$ and then $a$ through $t_4$, not through the original $t$.

The three minimum types are $B$, $\mathsf{Unit}$, and $A$. The last uses in M-Override. The minimum-typing theorem says any declarative conclusion is a supertype of the corresponding result; explicitly these are object-width supertypes of $B$, only $\mathsf{Unit}$ or Top for the projection, and object-width supertypes of $A$.

From an arbitrary typing of $v.{\ell }_j$, minimum typing gives the closed receiver a least object type . Canonical forms makes $v$ a literal built at $A_0=[{\ell }_i:C_i{]}_{i\in I}$. Width invariance recovers $C_j=B_j$. Formation inversion gives $s_j:A_0⊢b_j:C_j$, and source substitution with $v:A_0$ gives $b_j[v/s_j]:B_j$. If the requested invocation conclusion arose by subsumption, restore that final supertype by T-Sub.

Put $Q^{\prime }=[m:S,n:S,k:S]$ and $P^{\prime }=[m:T,n:S,k:S]$. Extend $q$ by $k=\varsigma (s:Q^{\prime })s.n$, and define $r^{\prime }=q^{\prime }.m\Leftarrow \varsigma (s:P^{\prime })t_0$. Covariance claims , so $r^{\prime }:P^{\prime }$, $r^{\prime }.k:S$, and $(r^{\prime }.k).\mathit{tag}:\mathsf{Unit}$. After the override root, let $v$ name the updated literal. The complete invocation schedule is $$(r^{\prime }.k).\mathit{tag}⟼(v.k).\mathit{tag}⟼(v.n).\mathit{tag}⟼(v.m).\mathit{tag}⟼t_0.\mathit{tag},$$ which is stuck. The added $k\to n$ call only delays the use of the illegally weakened $m$-result; the covariant component remains the first failed premise.

For $A=[\ell :B]$, $C_A(X)$ has ${\ell }^{\mathsf{sel}}:X\to B^{\ast }$, ${\ell }^{\mathsf{upd}}:(X\to B^{\ast })\to X$, and $\mathsf{self}:X$. At witness $X=A^{\ast }$, these become $A^{\ast }\to B^{\ast }$, $(A^{\ast }\to B^{\ast })\to A^{\ast }$, and $A^{\ast }$; there is no $A^{\ast }/X$ mismatch. The record is packed at and folded at $A^{\ast }$.

Put $o^{\prime }=[\ell =\varsigma (s:A)c]$. The source schedule is $$u⟼o^{\prime },u.\ell ⟼o^{\prime }.\ell ⟼c[o^{\prime }/s].$$ Let $f_b=\lambda s:A^{\ast }.{\mathrm{tr}}_{\mathrm{\Gamma },s:A}(b)$, $g_c=\lambda s:A^{\ast }.{\mathrm{tr}}_{\mathrm{\Gamma },s:A}(c)$, and $R(f)=r_{D_A}(f)$. The letrec/beta, unfold, open, update projection, and application beta roots give $${\mathrm{tr}}_{\mathrm{\Gamma }}(u){⟼}^{\ast }R(g_c)={\mathrm{tr}}_{\mathrm{\Gamma }}(o^{\prime }).$$ Target congruence therefore gives ${\mathrm{tr}}_{\mathrm{\Gamma }}(u.\ell ){⟼}^{\ast }{\mathrm{tr}}_{\mathrm{\Gamma }}(o^{\prime }.\ell )$. The next letrec/beta unfolding, unfold, open, selection and self projections, and application beta roots give $$g_c(R(g_c))⟼{\mathrm{tr}}_{\mathrm{\Gamma },s:A}(c)[{\mathrm{tr}}_{\mathrm{\Gamma }}(o^{\prime })/s]{=}_{\alpha }{\mathrm{tr}}_{\mathrm{\Gamma }}(c[o^{\prime }/s])$$ by translation substitution. This is the translation of each source reduct, not the incorrect term $c[u/s]$.

For the ordinary object use the chapter’s $o_0:\mathsf{UPoint}$, $\mathit{origin}={\mathsf{fold}}_{\mathsf{Point}}{o}_0$, and $\mathit{next}=(\mathsf{unfold}\mathit{origin}).\mathit{move}$. The object premise types $x,\mathit{get}$ at $\mathsf{Nat}$; its move body overrides $x$ in $\mathsf{UPoint}$ and folds the result, so it has $\mathsf{Point}$. Hence origin and next both have $\mathsf{Point}$.

Put Invocation gives $s.x:\mathsf{Nat}$. Override types the payload of $N$ at $\mathsf{UColorPoint}$, and fold gives $\mathsf{ColorPoint}$. The other bodies have their displayed ground types. Thus $$\mathit{corigin}={\mathsf{fold}}_{\mathsf{ColorPoint}}{c}_0,\mathit{cnext}=(\mathsf{unfold}\mathit{corigin}).\mathit{move}:\mathsf{ColorPoint}.$$ After one type unfold, width comparison reaches the shared move fields $\mathsf{ColorPoint}$ and $\mathsf{Point}$. Invariance rejects them, although each calculus derivation is independently safe.

Write $$i:=[\ell =\varsigma (t)[]],a:=[\ell =\varsigma (s)i].$$ The empty literal has $[]:[]$. Choosing $A=[\ell :[]]$ as the self type for the inner one-method literal gives the explicit formation $$\frac{t:A⊢[]:[]}{\cdot ⊢i:A}\mathrm{T}-\mathrm{Object}.$$ Width gives , so weakening and the explicit subsumption let outer object formation conclude $a:A$. For the second typing, weaken the same inner formation to $s:A^{\prime }⊢i:A$, where $A^{\prime }=[\ell :A]$, and use it directly as the outer body premise; outer formation concludes $a:A^{\prime }$.

If some $C$ were below both $A$ and $A^{\prime }$, width-invariant subtyping would require the $\ell$-component of $C$ to equal both $[]$ and $A$. These distinct types cannot both be that component. Erasing the self annotation therefore removes the syntax that fixed the conclusions of object formation and override, precisely the two annotated cases used by the minimum-type uniqueness proof.

Here is the incorrect target fragment explicitly. Put $$R:=\mu Y.\{x^{\mathsf{sel}}:Y\to \mathsf{Nat},{\mathit{get}}^{\mathsf{sel}}:Y\to \mathsf{Nat},\mathsf{self}:Y\},$$ and define Let the deliberately bad recursive declaration and its old receiver be The letrec and beta roots expose the old record: $$r_0{⟼}^{\ast }{\mathsf{fold}}_R\{x^{\mathsf{sel}}=f_x,{\mathit{get}}^{\mathsf{sel}}=f_{\mathit{get}},\mathsf{self}=r_0\}.$$ Functional record update of only the selection field is the target term $$r_1^{-}:={\mathsf{fold}}_R\{x^{\mathsf{sel}}=g,{\mathit{get}}^{\mathsf{sel}}=(\mathsf{unfold}{r}_0).{\mathit{get}}^{\mathsf{sel}},\mathsf{self}=(\mathsf{unfold}{r}_0).\mathsf{self}\}.$$ Thus the frozen translation of $p_1.\mathit{get}$ has the complete reduction Beside it, the source uses the newly constructed receiver $p_1^{\prime }=[x=\varsigma (s:P)1,\mathit{get}=\varsigma (s:P)s.x]$: $$p_1.\mathit{get}⟼p_1^{\prime }.\mathit{get}⟼p_1^{\prime }.x⟼1.$$ The defective term is $(\mathsf{unfold}{r}_0).\mathsf{self}=r_0$, retained inside $r_1^{-}$. Recursive creation instead rebuilds the suite as $r_{D_P}(g,f_{\mathit{get}})$ and ties its self field to that same updated application.

Induct on $b$, freshening binders. In an object body both substitutions pass under each fresh self binder, and the induction hypothesis proves equality; in a fold payload they commute homomorphically and the type annotation obeys ordinary type-substitution composition. The variable cases are immediate, including $b=s$. No freshness condition on $X$ in $a$ is needed because the left side explicitly uses $a[C/X]$. Type terms contain no term variables, so $C$ cannot contain $s$.