Linear and affine term calculus

The core signature of chapter 18 is The judgment is $\mathrm{\Gamma };\mathrm{\Delta }⊢e:A$. Both contexts are finite maps, their domains are disjoint, and exchange is map equality. Write ${\mathrm{\Delta }}_1\mathrm{\#}{\mathrm{\Delta }}_2$ for disjoint domains and ${\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2$ for their union under that premise. Every rule display containing $\uplus$ carries the corresponding disjointness premise. The thirteen core typing rules are

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

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

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

$\mathrm{\Gamma };\cdot ⊢\ast :1$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:1$$\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢e_2:C$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢\mathsf{let}\ast =e_1\mathsf{in}{e}_2:C$

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

$\mathrm{\Gamma };\mathrm{\Delta }⊢\lambda x.e:A⊸B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:A⊸B$$\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢e_2:A$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢e_1{e}_2:B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:A$$\mathrm{\Gamma };{\mathrm{\Delta }}_2⊢e_2:B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢e_1\otimes e_2:A\otimes B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:A\otimes B$$\mathrm{\Gamma };{\mathrm{\Delta }}_2,x:A,y:B⊢e_2:C$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢\mathsf{let}x\otimes y=e_1\mathsf{in}{e}_2:C$

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

$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathsf{inl}e:A\oplus B$

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

$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathsf{inr}e:A\oplus B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_0⊢e_0:A\oplus B$$\mathrm{\Gamma };{\mathrm{\Delta }}_r,x:A⊢e_1:C$$\mathrm{\Gamma };{\mathrm{\Delta }}_r,y:B⊢e_2:C$

$\mathrm{\Gamma };{\mathrm{\Delta }}_0\uplus {\mathrm{\Delta }}_r⊢\mathsf{case}{e}_0\mathsf{of}\mathsf{inl}x\Rightarrow e_1\mid \mathsf{inr}y\Rightarrow e_2:C$

$\mathrm{\Gamma };\cdot ⊢v:A$

$\mathrm{\Gamma };\cdot ⊢!v:!A$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1⊢e_1:!A$$\mathrm{\Gamma },x:A;{\mathrm{\Delta }}_2⊢e_2:B$

$\mathrm{\Gamma };{\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2⊢\mathsf{let}!x=e_1\mathsf{in}{e}_2:B$

The premise of T-BangI is a value and has empty linear context.

Weak left-to-right call-by-value evaluation uses There is no context beneath a lambda, bang, or unselected branch. The six core roots are

$(\lambda x.e)v⟼e[v/x]$

$\mathsf{let}x\otimes y=v\otimes w\mathsf{in}e⟼e[v/x,w/y]$

$\mathsf{let}\ast =\ast \mathsf{in}e⟼e$

$\mathsf{case}(\mathsf{inl}v)\mathsf{of}\mathsf{inl}x\Rightarrow e_1\mid \mathsf{inr}y\Rightarrow e_2⟼e_1[v/x]$

$\mathsf{case}(\mathsf{inr}v)\mathsf{of}\mathsf{inl}x\Rightarrow e_1\mid \mathsf{inr}y\Rightarrow e_2⟼e_2[v/y]$

$\mathsf{let}!x=!v\mathsf{in}e⟼e[v/x]$

The one-step relation is their compatible closure $E[e]⟶E[e^{\prime }]$.

For the token extension, fix an infinite set $\mathsf{Tok}$ and a finite live set $H\subseteq \mathsf{Tok}$. Add atomic types $\mathsf{File}$ and $\mathsf{Bytes}$, primitive values $\mathsf{open}$, $\mathsf{read}$, and $\mathsf{close}$, and runtime values ${\mathsf{file}}_h,{\mathsf{bytes}}_h$. The four closed typing axioms are

$\mathrm{\Gamma };\cdot ⊢\mathsf{open}:1⊸\mathsf{File}$

$\mathrm{\Gamma };\cdot ⊢\mathsf{read}:\mathsf{File}⊸(\mathsf{File}\otimes \mathsf{Bytes})$

$\mathrm{\Gamma };\cdot ⊢\mathsf{close}:\mathsf{File}⊸1$

$\mathrm{\Gamma };\cdot ⊢{\mathsf{bytes}}_h:\mathsf{Bytes}$

There is no closed source typing axiom for ${\mathsf{file}}_h$. Instead, $H⊩e:A$ means that distinct placeholders $(x_h{)}_{h\in H}$ and a template $e_0$ satisfy $$\cdot ;(x_h:\mathsf{File}{)}_{h\in H}⊢e_0:A,e=e_0[{\mathsf{file}}_h/x_h{]}_{h\in H}.$$ Core steps leave $H$ unchanged, and the additional roots are

$h\in \mathsf{Tok}\setminus H$

$(H,\mathsf{open}\ast )⟶(H\cup \{h\},{\mathsf{file}}_h)$

$h\in H$

$(H,\mathsf{read}{\mathsf{file}}_h)⟶(H,{\mathsf{file}}_h\otimes {\mathsf{bytes}}_h)$

$h\in H$

$(H,\mathsf{close}{\mathsf{file}}_h)⟶(H\setminus \{h\},\ast )$

Finally, the affine, relevant, and unrestricted deltas retain all thirteen core rules with a uniform judgment subscript and add only

$\mathrm{\Gamma };\mathrm{\Delta }{⊢}_{a}e:A$$x\notin \mathrm{dom}(\mathrm{\Gamma },\mathrm{\Delta })$

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

$\mathrm{\Gamma };\mathrm{\Delta },x:A,y:A{⊢}_{r}e:B$$z\notin \mathrm{dom}(\mathrm{\Gamma },\mathrm{\Delta })$

$\mathrm{\Gamma };\mathrm{\Delta },z:A{⊢}_{r}e[z/x,z/y]:B$

The unrestricted judgment has both rules with subscript $u$; the linear judgment has neither.

Rig-indexed dependent comparison

This source-bounded card is McBride’s dependent calculus [McB16], not an extension of the monomorphic linear calculus above. It borrows dependent-function and bidirectional vocabulary from chapter 26, chapter 27. To avoid collision with the chapter’s structural-regime notation, this card alpha-renames source $R,\mathrm{\Gamma },\mathrm{\Delta },\rho ,\pi$ to $\mathcal{Q},\mathrm{\Theta },\mathrm{\Xi },q,p$. A precontext $\mathrm{\Theta }$ records variables and types. A $\mathrm{\Theta }$-context $\mathrm{\Xi }$ marks every variable of that same precontext by a quantity in the rig $\mathcal{Q}$; addition and scalar multiplication of contexts are pointwise. The bidirectional judgments are $$\mathrm{\Xi }{⊢}_{q}T\ni t,\mathrm{\Xi }{⊢}_{q}e\in S.$$ Types are checked at quantity zero. The source application rule is

${\mathrm{\Xi }}_0{⊢}_{q}f\in (px:S)\to T$${\mathrm{\Xi }}_1{⊢}_{qp}S\ni s$

${\mathrm{\Xi }}_0+{\mathrm{\Xi }}_1{⊢}_{q}fs\in T[s:S/x]$

Both premises mark one precontext, so a variable can remain available for forming the dependent result type even when its run-time quantity in one premise is zero.

The rigid system has no weakening rule. Section 12 of the source separately orders quantities, extends that order pointwise to contexts, and adds

$\mathrm{\Xi }{⊢}_{q}T\ni t$$\mathrm{\Xi }\le {\mathrm{\Xi }}^{\prime }$

${\mathrm{\Xi }}^{\prime }{⊢}_{q}T\ni t$

Retaining factorization, splitting, substitution, and safe erasure imposes the additional order conditions stated there. Thus zero-priced contemplation and ordered discardability are different rule cards; neither is a proof-irrelevance principle. Lemma 40’s unique-erasure conclusion has the additional hypothesis $q\ne 0$; the erasure development also assumes $q+p=0\Rightarrow q=0=p$, the book’s rendering of the source’s “absence of negation” condition.