ch:oo-self-types: ch:oo-self-types

With the added field, the comparison required by S-Self contains Arrow subtyping asks for the domain premise and the codomain premise . Only the latter is available. Thus the binary method is not covariant in the changing receiver type. If both interfaces instead use the fixed argument type, the comparison is Its premises are , by reflexivity, and , by the recursive assumption. Hence the fixed-argument method is compatible with the Self-subtyping proof.

The classifications, together with the comparisons induced by , are as follows. The positive cases induce The negative case instead induces . The fourth line has two variance reversals: first gives ; this is exactly the contravariant domain premise for the displayed outer-arrow comparison. The rejected positive use is $(X\to \mathsf{Bool})$. To derive , arrow subtyping would require , the unavailable orientation. None of these five families is both positive and negative: each contains a genuine occurrence of $(X)$, and the occurrence paths all have one fixed parity.

Let $$r_C=\{x=0,\mathit{color}=\mathsf{true},\mathit{clone}=\lambda u:\mathsf{Unit}.c_0,\mathit{move}=\lambda d:\mathsf{Nat}.c_0\}.$$ Unfolding $(c_0)$ in the receiver position and expanding derived selection gives The use body has type $(\mathsf{Nat}\to C)$: projection first gives $(z.\mathit{move}:\mathsf{Nat}\to X)$, and gives . At the root, first perform the type substitution, $$(z.\mathit{move})[C/X]=z.\mathit{move},z:\mathsf{ColorPointF}(C),$$ and only then the term substitution, $$(z.\mathit{move})[r_C/z]=r_C.\mathit{move}.$$ Consequently Before application, each function in the trace has type $(\mathsf{Nat}\to C)$, and $(3:\mathsf{Nat})$; hence every displayed application has result type $(C)$. One further call-by-value step would unfold $(c_0)$ to its package value, but the requested named endpoint is $(c_0)$.

Write $$S_i=\mathsf{Self}X.R_i(X)(i=0,1),S=\mathsf{Self}X.R(X).$$ Typing inversion for the redex supplies The first application of transitivity combines and , giving . The second combines this judgment with , giving . Separately, transitivity gives ; Self-subtyping inversion then yields Type substitution with the well-formed hidden witness $C$ gives . Payload subsumption therefore changes $v:R_0(C)$ into $v:R(C)$.

Use the derived in the bound-variable case of type substitution on the body premise. Since $(X)$ does not escape $(D)$, this gives $$x:R(C)⊢b[C/X]:D.$$ Term substitution with $(v:R(C))$ finally gives $$⊢b[C/X][v/x]:D,$$ which is exactly the (UseSelf) reduct at the original result type. Replacing $(C)$ by $(S)$ would instead produce $(b[S/X])$ and require a payload of type $(R(S))$. The runtime package contains $(v:R_0(C))$, and neither packaging nor subsumption changes its hidden representation witness; there is no equality $(C=S)$. Such a replacement would erase the very abstraction that the package records.

Put $(Q=\{ok:\mathsf{Bool}\})$ and replace the two equality fields by $(X\to Q)$. Use payloads $$\mathit{eq}=\lambda q:P_E.\{ok=\mathsf{false}\}\text{and}\mathit{eq}=\lambda q:C_E.\{ok=q\mathbf{\cdot }\mathit{color}\}$$ for the plain and colored packages. If the forbidden selection coercion is inserted, the supposed term of type $(Q)$ reduces as follows: $$r_P=\{x=0,\mathit{eq}=\lambda q:P_E.\{ok=\mathsf{false}\}\}.$$ The last record is not a value, and its field term is neither a value nor a redex.

The missing judgment occurs when selection tries to turn the projected method Arrow subtyping would require , whereas the hidden bound gives only . The pointwise premise of S-Self compares the two record families at the same formal parameter $(X)$, so both equality fields there have the identical type $(X\to Q)$; record width can discard the color field. That premise says nothing about the distinct comparison needed by selection, and therefore is not a term coercion.

The required client is Under , subsumption gives $$p:\mathsf{ResetF}(X)=\{x:\mathsf{Nat},\mathit{reset}:X,\mathit{same}:X\to \mathsf{Bool}\}.$$ Projection therefore gives $(p.\mathit{reset}:X)$ and $(p.\mathit{same}:X\to \mathsf{Bool})$; application gives the body type $(\mathsf{Bool})$. Abstraction and F-bound introduction yield The derivation chooses one $(X)$ and uses it for both receiver and argument. It never compares two different post-fixpoints, so it implies no subtype relation between them; in particular, the contravariant domain of $(\mathit{same})$ blocks the usual width-style recursive comparison.

Let $(R=\mu X.\mathsf{ResetF}(X))$ in the equi-recursive calculus. First, conversion is an equality judgment: $$R=\mathsf{ResetF}(R).$$ Only afterward do reflexivity and conversion yield the subtyping premise needed for F-elimination: Thus $(r[R]:R\to \mathsf{Bool})$. The equality unfolds the recursive type; the subtype judgment discharges the bound. They are not one rule.

Define For an arbitrary $(Z:\ast )$, record width, with reflexivity on every retained field, gives The translation of $\mathsf{MarkedMinMax}$ is $\mu \mathsf{MarkedMinMaxOp}$. Rule S-OpPoint turns the pointwise judgments into operator comparisons, hence $$\mathsf{MarkedMinMax}\mathrm{\#}\mathsf{MinMax}\text{and}\mathsf{MinMax}\mathrm{\#}\mathsf{Max}.$$ Transitivity of operator subtyping gives $(\mathsf{MarkedMinMax}\mathrm{\#}\mathsf{Max})$ directly. Instantiating the client at the third operator gives, with $M=\mathsf{MarkedMinMax}$, $$\mathit{preMax}[M]:M\to M\to M.$$ Thus both arguments and the result are exactly of type $(\mathsf{MarkedMinMax})$. No argument or result is coerced to either $(\mathsf{MinMax})$ or $(\mathsf{Max})$.

The match-bound variable exposes the $(n)$-field, so $$g=\mathrm{\Lambda }X\mathrm{\#}\mathsf{Max}.\lambda p:X.p.n:\mathrm{\forall }X\mathrm{\#}\mathsf{Max}.X\to \mathsf{Nat}.$$ Because $\mathsf{MinMax}\mathrm{\#}\mathsf{Max}$, match application gives $$g[\mathsf{MinMax}]:\mathsf{MinMax}\to \mathsf{Nat}.$$

In the target, write the bound operator as $({\mathrm{\Phi }}_X⪯\mathsf{MaxOp})$. The translation is $$g^{†}=\mathrm{\Lambda }{\mathrm{\Phi }}_X⪯\mathsf{MaxOp}.\lambda p:\mu {\mathrm{\Phi }}_X.({\mathsf{unfold}}_{{\mathrm{\Phi }}_X}(p)).n.$$ For $(p:\mu {\mathrm{\Phi }}_X)$, the derivation has the three requested steps: The second line is S-OpApp; the third is term subsumption; the fourth is projection. Instantiation substitutes $(\mathsf{MinMaxOp})$ for $({\mathrm{\Phi }}_X)$. Matching authorizes that operator instantiation, not a source subsumption rule. Thus an independently supplied $(m:\mathsf{MinMax})$ may be passed to $(g[\mathsf{MinMax}])$, but the judgment $(m:\mathsf{Max})$ is still not derivable.

Allocation starts the calculation: $$⟨\cdot ,\mathsf{ref}0⟩⟼⟨\{\ell \mapsto 0\},\ell ⟩.$$ Take $({\mathrm{\Sigma }}_1=\{\ell :\mathsf{Nat}\})$, replace $(r)$ by $(\ell )$ in $(k_r)$, and call the resulting value $(k_{\ell })$. The invariant holds because the two domains are $(\{\ell \})$ and $(\cdot ;{\mathrm{\Sigma }}_1;\cdot ⊢0:\mathsf{Nat})$. Writing $(a_2=k_{\ell })$, put Here $R_K$ is the record family in $K$, and $a\mathbf{\cdot }j$ expands to $U_j(a)$. Compatible-context and root steps give The only equality is expansion of derived selection. The subsequent arrows are, in order, fixpoint unfolding, (UseSelf), projection, beta, assignment, beta, fixpoint unfolding, beta, fixpoint unfolding, (UseSelf), projection, and dereference, all in the displayed left-to-right contexts. After assignment, the store and $({\mathrm{\Sigma }}_1)$ still have the same domain and $(7:\mathsf{Nat})$, so the invariant is preserved. By contrast, $(\ell :=\mathsf{true})$ would require $(\mathsf{true}:\mathsf{Nat})$ in T-Assign; it is rejected before a configuration step exists.

Starting at each field type and multiplying the variance signs along the path to $(X)$ gives: The positive comparisons are for $\mathit{clone}$, for $\mathit{map}$ and $\mathit{choose}$, respectively. The negative field has . For $(\mathit{choose})$, the occurrence in the inner domain crosses two arrow domains and is positive; the result occurrence is directly positive. The largest legal positive subrecord therefore contains $(\mathit{clone})$, $(\mathit{map})$, and $(\mathit{choose})$, and removes only $(\mathit{equal})$. Keeping $(\mathit{equal})$ in a covariant record comparison would require in order to derive ; only is available.

Let The family is positive. Under $(t:T)$, the record has the payload type at witness $(T)$; reflexivity discharges , so T-PackSelf and T-Fix derive $(t_0:T)$. If $(r_T)$ denotes this record with $(t_0)$ in its last field, then $$(t_0\mathbf{\cdot }\mathit{toggle})\mathsf{unit}{⟼}^{\ast }(r_T.\mathit{toggle})\mathsf{unit}⟼(\lambda u:\mathsf{Unit}.t_0)\mathsf{unit}⟼t_0.$$

Omit the natural field and put $$T^{\prime }=\mathsf{Self}X.\{b:\mathsf{Bool},\mathit{toggle}:\mathsf{Unit}\to X\}.$$ At an arbitrary formal $(X)$, record width gives the full payload family below the smaller one, so S-Self gives . Opening the runtime package annotated $(T)$ at expected type $(T^{\prime })$, inversion yields hidden witness $(C=T)$, payload $(r_T:R_T(T))$, and . Self-family inversion gives ; type substitution gives ; payload subsumption gives $(r_T:R_{T^{\prime }}(T))$. Finally substitute $(T)$ for the hidden type binder and $(r_T)$ for the payload binder in the use body. This is the generalized (UseSelf) preservation calculation, with the omitted field discarded only by record subsumption.

Let For every $(Z:\ast )$, record width gives . Hence $(\mathsf{NamedOrdOp}⪯\mathsf{OrdOp})$, so $$\mu \mathsf{NamedOrdOp}\mathrm{\#}\mu \mathsf{OrdOp}.$$ Ordinary recursive subtyping need not hold. After unfolding, comparison of the $(\mathit{le})$ fields would compare $(\mu \mathsf{NamedOrdOp}\to \mathsf{Bool})$ with $(\mu \mathsf{OrdOp}\to \mathsf{Bool})$; the arrow-domain premise has the reverse orientation and is not supplied by record width.

The source match-polymorphic client and its target are For the target body, $({\mathsf{unfold}}_{\mathrm{\Phi }}p:\mathrm{\Phi }(\mu \mathrm{\Phi }))$, , and subsumption exposes $(\mathit{le}:\mu \mathrm{\Phi }\to \mathsf{Bool})$; applying it to $(q:\mu \mathrm{\Phi })$ gives $(\mathsf{Bool})$. Construction is explicit too. For example, if $$r_N=\{\mathit{name}=0,\mathit{le}=\lambda q:\mu \mathsf{NamedOrdOp}.\mathsf{false}\},$$ then $(r_N:\mathsf{NamedOrdOp}(\mu \mathsf{NamedOrdOp}))$ and $n={\mathsf{fold}}_{\mathsf{NamedOrdOp}}(r_N):\mu \mathsf{NamedOrdOp}$. Instantiating $({\mathit{cmp}}^{†})$ at $(\mathsf{NamedOrdOp})$ and applying it to $(n,n)$ unfolds $(n)$, exposes the record, projects $(\mathit{le})$, and beta-reduces to $(\mathsf{false})$.

The F-bounded analogue is It may be instantiated at $(N=\mu X.\mathsf{NamedOrdered}(X))$, because equi-recursive conversion and record width give . Neither construction derives the absent subsumption judgment $(m:\mu \mathsf{OrdOp})$ from $(m:\mu \mathsf{NamedOrdOp})$: matching discharges a polymorphic bound; it does not coerce independently supplied values.

For preservation, induct on the reduction derivation. In each compatible context, invert the outer typing rule, apply the induction hypothesis to the unique active subterm, and rebuild that same rule; for record fields this is done at the leftmost nonvalue component. Beta and fixpoint unfolding use term substitution. The $(\mathsf{succ})$, conditional, and record projection roots follow from inversion of their typing derivations.

For the Self root, canonical forms and typing inversion write the redex as a package with hidden witness $C$, runtime annotation $S_0=\mathsf{Self}X.R_0(X)$, payload $v:R_0(C)$, and expected type $S=\mathsf{Self}X.R(X)$, with Self-subtyping inversion gives under . Substitution of $(C)$ gives , and payload subsumption gives $(v:R(C))$. Transitivity gives , so hidden-witness type substitution in the body yields $(x:R(C)⊢b[C/X]:D)$. Payload substitution then derives $(b[C/X][v/x]:D)$, exactly the reduct. This covers the only root for which the public annotation and runtime annotation may differ.

For progress, induct on a closed typing derivation after stripping final subsumption. Constants, lambdas, record values, and packages are values. For $(\mathsf{succ})$, conditionals, applications, and projections, the induction hypotheses step the leftmost active subterm; otherwise canonical forms supply respectively a numeral, Boolean, lambda, or record with the requested label, and the corresponding root fires. A record steps its leftmost nonvalue field. A fixpoint always unfolds. For packing, the payload either steps or the package is a value. For a Self use, the receiver either steps or the Self canonical form supplies $(\mathsf{packSelf}C\mathsf{with}v\mathsf{as}{S}_0)$, so the generalized (UseSelf) root fires even when . These cases exhaust the grammar. Iterating preservation and applying progress at the last term proves that no closed well-typed term reaches a stuck term.

Extend the type to $$K^{+}=\mathsf{Self}X.\{\mathit{contents}:\mathsf{Ref}\mathsf{Nat},\mathit{set}:\mathsf{Nat}\to X,\mathit{bump}:\mathsf{Unit}\to X\}.$$ After allocating $(r:\mathsf{Ref}\mathsf{Nat})$, define The annotations make the two sequencing lambdas explicit. From $(r:\mathsf{Ref}\mathsf{Nat})$ one gets $(!r:\mathsf{Nat})$, then $(\mathsf{succ}(!r):\mathsf{Nat})$, then $(r:=\mathsf{succ}(!r):\mathsf{Unit})$; the inner application therefore returns $(k:K^{+})$. Thus $(\mathit{bump}:\mathsf{Unit}\to K^{+})$, the payload has the family instantiated at $(K^{+})$, and T-PackSelf plus T-Fix types $(k_r^{+}:K^{+})$.

Allocation gives $$⟨\cdot ,\mathsf{ref}0⟩⟼⟨{\sigma }_0,\ell ⟩,{\mathrm{\Sigma }}_1=\{\ell :\mathsf{Nat}\}.$$ Let $(a_1=a_2=k_{\ell }^{+})$, and put Here $R_{K^{+}}$ is the family displayed in $K^{+}$, and $a\mathbf{\cdot }j$ expands to $U_j^{+}(a)$. The outer function has type $(K^{+}\to \mathsf{Nat})$; selection gives $a_1\mathbf{\cdot }\mathit{bump}:\mathsf{Unit}\to K^{+}$, so $(e:\mathsf{Nat})$. The configuration trace is The intermediate types are determined at every root: unfolding $k_{\ell }^{+}$ yields $p_{\ell }^{+}:K^{+}$; opening that package exposes ${\hat{r}}_{\ell }:R_{K^{+}}(K^{+})$; projection yields ${\hat{r}}_{\ell }.\mathit{bump}:\mathsf{Unit}\to K^{+}$; the two beta roots preserve result type $K^{+}$; dereference, successor, and assignment have types $\mathsf{Nat}$, $\mathsf{Nat}$, and $\mathsf{Unit}$; the sequencing beta returns $k_{\ell }^{+}:K^{+}$. The second alias is unfolded and opened in the same way, after which contents projection has type $\mathsf{Ref}\mathsf{Nat}$ and the final dereference has type $\mathsf{Nat}$. Before allocation the store typing and store are empty. After allocation, after assignment, and after dereference the store typing remains $({\mathrm{\Sigma }}_1)$; its unique cell contains respectively $(0)$, $(1)$, and $(1)$, all of type $(\mathsf{Nat})$. The two aliases therefore share the same invariant cell.

If a field is replaced by $(\mathsf{Ref}X)$, the occurrence of $(X)$ lies beneath an invariant reference. By the chapter’s polarity grammar it is neither positive nor negative, so Self formation fails. A hypothetical covariant comparison would require from , but reference subtyping permits that judgment only when $(C=D)$; read/write covariance would be unsound.