Positive Self, F-bounds, matching, and state

Definition 16.4 fixes a core with call-by-value evaluation and bounded subtyping. It has immutable covariant records, unrestricted recursion, positive Self formation, and primitive pack/use operations. It proves safety; it is not normalizing. The existential encoding with a bound is explanatory. The primitive core treats pack/use iso-recursively.

Lemma 16.3 proves covariance for positive families and contravariance for negative families. Derived selection uses only the positive half. Self-subtyping inversion lemma 16.7 recovers the pointwise payload-family comparison from a public Self subtype.

Substitution and canonical forms support preservation and progress in theorem 16.9, theorem 16.10. The critical preservation case retains the runtime witness $C$, transports , substitutes $C$ for the hidden type binder, and only then substitutes the payload. The result type cannot contain the hidden type. Negative receiver arguments are deliberately rejected; the stuck counterexample in exercise 16.5 witnesses why.

${\mathsf{F}}_{\mathrm{eq}}$ is a separate equi-recursive comparison calculus. Its type-substitution lemma justifies F-elimination at a post-fixpoint . Homogeneous binary methods are expressible because one client-selected $X$ types both arguments, but no subtype relation between distinct recursive binary-method types follows. Proposition 21.12 proves that public recursive post-fixpoints do not erase arbitrary hidden-witness Self packages.

Definition 16.13 defines matching by pointwise operator subtyping in the restricted higher-order iso-recursive target ${\mathsf{H}}_{\mu }$. Reflexivity and transitivity are proposition 16.14; the restricted translation soundness result is theorem 16.15. It covers kinding, match abstraction, match application, and match-variable selection only. It asserts neither source subsumption nor a full operational simulation.

References are invariant, and a type containing the distinguished Self variable beneath $\mathsf{Ref}$ is rejected by positivity. Configuration preservation and progress are theorem 21.17, theorem 21.18; the allocation case extends $\mathrm{\Sigma }$, while assignment retains the cell’s invariant type. Corollary 21.19 gives syntactic state safety.

Definition 21.20 gives a local model for the reference-and-Self fragment. Its fundamental result and safety consequence are theorem 21.23, corollary 21.24. They are not transferred to the F-bounded or higher-order matching calculi.

Chapter 16 has no Kappa or Agda companion. Its central claims concern subtyping derivations, hidden type substitution, higher-kinded operator bounds, and quantified store invariants; appendix E records this deliberate boundary rather than presenting a finite trace as a proof.