Positive Self, F-bounds, matching, and state

The functional ${\mathsf{Self}}_{+}$ delta

Definition 16.4 extends the bounded-subtyping core by positive Self types and two primitive term forms: Every field type in $R(X)$ is positive in $X$. The Self-specific calculus extends reflexive–transitive subtyping by

$J\subseteq I$

Its ordinary term rules are

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢x:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢n:\mathsf{Nat}$

$b\in \{\mathsf{true},\mathsf{false}\}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢b:\mathsf{Bool}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{unit}:\mathsf{Unit}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢a:\mathsf{Nat}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{succ}(a):\mathsf{Nat}$

$\mathrm{\Delta };\mathrm{\Gamma },x:A⊢a:B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\lambda x:A.a:A\to B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢a:A\to B$$\mathrm{\Delta };\mathrm{\Gamma }⊢b:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢ab:B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢a:\mathsf{Bool}$$\mathrm{\Delta };\mathrm{\Gamma }⊢b:A$$\mathrm{\Delta };\mathrm{\Gamma }⊢c:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{if}a\mathsf{then}b\mathsf{else}c:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢a_i:A_i(i\in I)$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\{{\ell }_i=a_i{\}}_{i\in I}:\{{\ell }_i:A_i{\}}_{i\in I}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢a:\{{\ell }_i:A_i{\}}_{i\in I}$$j\in I$

$\mathrm{\Delta };\mathrm{\Gamma }⊢a.{\ell }_j:A_j$

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{fix}x:A.a:A$

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢a:B$

The Self-specific subtyping and typing rules are

$S=\mathsf{Self}X.R(X)$$\mathrm{\Delta };\mathrm{\Gamma }⊢a:R(C)$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{packSelf}C\mathsf{with}a\mathsf{as}S:S$

$S=\mathsf{Self}X.R(X)$$\mathrm{\Delta };\mathrm{\Gamma }⊢a:S$$X\notin \mathsf{FV}(D)$

Derived selection and its root are The selection body is subsumed from $B_j(X)$ to $B_j(S)$ by positivity; the reduction substitutes the hidden type before the payload term. The functional evaluation contexts are those of definition 16.5; they do not enter lambdas, recursion bodies, or Self-use bodies.

F-bounded comparison calculus

The separate equi-recursive calculus ${\mathsf{F}}_{\mathrm{eq}}$ has It uses equi-recursive conversion $$\mu X.A=A[\mu X.A/X]$$ and the F-bound rules

$\mathrm{\Delta };\mathrm{\Gamma }⊢a[C]:A[C/X]$

The root uses the displayed post-fixpoint premise; it grants no subtype comparison between distinct post-fixpoints.

Higher-order matching target

The restricted target ${\mathsf{H}}_{\mu }$ distinguishes kinds $\ast$ and $\ast \Rightarrow \ast$, pointwise operator subtyping $F⪯G$, bounded operator quantification, and iso-recursion. Proper-type subtyping includes

$J\subseteq I$

The ordinary target term rules are

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

$\mathrm{\Omega };\mathrm{\Gamma }⊢x:A$

$\mathrm{\Omega };\mathrm{\Gamma },x:A⊢t:B$

$\mathrm{\Omega };\mathrm{\Gamma }⊢\lambda x:A.t:A\to B$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t:A\to B$$\mathrm{\Omega };\mathrm{\Gamma }⊢u:A$

$\mathrm{\Omega };\mathrm{\Gamma }⊢tu:B$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t_i:A_i(i\in I)$

$\mathrm{\Omega };\mathrm{\Gamma }⊢\{{\ell }_i=t_i{\}}_{i\in I}:\{{\ell }_i:A_i{\}}_{i\in I}$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t:\{{\ell }_i:A_i{\}}_{i\in I}$$j\in I$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t.{\ell }_j:A_j$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t:A$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t:B$

Operator kinding and subtyping are

$\mathrm{\Omega },X:\ast ⊢A:\ast$

$\mathrm{\Omega }⊢\lambda X:\ast .A:\ast \Rightarrow \ast$

$\mathrm{\Omega }⊢F:\ast \Rightarrow \ast$$\mathrm{\Omega }⊢A:\ast$

$\mathrm{\Omega }⊢F(A):\ast$

$\mathrm{\Omega }⊢F:\ast \Rightarrow \ast$$\mathrm{Contr}(F)$

$\mathrm{\Omega }⊢\mu F:\ast$

$\mathrm{\Omega }⊢F⪯G$

$\mathrm{\Omega }⊢F⪯G$$\mathrm{\Omega }⊢A:\ast$

$\mathrm{\Phi }⪯F:\ast \Rightarrow \ast \in \mathrm{\Omega }$

$\mathrm{\Omega }⊢\mathrm{\Phi }⪯F$

$\mathrm{\Omega }⊢F:\ast \Rightarrow \ast$$\mathrm{Contr}(F)$$\mathrm{\Omega },\mathrm{\Phi }⪯F:\ast \Rightarrow \ast ⊢A:\ast$

$\mathrm{\Omega }⊢\mathrm{\forall }\mathrm{\Phi }⪯F.A:\ast$

$\mathrm{\Omega },\mathrm{\Phi }⪯F;\mathrm{\Gamma }⊢t:A$

$\mathrm{\Omega };\mathrm{\Gamma }⊢\mathrm{\Lambda }\mathrm{\Phi }⪯F.t:\mathrm{\forall }\mathrm{\Phi }⪯F.A$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t:\mathrm{\forall }\mathrm{\Phi }⪯F.A$$\mathrm{\Omega }⊢G:\ast \Rightarrow \ast$$\mathrm{Contr}(G)$$\mathrm{\Omega }⊢G⪯F$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t[G]:A[G/\mathrm{\Phi }]$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t:F(\mu F)$

$\mathrm{\Omega };\mathrm{\Gamma }⊢{\mathsf{fold}}_F(t):\mu F$

$\mathrm{\Omega };\mathrm{\Gamma }⊢t:\mu F$

$\mathrm{\Omega };\mathrm{\Gamma }⊢{\mathsf{unfold}}_F(t):F(\mu F)$

For source object types, matching is defined only by translated operator comparison: $$\mathrm{\Xi }⊢A\mathrm{\#}B⟺{\mathrm{\Xi }}^{†}⊢\mathrm{Oper}(A)⪯\mathrm{Oper}(B).$$ It licenses match abstraction, match application, and selection through a match-bound variable. It does not license source subsumption. The separate source typing judgment 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$

Invariant references and configuration roots

The state extension uses $\mathrm{\Delta };\mathrm{\Sigma };\mathrm{\Gamma }⊢a:A$, invariant $\mathsf{Ref}A$, and $$\mathrm{\Sigma }\vDash \sigma ⟺\mathrm{dom}(\mathrm{\Sigma })=\mathrm{dom}(\sigma )\wedge \cdot ;\mathrm{\Sigma };\cdot ⊢\sigma (\ell ):\mathrm{\Sigma }(\ell )(\ell \in \mathrm{dom}(\mathrm{\Sigma })).$$ The reference 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$

Allocation extends both store and store typing; dereference and assignment preserve the current store typing: