Modal effects and the two source cards

This appendix freezes the selected rules used by chapter 33. Identical metavariables in the three cards do not identify their judgments.

$\mathsf{Met}[\mathcal{T}]$

Fix an effect structure $\mathcal{T}$, a signature $\mathrm{\Sigma }(\ell )=A⇝B$, and the modality action and composition from section 33.1. Write $\mathsf{L}({\mathrm{\Gamma }}^{\prime })$ for the composite of locks in ${\mathrm{\Gamma }}^{\prime }$. Kinds are $\mathsf{Abs}$, $\mathsf{Any}$, and $\mathsf{Eff}$, with $\mathsf{Abs}$ the sole proper subkind of $\mathsf{Any}$. The effect structure supplies extension kinding $\mathrm{\Gamma }⊢D:\mathsf{Eff}$ and equivalence $\mathrm{\Gamma }⊢D{\equiv }_{\mathcal{T}}{D}^{\prime }$. The induced effect-context interface is

$\mathrm{\Gamma }⊢\varnothing :\mathsf{Eff}$

$ϵ:\mathsf{Eff}\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢ϵ:\mathsf{Eff}$

$\mathrm{\Gamma }⊢D:\mathsf{Eff}$$\mathrm{\Gamma }⊢E:\mathsf{Eff}$

$\mathrm{\Gamma }⊢D,E:\mathsf{Eff}$

$\mathrm{\Gamma }⊢\varnothing {\equiv }_{\mathcal{T}}\varnothing$

$ϵ:\mathsf{Eff}\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢ϵ{\equiv }_{\mathcal{T}}ϵ$

$\mathrm{\Gamma }⊢D_1{\equiv }_{\mathcal{T}}{D}_2$$\mathrm{\Gamma }⊢E_1{\equiv }_{\mathcal{T}}{E}_2$

$\mathrm{\Gamma }⊢D_1,E_1{\equiv }_{\mathcal{T}}{D}_2,E_2$

$\mathrm{\Gamma }⊢E,D{\equiv }_{\mathcal{T}}F$

$\mathrm{\Gamma }⊢E{⪯}_{\mathsf{e}}F$

Variables have their declared kind; $1:\mathsf{Abs}$; $[E]A:\mathsf{Abs}$ when $A:\mathsf{Any}$; $⟨D⟩A:K$ when $A:K$; arrows have kind $\mathsf{Any}$; and $\mathrm{\forall }{\alpha }^K.A:K^{\prime }$ when $\mathrm{\Gamma },\alpha :K⊢A:K^{\prime }$. Each operation declaration $A⇝B$ requires $A,B:\mathsf{Abs}$.

For completeness, the value-type kinding rules are

$\mathrm{\Gamma }⊢A:\mathsf{Abs}$

$\mathrm{\Gamma }⊢A:\mathsf{Any}$

$\alpha :K\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢\alpha :K$

$\mathrm{\Gamma }⊢1:\mathsf{Abs}$

$\mathrm{\Gamma }⊢[E]\mathrm{\Gamma }⊢A:\mathsf{Any}$

$\mathrm{\Gamma }⊢{◻}_{[E]}A:\mathsf{Abs}$

$\mathrm{\Gamma }⊢⟨D⟩\mathrm{\Gamma }⊢A:K$

$\mathrm{\Gamma }⊢{◻}_{⟨D⟩}A:K$

$\mathrm{\Gamma }⊢A:\mathsf{Any}$$\mathrm{\Gamma }⊢B:\mathsf{Any}$

$\mathrm{\Gamma }⊢A\to B:\mathsf{Any}$

$\mathrm{\Gamma },\alpha :K⊢A:K^{\prime }$

$\mathrm{\Gamma }⊢\mathrm{\forall }{\alpha }^K.A:K^{\prime }$

$\mathrm{\Gamma }⊢E:\mathsf{Eff}$

$\mathrm{\Gamma }⊢[E]$

$\mathrm{\Gamma }⊢D:\mathsf{Eff}$

$\mathrm{\Gamma }⊢⟨D⟩$

$\mathrm{\Gamma }⊢A:\mathsf{Abs}$$\mathrm{\Gamma }⊢B:\mathsf{Abs}$

$\mathrm{\Gamma }⊢A⇝B$

Figure 9, Appendix B.1, p. 31 of [TL26] reuses $K$ for both the quantified variable and the body kind in K-Forall. That printing rejects the paper’s own effect-polymorphic capability translation. Rule K-Forall above makes the necessary distinction between binder kind $K$ and body kind $K^{\prime }$.

Modal and type equivalence are structural over the selected effect equivalence:

$\mathrm{\Gamma }⊢E{\equiv }_{\mathcal{T}}F$

$\mathrm{\Gamma }⊢[E]{\equiv }_{\mathsf{Met}}[F]$

$\mathrm{\Gamma }⊢D{\equiv }_{\mathcal{T}}{D}^{\prime }$

$\mathrm{\Gamma }⊢⟨D⟩{\equiv }_{\mathsf{Met}}⟨D^{\prime }⟩$

$\alpha :K\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢\alpha {\equiv }_{\mathsf{Met}}\alpha$

$\mathrm{\Gamma }⊢1{\equiv }_{\mathsf{Met}}1$

$\mathrm{\Gamma }⊢\mu {\equiv }_{\mathsf{Met}}\nu$$\mathrm{\Gamma }⊢A{\equiv }_{\mathsf{Met}}B$

$\mathrm{\Gamma }⊢{◻}_{\mu }A{\equiv }_{\mathsf{Met}}{◻}_{\nu }B$

$\mathrm{\Gamma }⊢A{\equiv }_{\mathsf{Met}}{A}^{\prime }$$\mathrm{\Gamma }⊢B{\equiv }_{\mathsf{Met}}{B}^{\prime }$

$\mathrm{\Gamma }⊢A\to B{\equiv }_{\mathsf{Met}}{A}^{\prime }\to B^{\prime }$

$\mathrm{\Gamma },\alpha :K⊢A{\equiv }_{\mathsf{Met}}B$

$\mathrm{\Gamma }⊢\mathrm{\forall }{\alpha }^K.A{\equiv }_{\mathsf{Met}}\mathrm{\forall }{\alpha }^K.B$

The context well-formedness judgment is $\mathrm{\Gamma }@E$. Its full rules are

$\varnothing @E$

$\mathrm{\Gamma }@F$$\mathrm{\Gamma }⊢A:K$

$\mathrm{\Gamma },x{:}_{{\mu }_F}A@F$

$\mathrm{\Gamma }@F$$\mu (F)=E$

$\mathrm{\Gamma },\mathsf{lock}({\mu }_F)@E$

$\mathrm{\Gamma }@E$

$\mathrm{\Gamma },\alpha :K@E$

$\mathrm{\Gamma }@E$$\mathrm{\Gamma }⊢A⇝B$

$\mathrm{\Gamma },\ell :A⇝B@E$

The effect-structure kinding rules and the following term rules complete the frozen target signature.

$\mathrm{\Gamma }⊢():1@E$

$\mathrm{\Gamma },x:A⊢M:B@E$

$\mathrm{\Gamma }⊢\lambda x^A.M:A\to B@E$

$\mathrm{\Gamma }⊢M:A\to B@E$$\mathrm{\Gamma }⊢N:A@E$

$\mathrm{\Gamma }⊢MN:B@E$

$\mathrm{\Gamma },\alpha :K⊢V:A@E$

$\mathrm{\Gamma }⊢\mathrm{\Lambda }{\alpha }^K.V:\mathrm{\forall }{\alpha }^K.A@E$

$\mathrm{\Gamma }⊢M:\mathrm{\forall }{\alpha }^K.A@E$$\mathrm{\Gamma }⊢B:K$

$\mathrm{\Gamma }⊢MB:A[B/\alpha ]@E$

Variable access factors through a type-sensitive auxiliary transformation:

$\mathrm{\Gamma }⊢A:\mathsf{Abs}$

$\mathrm{\Gamma }⊢(\mu ,A)\Rightarrow \nu @F$

$\mathrm{\Gamma }⊢\mu \Rightarrow \nu @F$

$\mathrm{\Gamma }⊢(\mu ,A)\Rightarrow \nu @F$

$\mathrm{\Gamma }⊢(\mu ,A)\Rightarrow \mathsf{L}({\mathrm{\Gamma }}^{\prime })@F$

$\mathrm{\Gamma },x{:}_{{\mu }_F}A,{\mathrm{\Gamma }}^{\prime }⊢x:A@E$

$\mathrm{\Gamma },\mathsf{lock}({\mu }_F)⊢V:A@\mu (F)$

$\mathrm{\Gamma }⊢{\mathsf{mod}}_{\mu }V:{◻}_{\mu }A@F$

$\mathrm{\Gamma },\mathsf{lock}({\nu }_F)⊢V:{◻}_{\mu }A@\nu (F)$$\mathrm{\Gamma },x{:}_{(\nu \circ \mu {)}_F}A⊢N:B@F$

$\mathrm{\Gamma }⊢{\mathsf{let}}_{\nu }{\mathsf{mod}}_{\mu }x=V\mathsf{in}N:B@F$

Only values may be introduced or eliminated by these rules. The ordinary unit, abstraction, application, type-abstraction, and type-application rules are the call-by-value System-F rules, all at one displayed effect context. Operations and fresh local labels use

$\mathrm{\Sigma },\mathrm{\Gamma }\ni \ell :A⇝B$$\mathrm{\Gamma }⊢N:A@(\ell ,E)$

$\mathrm{\Gamma }⊢\mathsf{do}\ell N:B@(\ell ,E)$

$\mathrm{\Gamma },\ell :A⇝B⊢M:C@E$

$\mathrm{\Gamma }⊢\mathsf{local}\ell :A⇝B\mathsf{in}M:C@E$

For $H=\{\mathsf{return}x\mapsto N,\ell pr\mapsto N^{\prime }\}$, the handler rule is

$\mu (F)=E$$\mathrm{\Gamma }⊢\mu \Rightarrow \mathsf{id}@F$$\mathrm{\Gamma }⊢\mu \Rightarrow \mu \circ \mu @F$$\mathrm{\Gamma },\mathsf{lock}({\mu }_F),\mathsf{lock}(⟨\ell {⟩}_E)⊢M:A@(\ell ,E)$$\mathrm{\Gamma },\mathsf{lock}({\mu }_F),x{:}_{{\mathsf{id}}_E}{◻}_{\mu \circ ⟨\ell ⟩}A⊢N:B@E$$\mathrm{\Sigma }(\ell )=A^{\prime }⇝B^{\prime }$$\mathrm{\Gamma },\mathsf{lock}({\mu }_F),p:A^{\prime },r:{◻}_{\mu }(B^{\prime }\to B)⊢N^{\prime }:B@E$

$\mathrm{\Gamma }⊢{\mathsf{handle}}^{\mu }M\mathsf{with}H:B@F$

Value normal forms and evaluation contexts are The unit case is the minimal repair identified in section 33.1; all other clauses reproduce source Figure 2. The complete roots are The generated label ${\ell }^{\prime }$ avoids $\mathrm{dom}(\mathrm{\Sigma },\mathrm{\Omega })$. The last contraction requires that $K$ bind no handler for $\ell$; one-step reduction is the compatible closure under $K$.

System $F_{\epsilon }$

The kinds, rows, types, contexts, values, and computations are Rows preserve duplicates and are equal modulo permutation. The judgments are $\mathrm{\Gamma }{⊢}_{v}V:A$ and $\mathrm{\Gamma }{⊢}_{c}M:A!E$. Their complete static rules are

$\mathrm{\Gamma }{⊢}_v():1$

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

$\mathrm{\Gamma }{⊢}_{v}x:A$

$\mathrm{\Gamma },\alpha :K{⊢}_{v}V:A$

$\mathrm{\Gamma }{⊢}_v\mathrm{\Lambda }{\alpha }^K.V:\mathrm{\forall }{\alpha }^K.A$

Figure 11, Appendix D.1, p. 44 of [TL26] prints $A$, rather than $\mathrm{\forall }{\alpha }^K.A$, in the conclusion of its type-abstraction rule. The displayed conclusion is the minimal well-formed repair: it is the type consumed by F-TApp and by the paper’s translation clause.

$\mathrm{\Gamma },x:A{⊢}_{c}M:B!E$

$\mathrm{\Gamma }{⊢}_v{\lambda }^E{x}^A.M:A{\to }^{E}B$

$\mathrm{\Gamma }{⊢}_{v}V:A{\to }^{E}B$$\mathrm{\Gamma }{⊢}_{v}W:A$

$\mathrm{\Gamma }{⊢}_{c}VW:B!E$

$\mathrm{\Gamma }{⊢}_{v}V:A$

$\mathrm{\Gamma }{⊢}_c\mathsf{return}V:A!E$

$\mathrm{\Gamma }{⊢}_{v}V:\mathrm{\forall }{\alpha }^K.B$$\mathrm{\Gamma }⊢A:K$

$\mathrm{\Gamma }{⊢}_{c}VA:B[A/\alpha ]!E$

$\mathrm{\Gamma }{⊢}_{c}M:A!E$$\mathrm{\Gamma },x:A{⊢}_{c}N:B!E$

$\mathrm{\Gamma }{⊢}_c\mathsf{let}x=M\mathsf{in}N:B!E$

$\mathrm{\Sigma }(\ell )=A⇝B$$\mathrm{\Gamma }{⊢}_{v}V:A$

$\mathrm{\Gamma }{⊢}_c\mathsf{do}\ell V:B!(\ell ,E)$

$\mathrm{\Sigma }(\ell )=A^{\prime }⇝B^{\prime }$$\mathrm{\Gamma },p:A^{\prime },r:B^{\prime }{\to }^{E}A{⊢}_{c}N:A!E$

$\mathrm{\Gamma }{⊢}_v\mathsf{handler}\{\ell pr\mapsto N\}:(1{\to }^{\ell ,E}A){\to }^{E}A$

Runtime computations add $\mathsf{handle}M\mathsf{with}H$, with contexts $$R::=[]\mid \mathsf{let}x=R\mathsf{in}N\mid \mathsf{handle}R\mathsf{with}H.$$ The complete roots of Figure 12, Appendix D.1, pp. 44–45 are The final root requires $\ell \notin \mathrm{bl}(R)$ and $(\ell pr\mapsto N)\in H$; reduction is closed under $R$.

System $C$

The exact static grammar is System $C$ has judgments $\mathrm{\Gamma }{⊢}_{v}V:A$, $\mathrm{\Gamma }{⊢}_{b}P:T\mid C$, and $\mathrm{\Gamma }{⊢}_{c}M:A\mid C$. The complete static rules are

$\mathrm{\Gamma }{⊢}_v():1$

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

$\mathrm{\Gamma }{⊢}_{v}x:A$

$\mathrm{\Gamma }{⊢}_{b}P:T\mid C$

$\mathrm{\Gamma }{⊢}_v\mathsf{box}P:T@C$

$f{:}^{\ast }T\in \mathrm{\Gamma }$

$\mathrm{\Gamma }{⊢}_{b}f:T\mid \{f\}$

$f{:}^{C}T\in \mathrm{\Gamma }$

$\mathrm{\Gamma }{⊢}_{b}f:T\mid C$

$\mathrm{\Gamma }{⊢}_{v}V:T@C$

$\mathrm{\Gamma }{⊢}_b\mathsf{unbox}V:T\mid C$

$\mathrm{\Gamma },\overline{x}:\overline{A},\overline{f}{:}^{\ast }\overline{T}{⊢}_{c}M:B\mid C\cup \{\overline{f}\}$

$\mathrm{\Gamma }{⊢}_b\{(\overline{x};\overline{f})\Rightarrow M\}:(\overline{A};\overline{f}:\overline{T})\Rightarrow B\mid C$

$\mathrm{\Gamma }{⊢}_{b}P:T\mid C^{\prime }$$C^{\prime }\subseteq C$

$\mathrm{\Gamma }{⊢}_{b}P:T\mid C$

$\mathrm{\Gamma }{⊢}_{v}V:A$

$\mathrm{\Gamma }{⊢}_c\mathsf{return}V:A\mid \varnothing$

$\mathrm{\Gamma }{⊢}_{b}P:(\overline{A};\overline{f}:\overline{T})\Rightarrow B\mid C$$(\mathrm{\Gamma }{⊢}_v{V}_i:A_i{)}_i$$(\mathrm{\Gamma }{⊢}_b{Q}_j:T_j\mid C_j{)}_j$

$\mathrm{\Gamma }{⊢}_{c}P(\overline{V};\overline{Q}):B[\overline{C}/\overline{f}]\mid C\cup \bigcup _j{C}_j$

$\mathrm{\Gamma }{⊢}_{c}M:A\mid C$$\mathrm{\Gamma },x:A{⊢}_{c}N:B\mid C^{\prime }$

$\mathrm{\Gamma }{⊢}_c\mathsf{let}x=M\mathsf{in}N:B\mid C\cup C^{\prime }$

$\mathrm{\Gamma }{⊢}_{b}P:T\mid C^{\prime }$$\mathrm{\Gamma },f{:}^{C^{\prime }}T{⊢}_{c}N:A\mid C$

$\mathrm{\Gamma }{⊢}_c\mathsf{def}f=P\mathsf{in}N:A\mid C$

$\mathrm{\Gamma }{⊢}_{c}M:A\mid C^{\prime }$$C^{\prime }\subseteq C$

$\mathrm{\Gamma }{⊢}_{c}M:A\mid C$

$\mathrm{\Gamma },f{:}^{\ast }((A^{\prime })\Rightarrow B^{\prime }){⊢}_{c}M:A\mid C\cup \{f\}$$\mathrm{\Gamma },p:A^{\prime },r{:}^C((B^{\prime })\Rightarrow A){⊢}_{c}N:A\mid C$

$\mathrm{\Gamma }{⊢}_c\mathsf{try}\{f^{A^{\prime }\Rightarrow B^{\prime }}\Rightarrow M\}\mathsf{with}\{p,r\mapsto N\}:A\mid C$

These are Figure 4, §5.1, p. 21 of [TL26]. The handler premise binds $f$ as tracked; its clause binds $r$ transparently with the residual capability set.

Runtime syntax extends capabilities by labels: For the operation root, abbreviate the reified deep resumption by $${\mathsf{resume}}_{\ell ,K,H}:=\{(y)\Rightarrow {\mathsf{try}}_{\ell }K[\mathsf{return}y]\mathsf{with}H\}.$$ In addition to compatible closure, the roots are Here $H=\{p,r\mapsto N\}$, the fourth root uses $\varnothing {⊢}_b{Q}_j:T_j\mid C_j$ for each actual block, the generated $\ell$ is fresh, and the last root requires $\ell \notin \mathrm{bl}(K)$. These are Figure 13, Appendix D.2, pp. 44–45 of the same source. Block beta substitutes actual blocks in terms and their capability sets in types as two distinct simultaneous components.

The two translations are the type-directed maps in section 33.2, section 33.3. They share no source judgment and must not be composed through a presumed inverse.