Capture, typestate, and coeffect interfaces

Chapter 51:

Types are $X$ or $C▹U$, where and $C::=\{x_1,\dots ,x_n\}\mid \star$. Capture-set substitution replaces $x$ by a finite or universal bound in type annotations. The complete subcapturing generators are

$\mathrm{\Gamma }⊢C{\preccurlyeq }_{\mathsf{cap}}\star$

$\mathrm{\Gamma }⊢\{x_i\}{\preccurlyeq }_{\mathsf{cap}}C(1\le i\le n)$

$\mathrm{\Gamma }⊢\{x_1,\dots ,x_n\}{\preccurlyeq }_{\mathsf{cap}}C$

$1\le i\le n$

$\mathrm{\Gamma }⊢\{x_i\}{\preccurlyeq }_{\mathsf{cap}}\{x_1,\dots ,x_n\}$

$x:T\in \mathrm{\Gamma }$$\mathrm{\Gamma }⊢\mathrm{cv}(T,\mathrm{\Gamma }){\preccurlyeq }_{\mathsf{cap}}C$

$\mathrm{\Gamma }⊢\{x\}{\preccurlyeq }_{\mathsf{cap}}C$

Reflexivity and transitivity are admissible. Capture and function subtyping retain their two premises:

$\mathrm{\Gamma }⊢C_1{\preccurlyeq }_{\mathsf{cap}}{C}_2$

The capture-specific typing interface is $$\frac{x:C▹U\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:\{x\}▹U}\mathrm{Var}-\mathrm{C}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma },x:S⊢t:T\\ \mathrm{\Gamma }⊢\mathrm{\Pi }(x:S).T\mathsf{wf}\end{array}}{\mathrm{\Gamma }⊢\lambda (x:S).t:\mathrm{fv}(\lambda (x:S).t)▹\mathrm{\Pi }(x:S).T}\mathrm{Abs}-\mathrm{C}.$$ Variables declared at abstract type $X$ retain type $X$. Type abstraction attaches its free variables, type application performs bounded substitution, and subsumption closes the typing relation:

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

$\mathrm{\Gamma }⊢x:X$

$\mathrm{\Gamma }⊢S\mathsf{wf}$

$\mathrm{\Gamma }⊢t[S]:T[S/X]$

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

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

$$\frac{\begin{array}{c}\mathrm{\Gamma }⊢t:C▹\mathrm{\Pi }(x:S).T\\ \mathrm{\Gamma }⊢s:S\end{array}}{\mathrm{\Gamma }⊢ts:T[\mathrm{cv}(S,\mathrm{\Gamma })/x]}\mathrm{App}-\mathrm{C}.$$ $$\frac{v\text{ value}}{(\lambda (x:S).t)v{⟶}_{\mathsf{cap}}t[\mathrm{fv}(v)/x][v/x]}\mathrm{Beta}-\mathrm{C}.$$ Formation tracks positive and negative occurrences of term variables in type annotations. An arrow swaps polarities in its domain and admits its binder only positively in its codomain.

The separate card uses pure types containing $◻(C▹R)$, explicit unboxing, and monadic-normal-form machine states $⟨S\mid E\mid e⟩$. Its state-typing judgment combines store, continuation, and focused-expression typing. These rules do not extend the signature above.

Chapter 52: affine file typestate

The state set is $\{\mathsf{open},\mathsf{eof},\mathsf{closed}\}$. Read branches from open to open or eof; close goes from open or eof to closed. Protocol contexts map variables to $\mathsf{File}[q]$ and admit no contraction. The flow judgment $\mathrm{\Delta }⊢P⊣{\mathrm{\Delta }}^{\prime }$ has the following return, open, close, and read rules:

$\mathrm{\Delta }⊢\mathsf{return}⊣\mathrm{\Delta }$

$\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]⊢P⊣{\mathrm{\Delta }}^{\prime }$$f\notin \mathrm{dom}(\mathrm{\Delta })$

$\mathrm{\Delta }⊢\mathsf{open}f;P⊣{\mathrm{\Delta }}^{\prime }$

$q\in \{\mathsf{open},\mathsf{eof}\}$$\mathrm{\Delta }⊢P⊣{\mathrm{\Delta }}^{\prime }$

$\mathrm{\Delta },f:\mathsf{File}[q]⊢\mathsf{close}f;P⊣{\mathrm{\Delta }}^{\prime }$

$\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]⊢P_m⊣{\mathrm{\Delta }}^{\prime }$$\mathrm{\Delta },f:\mathsf{File}[\mathsf{eof}]⊢P_e⊣{\mathrm{\Delta }}^{\prime }$

$\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]⊢\mathsf{read}f\mathsf{as}\{\mathsf{more}(f)\Rightarrow P_m\mid \mathsf{eof}(f)\Rightarrow P_e\}⊣{\mathrm{\Delta }}^{\prime }$

The two read premises have different input states and the same output context. Runtime/static agreement $H,\eta {\vDash }_{\mathsf{ts}}\mathrm{\Delta }$ requires state equality and injective handle identities. The root steps are

$\ell \notin \mathrm{dom}(H)$

$⟨H,\eta ,\mathsf{open}f;P⟩{⟶}_{\mathsf{ts}}⟨H[\ell \mapsto \mathsf{open}],\eta [f\mapsto \ell ],P⟩$

$\eta (f)=\ell$$H(\ell )\in \{\mathsf{open},\mathsf{eof}\}$

$⟨H,\eta ,\mathsf{close}f;P⟩{⟶}_{\mathsf{ts}}⟨H\setminus \ell ,\eta \setminus f,P⟩$

$\eta (f)=\ell$$H(\ell )=\mathsf{open}$

$⟨H,\eta ,\mathsf{read}f\mathsf{as}\{P_m\mid P_e\}⟩{⟶}_{\mathsf{ts}}⟨H,\eta ,P_m⟩$

$\eta (f)=\ell$$H(\ell )=\mathsf{open}$

$⟨H,\eta ,\mathsf{read}f\mathsf{as}\{P_m\mid P_e\}⟩{⟶}_{\mathsf{ts}}⟨H[\ell \mapsto \mathsf{eof}],\eta ,P_e⟩$

The call step unfolds a checked body after capture-avoiding renaming:

$X:(x:\mathsf{File}[q])⊸{\mathrm{\Delta }}_X=P_X\in \mathrm{\Omega }$

$⟨H,\eta ,X(f)⟩{⟶}_{\mathsf{ts}}⟨H,\eta ,P_X[f/x]⟩$

For a fixed checked procedure table $\mathrm{\Omega }$, the call interface is $$\frac{X:(x:\mathsf{File}[q])⊸{\mathrm{\Delta }}_X=P_X\in \mathrm{\Omega }}{f:\mathsf{File}[q]⊢X(f)⊣{\mathrm{\Delta }}_X[f/x]}\mathrm{TS}-\mathrm{Call}.$$ Here $\mathrm{dom}({\mathrm{\Delta }}_X)\subseteq \{x\}$. Its dynamic companion replaces $X(f)$ by $P_X[f/x]$ after alpha-renaming every procedure-local handle binder fresh for the caller.

Chapter 53: three coeffect cards

A scalar structure $(\mathcal{C},⊛,{\oplus }_{\mathsf{c}},\mathsf{use},\mathsf{ign},\le )$ has two monoids and two-sided distributivity of $⊛$ over ${\oplus }_{\mathsf{c}}$. A flat calculus adds ${\wedge }_{\mathsf{c}}$ with $r{\wedge }_{\mathsf{c}}s\le r{\oplus }_{\mathsf{c}}s$ and judgments $\mathrm{\Gamma }{@}_{\mathsf{f}}r⊢e:\tau$. Flat call-by-value beta contracts only arguments typed at $\mathsf{use}$. Flat call-by-name preservation requires either top-pointedness or bottom-pointedness together with ${\wedge }_{\mathsf{c}}=⊛={\oplus }_{\mathsf{c}}$, commutativity, and idempotence.

Its four typing rules are

$\varnothing {@}_{\mathsf{f}}\mathsf{ign}⊢c:\iota$

$x:\tau {@}_{\mathsf{f}}\mathsf{use}⊢x:\tau$

$\mathrm{\Gamma },x:\sigma {@}_{\mathsf{f}}(r{\wedge }_{\mathsf{c}}s)⊢e:\tau$

$\mathrm{\Gamma }{@}_{\mathsf{f}}r⊢\lambda x.e:\sigma {\stackrel{s}{\to }}_{\mathsf{c}}\tau$

${\mathrm{\Gamma }}_1{@}_{\mathsf{f}}r⊢e_1:\sigma {\stackrel{t}{\to }}_{\mathsf{c}}\tau$${\mathrm{\Gamma }}_2{@}_{\mathsf{f}}s⊢e_2:\sigma$

${\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2{@}_{\mathsf{f}}(r{\oplus }_{\mathsf{c}}(t⊛s))⊢e_1{e}_2:\tau$

The structural calculus annotates an $n$-variable context by a vector in ${\mathcal{C}}^n$. Abstraction removes the last scalar into the latent arrow; application concatenates the function vector with the argument vector scaled by the latent scalar. Weakening appends $\mathsf{ign}$, exchange swaps the corresponding vector cells, and contraction combines adjacent cells with ${\oplus }_{\mathsf{c}}$. Its substitution conclusion replaces the bound cell $r$ by the vector $r⊛S$. The binder and application rules expose how that vector changes:

$\mathrm{\Gamma },x:\sigma {@}_{\mathsf{s}}(R++⟨s⟩)⊢e:\tau$

$\mathrm{\Gamma }{@}_{\mathsf{s}}R⊢\lambda x.e:\sigma {\stackrel{s}{\to }}_{\mathsf{c}}\tau$

${\mathrm{\Gamma }}_1{@}_{\mathsf{s}}R⊢e_1:\sigma {\stackrel{t}{\to }}_{\mathsf{c}}\tau$${\mathrm{\Gamma }}_2{@}_{\mathsf{s}}S⊢e_2:\sigma$

${\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2{@}_{\mathsf{s}}(R++(t⊛S))⊢e_1{e}_2:\tau$