Functional objects and recursive object representations

For distinct labels, the source extension is Its three primitive typing rules are

$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:A)b_i{]}_{i\in I}:A$

$\mathrm{\Gamma }⊢a:[{\ell }_i:B_i{]}_{i\in I}$$j\in I$

$\mathrm{\Gamma }⊢a.{\ell }_j:B_j$

$\mathrm{\Gamma }⊢a:A$$A=[{\ell }_i:B_i{]}_{i\in I}$$\mathrm{\Gamma },s:A⊢b:B_j$$j\in I$

$\mathrm{\Gamma }⊢a.{\ell }_j\Leftarrow \varsigma (s:A)b:A$

Objects are values, evaluation is weak. Put $v=[{\ell }_i=\varsigma (s_i:A^{\prime })b_i{]}_{i\in I}$. The roots are The second root records the runtime minimum type $A^{\prime }$, where . Width-invariant subtyping and subsumption are

$J\subseteq I$$B_j=C_j(j\in J)$

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

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

Minimum typing removes T-Sub; variables, ground forms, and invocation remain syntax directed, while formation and override become

$A=[{\ell }_i:B_i{]}_{i\in I}$$\mathrm{\Gamma },s_i:A{⊢}_{min}{b}_i:B_i^{\prime }$

$\mathrm{\Gamma }{⊢}_{min}[{\ell }_i=\varsigma (s_i:A)b_i{]}_{i\in I}:A$

$A=[{\ell }_i:B_i{]}_{i\in I}$$\mathrm{\Gamma }{⊢}_{min}a:A^{\prime }$$\mathrm{\Gamma },s:A{⊢}_{min}b:B^{\prime }$$j\in I$

$\mathrm{\Gamma }{⊢}_{min}a.{\ell }_j\Leftarrow \varsigma (s:A)b:A$

$\mathrm{\Gamma }{⊢}_{min}a:[{\ell }_i:B_i{]}_{i\in I}$$j\in I$

$\mathrm{\Gamma }{⊢}_{min}a.{\ell }_j:B_j$

Fluent methods use the iso-recursive equation $$\mathsf{Point}=\mu X.[x:\mathsf{Nat},\mathit{get}:\mathsf{Nat},\mathit{move}:X]$$ with the fold/unfold rules of subappendix A.21.

The translation target adds arrows, covariant records, bounded existentials, and iso-recursive types. Its characteristic subtyping calculus has formation rules

$\mathrm{\Delta }⊢S\mathsf{type}$$\mathrm{\Delta }⊢T\mathsf{type}$

$\mathrm{\Delta }⊢S\to T\mathsf{type}$

$\mathrm{\Delta }⊢S_i\mathsf{type}(i\in I)$

$\mathrm{\Delta }⊢\{k_i:S_i{\}}_{i\in I}\mathsf{type}$

$\mathrm{\Delta }⊢S\mathsf{type}$

$\mathrm{\Delta }⊢\mu X.T\mathsf{type}$

Its structural subtyping rules are

$\mathrm{\Delta }⊢S\mathsf{type}$

$\mathrm{\Delta }⊢S\mathsf{type}$

Its characteristic subtyping rules are

$J\subseteq I$

Ordinary target typing is generated by

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

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:S$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:T$

$\mathrm{\Delta };\mathrm{\Gamma },x:S⊢t:T$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\lambda x:S.t:S\to T$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:S\to T$$\mathrm{\Delta };\mathrm{\Gamma }⊢u:S$

$\mathrm{\Delta };\mathrm{\Gamma }⊢tu:T$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t_i:S_i(i\in I)$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\{k_i=t_i{\}}_{i\in I}:\{k_i:S_i{\}}_{i\in I}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:\{k_i:S_i{\}}_{i\in I}$$j\in I$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t.k_j:S_j$

The exact boundary rules are

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:T[R/X]$

$X\notin \mathsf{FV}(U)$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:T[\mu X.T/X]$

$\mathrm{\Delta };\mathrm{\Gamma }⊢{\mathsf{fold}}_{\mu X.T}t:\mu X.T$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:\mu X.T$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{unfold}t:T[\mu X.T/X]$

If $F=S_1\to \cdots \to S_n\to T$, recursive creation is typed by

$\mathrm{\Delta };\mathrm{\Gamma },f:F,x_1:S_1,\dots ,x_n:S_n⊢t:T$$\mathrm{\Delta };\mathrm{\Gamma },f:F⊢u:U$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{letrec}f(x_i:S_i{)}_{i=1}^n:T=t\mathsf{in}u:U$

Opening an actual package annotated at a subsumed existential type contracts using its actual witness and payload: For $A=[{\ell }_i:B_i{]}_{i\in I}$, put The recursive declaration is With $r_{D_A}=\mathsf{letrec}{D}_A\mathsf{in}\mathit{create}$, the exact object clause is $${\mathrm{tr}}_{\mathrm{\Gamma }}([{\ell }_i=\varsigma (s_i:A)b_i{]}_{i\in I})=r_{D_A}(\lambda s_i:A^{\ast }.{\mathrm{tr}}_{\mathrm{\Gamma },s_i:A}(b_i){)}_{i\in I}.$$ Unfolding the recursive function places the literal same term $r_{D_A}(\overline{f})$ in its $\mathsf{self}$ field and places $r_{D_A}(\overline{f}[i:=g])$ in update field $i$. Invocation unfolds, opens, selects ${\ell }_j^{\mathsf{sel}}$, and supplies $\mathsf{self}$; override selects ${\ell }_j^{\mathsf{upd}}$ and supplies the translated replacement.