Effect Capabilities and Tunnelling

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Let $\mathsf{ask}:1\to \mathsf{Int}$ be an operation. Two handlers implement it: $$H_{\mathsf{out}}(())=7,H_{\mathsf{in}}(())=9.$$ A library function receives a suspended computation $q$ and evaluates it under the inner handler: $$\mathsf{underInner}(q):={\mathsf{handle}}_{H_{\mathsf{in}}}(q()).$$ Suppose $q$ is defined while the outer handler is in scope: $${\mathsf{handle}}_{H_{\mathsf{out}}}(\mathsf{let}q=\lambda ().\mathsf{ask}()\mathsf{in}\mathsf{underInner}(q)).$$ In the minimal nearest-name model, beta reduction exposes the request under the inner handler; nearest-name dispatch makes the inner clause answer it. Thus the initial program and its result are $${\mathsf{handle}}_{H_{\mathsf{out}}}(\mathsf{let}q=\lambda ().\mathsf{ask}()\mathsf{in}{\mathsf{handle}}_{H_{\mathsf{in}}}(q()))\text{and}9.$$ The lexical definition of $q$ is irrelevant to nearest-name lookup. In an authority-indexed model, write $\mathsf{ask}@H$ for a request authorized to invoke the particular handler $H$, and abbreviate $$p_{\mathsf{auth}}:={\mathsf{handle}}_{H_{\mathsf{out}}}(\mathsf{let}q=\lambda ().\mathsf{ask}@H_{\mathsf{out}}()\mathsf{in}{\mathsf{handle}}_{H_{\mathsf{in}}}(q())).$$ Identity-matched dispatch instead skips the wrong-identity inner handler, so the initial program and its result are $$p_{\mathsf{auth}}\text{and}7.$$ Both programs have the same effect presence information, namely that $\mathsf{ask}$ may occur. They differ in handler identity.

The distinction becomes sharper when the closure escapes. Give the outer handler a fresh runtime label ${\ell }_{\mathsf{out}}$, and let the returned closure retain the corresponding authority: $$\mathsf{let}q={\mathsf{handle}}_{H_{\mathsf{out}}}(\mathsf{return}(\lambda ().\mathsf{ask}@{\ell }_{\mathsf{out}}()))\mathsf{in}q().$$ Handler return removes the delimiter and beta reduction exposes an authority use with no matching active label. The initial program therefore evaluates to the displayed stuck term: $$\mathsf{let}q={\mathsf{handle}}_{H_{\mathsf{out}}}(\mathsf{return}(\lambda ().\mathsf{ask}@{\ell }_{\mathsf{out}}()))\mathsf{in}q()\text{and}\mathsf{ask}@{\ell }_{\mathsf{out}}().$$ The final term is stuck because ${\ell }_{\mathsf{out}}$ is no longer active. A sound static system must either prevent this escape or retain enough latent scope information to reject the later call.

Finally, operation equality does not imply handler equality: $$\mathsf{op}(H_{\mathsf{out}})=\mathsf{ask}=\mathsf{op}(H_{\mathsf{in}}),H_{\mathsf{out}}\ne H_{\mathsf{in}}.$$ An effect row can state $\{\mathsf{ask}\}$, but that statement alone authorizes neither handler. An effect capability is an explicit token naming authority at the call site; lexical tunnelling resolves authority instead from the lexical identity of a request.

System $\mathsf{Xi}$: capabilities as second-class blocks

The first repair makes authority explicit. The selected core is System $\mathsf{Xi}$ from Effects as Capabilities [BSO20]. Its source syntax is fine-grain call by value: expressions are pure values, statements may control the continuation, and blocks are not expression values.

The complete source rules are the following. Expression rules are ordinary:

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

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

$\mathcal{C}(v)=\tau$

$\mathrm{\Gamma }⊢v:\tau$

Blocks and statements use separate contexts:

$\mathrm{\Delta }(f)=\sigma$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢f:\sigma$

$\mathrm{\Gamma },\overline{x}:\overline{\tau }\mid \mathrm{\Delta },\overline{f}:\overline{\sigma }\mid \mathrm{\Xi }⊢s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\{(\overline{x}:\overline{\tau },\overline{f}:\overline{\sigma })\Rightarrow s\}:(\overline{\tau },\overline{\sigma })\to \tau$

$\mathrm{\Gamma }⊢e:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢e:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢s_0:{\tau }_0$$\mathrm{\Gamma },x:{\tau }_0\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢s_1:{\tau }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\mathsf{val}x=s_0;s_1:{\tau }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b:\sigma$$\mathrm{\Gamma }\mid \mathrm{\Delta },f:\sigma \mid \mathrm{\Xi }⊢s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\mathsf{def}f=b;s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b:(\overline{\tau },\overline{\sigma })\to {\tau }_0$$(\mathrm{\Gamma }⊢e_i:{\tau }_i{)}_i$$(\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b_j:{\sigma }_j{)}_j$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢b(\overline{e},\overline{b}):{\tau }_0$

$\mathrm{\Omega }(F)={\tau }_1\to {\tau }_0$$\mathrm{\Gamma }\mid \mathrm{\Delta },F:{\tau }_1\to {\tau }_0\mid \mathrm{\Xi }⊢s:\tau$$\mathrm{\Gamma },x:{\tau }_1\mid \mathrm{\Delta },k:{\tau }_0\to \tau \mid \mathrm{\Xi }⊢s_h:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢\mathsf{handle}\{F\Rightarrow s\}\mathsf{with}\{(x,k)\Rightarrow s_h\}:\tau$

The derivation-indexed runtime interface and label invariant are:

$\mathrm{\Xi }={\mathrm{\Xi }}_0,\ell :\tau ,{\mathrm{\Xi }}_{+}$$\mathrm{\Gamma },x:{\tau }_1\mid \mathrm{\Delta },k:{\tau }_0\to \tau \mid {\mathrm{\Xi }}_0⊢s_h:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢{\mathsf{cap}}_{\ell }\{(x,k)\Rightarrow s_h\}:{\tau }_1\to {\tau }_0$

$\ell \notin \mathrm{dom}(\mathrm{\Xi })$$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi },\ell :\tau ⊢s:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Xi }⊢{\mathrm{\#}}_{\ell }\{s\}:\tau$

The decomposition in X-Cap records the capability’s allocation origin. Its stored body is typed in the birth prefix ${\mathrm{\Xi }}_0$, outside both its own delimiter and every later delimiter in ${\mathrm{\Xi }}_{+}$. The capability newly bound in the handled premise is therefore not in scope in its own clause; the only way to reenter that same delimiter is through continuation $k$, which reinstalls it. A same-spelled capability already present in the outer block context remains a distinct outer binding. Keeping the prefix, rather than merely deleting $\ell$ from an unordered set, is load bearing for preservation when a request crosses intervening delimiters. Rule X-BVar uses the rightmost lookup fixed above. Replacing it by unordered membership would admit the shadowed outer $F$ in the handled premise and would invalidate the translation argument below.

For example, assume $B=\mathsf{Int}\to \mathsf{Int}$ and $\mathrm{\Omega }(F)=\mathrm{\Delta }(F)=B$. Write $$s_{20}=\mathsf{handle}\{F\Rightarrow F(20)\}\mathsf{with}\{(x,k)\Rightarrow k(x)\}.$$ Then $$\frac{\begin{array}{c}\mathrm{\Omega }(F)=B\\ {\displaystyle \frac{\begin{array}{c}(\mathrm{\Delta },F:B)(F)=B\\ \mathrm{\Gamma }⊢20:\mathsf{Int}\end{array}}{\mathrm{\Gamma }\mid \mathrm{\Delta },F:B\mid \varnothing ⊢F(20):\mathsf{Int}}}\mathrm{X}-\mathrm{Call}\\ {\displaystyle \frac{\begin{array}{c}(\mathrm{\Delta },k:B)(k)=B\\ \mathrm{\Gamma },x:\mathsf{Int}⊢x:\mathsf{Int}\end{array}}{\mathrm{\Gamma },x:\mathsf{Int}\mid \mathrm{\Delta },k:B\mid \varnothing ⊢k(x):\mathsf{Int}}}\mathrm{X}-\mathrm{Call}\end{array}}{\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \varnothing ⊢s_{20}:\mathsf{Int}}\mathrm{X}-\mathrm{Handle}.$$ This derivation uses every source judgment: the arguments are expressions, $F$ and $k$ are blocks, and the whole program is a statement.

Why blocks are second class

The tempting escape term is $$\mathsf{handle}\{F\Rightarrow F\}\mathsf{with}\{(x,k)\Rightarrow k(x)\}.$$ It has no typing derivation. The handled body must be a statement of a value type $\tau$, but $F$ is a block variable and there is no rule that embeds a block judgment into a statement or expression judgment. Likewise, value arguments cannot be blocks, and every block result is a value type. These are three faces of the same second-class restriction.

The restriction still permits higher-order blocks. A block may receive another block as an argument and invoke it while the defining delimiter is active: What is forbidden is returning $q$ as an expression value after the handler scope ends.

System $\mathsf{Xi}$ dynamics and safety

Runtime labels are generated by handlers. General evaluation contexts and contexts delimited with respect to $\ell$ are Thus $H_{\ell }$ contains no delimiter labelled $\ell$. The complete root contractions are Handler allocation is the fresh-label contraction Capability capture substitutes both the request argument and a reified continuation: The handler rule chooses $\ell$ fresh. Reduction $⟶$ is compatible closure under $H$. A capability call is not a redex by itself; it reduces only together with the matching delimiter.

The earlier example calculates as follows: The continuation reinstalls the delimiter, which is why the handler is deep.

The naive escaped capability $$H_{\ell }[{\mathsf{cap}}_{\ell }\{(x,k)\Rightarrow s\}(v)]$$ is stuck when there is no surrounding ${\mathrm{\#}}_{\ell }$. The label context is introduced precisely to prove that a closed source program cannot reduce to such a term.

The safety proof needs the usual structural lemmas. They are stated for all three judgments simultaneously. A block substitution on a derivation is scope respecting when, at every X-Cap subderivation labelled $\ell$, its restriction to the free block variables of the stored handler body is typable under the birth prefix ${\mathrm{\Xi }}_0$ displayed by that rule. Source substitutions are scope respecting because source blocks contain no labels. The substitutions created by the reduction rules are scope respecting because X-Handle-beta chooses $\ell$ fresh and the capability binding introduced for the handled occurrences of $F$ is absent from its own clause; any same-spelled $F$ in that clause denotes an outer binding. This is the derivation-indexed form of the second-class scope invariant.

Proof of Lemma 32.4 — Generatedness closure

Proof. Append one step to the witnessing reduction sequence. ◻

Proof of Lemma 32.5 — Ordered insertion weakening

Proof. Induct on the derivation, retaining the cut ${\mathrm{\Xi }}_L|{\mathrm{\Xi }}_R$ at which ${\mathrm{\Xi }}_s$ is inserted. Variable leaves use membership monotonicity, while block-variable leaves are unchanged because the insertion extends only $\mathrm{\Xi }$, not $\mathrm{\Delta }$. Every ordinary rule applies the induction hypotheses to its premises. For X-Cap, compare the cut with the displayed decomposition ${\mathrm{\Xi }}_0,\ell :\tau ,{\mathrm{\Xi }}_{+}$. If the cut lies in ${\mathrm{\Xi }}_0$, apply the induction hypothesis to the stored-body derivation; the enlarged prefix is the new birth prefix in the adjusted decomposition. If the cut lies at or to the right of $\ell$, adjust only that decomposition and leave the stored body under its original prefix. Thus the capability-origin invariant is preserved. For X-Delim, alpha-rename its freshly bound $\ell$ away from ${\mathrm{\Xi }}_s$, carry the same outer cut into its premise—that is, use the cut ${\mathrm{\Xi }}_L|({\mathrm{\Xi }}_R,\ell :\tau )$—and reapply X-Delim. This proves arbitrary ordered insertion; iteration proves insertion of a finite fresh block. ◻

Proof of Lemma 32.6 — Block-context exchange and identical shadowing

Proof. Induct on the derivation. For a block-variable leaf, rightmost lookup either selects a name different from the exchanged pair, selects one member with its unchanged type, or changes an old $f:\sigma$ lookup to the new $f:\sigma$ lookup. Every case has the same conclusion type. All other rules rebuild from their induction hypotheses. At X-Cap, perform the same transformation only on the block context; its recorded label birth prefix ${\mathrm{\Xi }}_0$ is unchanged, so the scope-respecting premise is preserved. ◻

Proof of Lemma 32.7 — Value and scope-respecting block substitution

Proof. Induct on the typing derivation in each clause. The variable and block-variable cases split on whether the looked-up name is the substituted name. Binder cases alpha-rename bound names first. In X-Handle, apply value substitution to the operation parameter and block substitution to the continuation. In X-Cap, use the substitution restricted to the displayed birth prefix ${\mathrm{\Xi }}_0$; scope respect is exactly the premise needed for the stored handler-body derivation. In X-Delim, alpha-renaming keeps the fresh label outside the support of the substitution, so the freshness premise is unchanged. ◻

Proof of Lemma 32.8 — Canonical forms

Proof. Invert the final typing rule. A variable conclusion is impossible in the corresponding empty variable context. The remaining expression rule produces a primitive value; the remaining block rules produce a block abstraction or a capability. In the capability case, inversion of X-Cap gives $\mathrm{\Xi }(\ell )={\tau }^{\prime }$, hence $\ell \in \mathrm{dom}(\mathrm{\Xi })$. ◻

Proof of Lemma 32.9 — Label-aware progress

Proof. Induct on the statement-typing derivation. An expression is a value by lemma 32.8. For sequencing, apply the induction hypothesis to the bound statement: a value gives X-Val-beta, a step lifts through the context, and an undelimited request remains undelimited after prefixing the sequencing context. A definition has a runtime block value by lemma 32.8 and contracts by X-Def-beta. For a closed block call, the operator and block arguments are runtime block values. A block abstraction gives X-Block-beta; item 1 of lemma 32.8 makes every ordinary value argument a primitive value, so no argument step is missing. A capability labelled $\ell$ gives the third alternative, and inversion of X-Cap puts $\ell$ in $\mathrm{dom}(\mathrm{\Xi })$. A handler gives X-Handle-beta.

For ${\mathrm{\#}}_{\ell }\{s_0\}$, apply the induction hypothesis to the premise typed under $\mathrm{\Xi },\ell :\tau$. A value gives X-Delim-ret, and a step lifts under the delimiter. If the induction hypothesis gives a request labelled $\ell$, the outer delimiter and its no-$\ell$-binding context form an X-Cap-beta redex. If the induction hypothesis gives a request labelled ${\ell }^{\prime }\ne \ell$, then prefixing ${\mathrm{\#}}_{\ell }$ preserves the no-binding condition for ${\ell }^{\prime }$, so the whole statement has the third form for the outer label ${\ell }^{\prime }\in \mathrm{dom}(\mathrm{\Xi })$. ◻

Proof of Theorem 32.10 — Progress for System Xi

Proof. Apply lemma 32.9. Its third alternative requires a label in $\mathrm{dom}(\varnothing )$ and is therefore impossible. ◻

Proof of Lemma 32.11 — Typed evaluation-context replacement

Proof. Induct on the context. For the empty context the replacement premise is the conclusion. A sequencing context uses the replacement induction hypothesis in the first premise of X-Val; its second premise is unchanged. A delimiter context uses the induction hypothesis in the premise of X-Delim; the fresh-label premise is unchanged. The grammar of $H_{\ell }$ is the same induction with the additional fact that every crossed delimiter has label different from $\ell$. ◻

Proof of Theorem 32.12 — Preservation

Proof. The three ordinary beta roots use lemma 32.7.

Compatible closure follows from lemma 32.11.

For X-Handle-beta, write ${\mathrm{\Xi }}_0$ for the outer label context and choose fresh $\ell$. Weakening types the handled computation under ${\mathrm{\Xi }}_0,\ell :\tau$. Its handler clause remains typed under its birth prefix ${\mathrm{\Xi }}_0$, so X-Cap, with empty later suffix, types the substituted capability at ${\tau }_1\to {\tau }_0$. The generated substitution is scope respecting: $F$ is bound only in the handled computation and is absent from its own handler clause. Block substitution types the handled body. Rule X-Delim then closes the fresh label scope.

For X-Cap-beta, write ${\mathrm{\Xi }}_0$ for the label context outside the matching delimiter. At the request occurrence, the crossed delimiters in $H_{\ell }$ form a later suffix ${\mathrm{\Xi }}_{+}$. Inversion of X-Delim and X-Cap recovers the allocation decomposition ${\mathrm{\Xi }}_0,\ell :\tau ,{\mathrm{\Xi }}_{+}$ and gives By lemma 32.11, the typed no-binding context gives, for fresh $y:{\tau }_0$, $$\mathrm{\Gamma },y:{\tau }_0\mid \mathrm{\Delta }\mid {\mathrm{\Xi }}_0⊢{\mathrm{\#}}_{\ell }\{H_{\ell }[y]\}:\tau .$$ Here lemma 32.5 first adds the fresh $y:{\tau }_0$ assumption to every inactive premise crossed while exposing the hole; context replacement then changes only the distinguished subderivation. Define the reified continuation $$K_{\ell }:=\{(y:{\tau }_0)\Rightarrow {\mathrm{\#}}_{\ell }\{H_{\ell }[y]\}\}.$$ It has type ${\tau }_0\to \tau$ under ${\mathrm{\Xi }}_0$. Simultaneous value and block substitution therefore types the reduct $s_h[v/x,K_{\ell }/k]$ at $\tau$ in the outer context, exactly as required after the delimiter disappears. The no-$\ell$-binding grammar for $H_{\ell }$ contains no inner ${\mathrm{\#}}_{\ell }$, so the reinstalled delimiter is the unique matching binder. The suffix labels occur only inside the reified continuation; they are absent from the stored handler body, exactly as its birth-prefix premise requires. The delimiter-return case follows by inversion.

It remains to verify the second conclusion. Inspect the contracted root and then induct outward through its evaluation context. Ordinary beta roots introduce no capability. At X-Handle-beta, freshness of $\ell$ and separation of the handled premise from the clause give the stored body exactly its outer birth prefix. At X-Cap-beta, the no-$\ell$-binding context reifies a continuation whose delimiter restores the same allocation point; the stored clause stays under its recorded prefix. Delimiter return removes a label and no stored body. Context replacement preserves these facts at each outer frame. ◻

Proof of Corollary 32.13 — System Xi label safety

Proof. The closed source typing gives ${\mathsf{Gen}}_{\mathrm{\Omega }}$ at the initial state. Apply lemma 32.4 and preservation at each step, then progress. Thus no reachable nonvalue is stuck on an undelimited System-$\mathsf{Xi}$ capability. ◻

Effekt: requirements translated to capabilities

Effekt replaces explicit System-$\mathsf{Xi}$ capability blocks and runtime labels by a source effect judgment. A closed set of operation names records the capabilities required from the context; the translation later restores one explicit capability parameter for each required name.

Expression typing is the same as in System $\mathsf{Xi}$. The complete statement rules are

$\mathrm{\Gamma }⊢e:\tau$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢e:\tau \mid \varnothing$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s_0:{\tau }_0\mid {\epsilon }_0$$\mathrm{\Gamma },x:{\tau }_0\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s_1:{\tau }_1\mid {\epsilon }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{val}x=s_0;s_1:{\tau }_1\mid {\epsilon }_0\cup {\epsilon }_1$

$\mathrm{\Gamma },\overline{x}:\overline{\tau }\mid \mathrm{\Delta },\overline{g}:\overline{\sigma }\mid \mathrm{\Sigma }⊢s_0:{\tau }_0\mid {\epsilon }_0^{\prime }$$\mathrm{\Gamma }\mid \mathrm{\Delta },f:(\overline{\tau },\overline{\sigma })\to {\tau }_0/{\epsilon }_0\mid \mathrm{\Sigma }⊢s:\tau \mid \epsilon$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{def}f(\overline{x}:\overline{\tau },\overline{g}:\overline{\sigma }):{\tau }_0/{\epsilon }_0=s_0;s:\tau \mid ({\epsilon }_0^{\prime }\setminus {\epsilon }_0)\cup \epsilon$

where ${\epsilon }_0^{\prime }$ is the inferred effect set of the body. The block closes over ${\epsilon }_0^{\prime }\setminus {\epsilon }_0$ at its definition site, and its declared type requires callers to provide every capability in ${\epsilon }_0$. There is deliberately no premise requiring every member of ${\epsilon }_0$ to occur in ${\epsilon }_0^{\prime }$: an unused annotated effect becomes an unused capability parameter, admitted by weakening. An implementation may warn about it, but must not reject it in this calculus.

For example, with $\mathrm{\Sigma }(\mathsf{Ask})=1\to \mathsf{Int}$, the block $$\mathsf{def}f():\mathsf{Int}/\{\mathsf{Ask}\}=7;f()$$ is typable. Its body has inferred effect $\varnothing$, so ${\epsilon }_0^{\prime }\setminus {\epsilon }_0=\varnothing$, while the call uses the declared set $\{\mathsf{Ask}\}$. Adding the tempting premise ${\epsilon }_0\subseteq {\epsilon }_0^{\prime }$ would reject this harmless unused capability and would invalidate effect weakening for block annotations.

$\mathrm{\Delta }(f)=(\overline{\tau },\overline{\sigma })\to \tau /\epsilon$$(\mathrm{\Gamma }⊢e_i:{\tau }_i{)}_i$$(\mathrm{\Delta }(g_j)={\sigma }_j{)}_j$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢f(\overline{e},\overline{g}):\tau \mid \epsilon$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma },F:{\tau }_1\to {\tau }_0⊢s:\tau \mid \epsilon$$F\notin \epsilon$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{effect}F(x:{\tau }_1):{\tau }_0;s:\tau \mid \epsilon$

$\mathrm{\Sigma }(F)={\tau }_1\to {\tau }_0$$\mathrm{\Gamma }⊢e:{\tau }_1$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{do}F(e):{\tau }_0\mid \{F\}$

$\mathrm{\Sigma }(F)={\tau }_1\to {\tau }_0$$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢s:\tau \mid \epsilon$$\mathrm{\Gamma },x:{\tau }_1\mid \mathrm{\Delta },\mathsf{resume}:{\tau }_0\to \tau /\varnothing \mid \mathrm{\Sigma }⊢s_h:\tau \mid {\epsilon }_h$

$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{try}\{s\}\mathsf{with}F\{(x:{\tau }_1)\Rightarrow s_h\}:\tau \mid (\epsilon \setminus \{F\})\cup {\epsilon }_h$

The continuation is contextually pure: it is a second-class block whose own control effects are handled outside the operation clause.

Let $s_{\mathsf{ask}}$ abbreviate $$\mathsf{try}\{\mathsf{do}\mathsf{Ask}(())\}\mathsf{with}\mathsf{Ask}\{(u:1)\Rightarrow \mathsf{resume}(7)\}.$$ For the derivation only, abbreviate $${\mathrm{\Sigma }}_A:=\mathrm{\Sigma },\mathsf{Ask}:1\to \mathsf{Int},{\mathrm{\Delta }}_r:=\mathrm{\Delta },\mathsf{resume}:\mathsf{Int}\to \mathsf{Int}/\varnothing .$$ The complete source derivation is assembled from the request and resumption subderivations $$\frac{\begin{array}{c}\mathsf{Ask}:1\to \mathsf{Int}\in {\mathrm{\Sigma }}_A\\ \mathrm{\Gamma }⊢():1\end{array}}{\mathrm{\Gamma }\mid \mathrm{\Delta }\mid {\mathrm{\Sigma }}_A⊢\mathsf{do}\mathsf{Ask}(()):\mathsf{Int}\mid \{\mathsf{Ask}\}}\mathrm{E}-\mathrm{Do}{\mathcal{D}}_{\mathsf{do}}$$ and $$\frac{\begin{array}{c}{\mathrm{\Delta }}_r(\mathsf{resume})=\mathsf{Int}\to \mathsf{Int}/\varnothing \\ \mathrm{\Gamma },u:1⊢7:\mathsf{Int}\end{array}}{\mathrm{\Gamma },u:1\mid {\mathrm{\Delta }}_r\mid {\mathrm{\Sigma }}_A⊢\mathsf{resume}(7):\mathsf{Int}\mid \varnothing }\mathrm{E}-\mathrm{Call}{\mathcal{D}}_{\mathsf{resume}}.$$ Using ${\mathcal{D}}_{\mathsf{do}}$ and ${\mathcal{D}}_{\mathsf{resume}}$ as the two E-Try premises gives $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathsf{Ask}:1\to \mathsf{Int}\in {\mathrm{\Sigma }}_A\\ {\mathcal{D}}_{\mathsf{do}}\\ {\mathcal{D}}_{\mathsf{resume}}\end{array}}{\mathrm{\Gamma }\mid \mathrm{\Delta }\mid {\mathrm{\Sigma }}_A⊢s_{\mathsf{ask}}:\mathsf{Int}\mid \varnothing }}\mathrm{E}-\mathrm{Try}\\ \mathsf{Ask}\notin \varnothing \end{array}}{\mathrm{\Gamma }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }⊢\mathsf{effect}\mathsf{Ask}(u:1):\mathsf{Int};s_{\mathsf{ask}}:\mathsf{Int}\mid \varnothing }\mathrm{E}-\mathrm{Effect}.$$ Rule E-Do introduces the requirement, E-Try removes it and types its resumption block, and E-Effect discharges the operation name from the signature context.

The named Effekt-to-System-$\mathsf{Xi}$ translation

Fix a canonical ordering of every effect set. Write $\mathsf{CapTy}$, $\mathsf{CapEff}$, and ${\mathsf{CapStmt}}_{\mathrm{\Sigma },\mathrm{\Delta }}$ for the syntax translations; these are not semantic interpretations. Value types and expressions are unchanged. If $\mathrm{\Sigma }(F)={\tau }_1\to {\tau }_0$, put $${\mathsf{CapOp}}_{\mathrm{\Sigma }}(F):={\tau }_1\to {\tau }_0.$$ For $\overline{F}=F_1,\dots ,F_n$, let $$\overline{{\mathsf{CapOp}}_{\mathrm{\Sigma }}(\overline{F})}:={\mathsf{CapOp}}_{\mathrm{\Sigma }}(F_1),\dots ,{\mathsf{CapOp}}_{\mathrm{\Sigma }}(F_n).$$ Then The statement translation is directed by the source typing derivation. Its subscript records the signature and the current source block context: the call clause reads the ordered effect list $\overline{F}$ from $\mathrm{\Delta }(f)$, while a recursive call under a binder uses the extended current context. The fixed canonical ordering makes this context-directed translation deterministic. Its homomorphic clauses are Block definitions receive the ordered capabilities explicitly: Handlers bind the operation capability and resumption: The block-call clause uses the ordered effects in the declared type of $f$.

The complete handler example uses the earlier abbreviation $s_{\mathsf{ask}}$ and translates to The operation declaration disappears, the request becomes an ordinary block call, and the handler explicitly binds the capability block. Set the System-$\mathsf{Xi}$ operation signature to $\mathrm{\Omega }(\mathsf{op})=\mathrm{\Sigma }(\mathsf{op})$ for every Effekt operation. Thus if $\mathrm{\Sigma }(\mathsf{op})=A\to B$, the translated X-Handle premise uses parameter type $A$ and resumption-result type $B$, exactly as E-Try requires.

Proof of Theorem 32.15 — Effekt-to-System- Xi type preservation

Proof. Induct on the Effekt typing derivation. The expression and sequencing cases are homomorphic, using target weakening to place both translated premises under the union of their capability contexts.

For E-Def, write the annotated effects as ${\epsilon }_0$ and the inferred body effects as ${\epsilon }_0^{\prime }$. The induction hypothesis types the translated body under $${\mathsf{CapTy}}_{\mathrm{\Sigma }}(\mathrm{\Delta },\overline{g}:\overline{\sigma }),{\mathsf{CapEff}}_{\mathrm{\Sigma }}({\epsilon }_0^{\prime }).$$ Decompose the last context into the definition-site capabilities ${\mathsf{CapEff}}_{\mathrm{\Sigma }}({\epsilon }_0^{\prime }\setminus {\epsilon }_0)$ and the formal capability parameters ${\mathsf{CapEff}}_{\mathrm{\Sigma }}({\epsilon }_0)$. Add a genuinely fresh formal by lemma 32.5; if its name already occurs at the same closed operation type, use identical shadowing from lemma 32.6. Exchange distinct adjacent bindings to restore the canonical order. Rule X-Block therefore gives exactly ${\mathsf{CapTy}}_{\mathrm{\Sigma }}((\overline{\tau },\overline{\sigma })\to {\tau }_0/{\epsilon }_0)$. The continuation induction hypothesis is typed under ${\mathsf{CapEff}}_{\mathrm{\Sigma }}(\epsilon )$. Weakening both premises to ${\mathsf{CapEff}}_{\mathrm{\Sigma }}(({\epsilon }_0^{\prime }\setminus {\epsilon }_0)\cup \epsilon )$ and applying X-Def proves the case. In E-Call, the declared source block type fixes the same canonical order of capability arguments, so X-Call applies.

Translation erases E-Effect. Its side condition $F\notin \epsilon$ gives ${\mathsf{CapEff}}_{\mathrm{\Sigma }}(\epsilon \cup \{F\})={\mathsf{CapEff}}_{\mathrm{\Sigma }}(\epsilon ),F:{\mathsf{CapTy}}_{\mathrm{\Sigma }}(F)$, so the premise already has the conclusion’s translated capability assumptions. Rule E-Do becomes X-Call on the capability block $F$. For E-Try, put $$\mathrm{\Theta }:={\mathsf{CapTy}}_{\mathrm{\Sigma }}(\mathrm{\Delta }),{\mathsf{CapEff}}_{\mathrm{\Sigma }}((\epsilon \setminus \{F\})\cup {\epsilon }_h).$$ The handled-statement induction hypothesis is typed under $${\mathsf{CapTy}}_{\mathrm{\Sigma }}(\mathrm{\Delta }),{\mathsf{CapEff}}_{\mathrm{\Sigma }}(\epsilon ).$$ Since ${\mathsf{CapEff}}_{\mathrm{\Sigma }}(\epsilon \setminus \{F\})\subseteq \mathrm{\Theta }$, weakening adds the fresh capabilities in $\mathrm{\Theta }$. Exchange moves distinct bindings into canonical order. Append $F:{\tau }_1\to {\tau }_0$ on the right; identical shadowing from lemma 32.6 preserves the derivation whether or not ${\epsilon }_h$ already contributed an outer $F$, and rightmost lookup selects the handled binding. The handler-clause induction hypothesis is typed under $${\mathsf{CapTy}}_{\mathrm{\Sigma }}(\mathrm{\Delta }),{\mathsf{CapEff}}_{\mathrm{\Sigma }}({\epsilon }_h),\mathsf{resume}:{\tau }_0\to \tau ,$$ and weakens to $\mathrm{\Theta },\mathsf{resume}:{\tau }_0\to \tau$. Rule X-Handle therefore yields the translated conclusion under exactly $\mathrm{\Theta }$. No translation clause creates a runtime label, so the target label context is empty. ◻

Proof of Corollary 32.16 — Effekt effect safety

Proof. By theorem 32.15, the translation is closed and typed under an empty label context. Put $\mathrm{\Omega }(\mathsf{op})=\mathrm{\Sigma }(\mathsf{op})$. No clause of ${\mathsf{CapStmt}}_{\mathrm{\Sigma },\mathrm{\Delta }}$ introduces ${\mathsf{cap}}_{\ell }$ or ${\mathrm{\#}}_{\ell }$, so $s_0={\mathsf{CapStmt}}_{\mathrm{\Sigma },\mathrm{\Delta }}(s)$ is the source witness in definition 32.2; the reflexive zero-step trace proves ${\mathsf{Gen}}_{\mathrm{\Omega }}(s_0)$. Use lemma 32.4, theorem 32.12, theorem 32.10 at each execution step. This corollary belongs to the selected Effekt source language through its translation. It is not a theorem about every feature of the full Effekt implementation. ◻

Effect tunnelling: lexical handler identity

Capability passing forbids a capability from escaping by making blocks second class. Tunnelling takes another route: first-class functions may carry latent capability effects, and each request names the handler it intends to invoke. The calculus is independent of System $\mathsf{Xi}$; no translation between them is assumed.

The selected signature makes its formation, ordinary typing, partial-order, and characteristic tunnelling rules explicit.

The well-formedness layer makes every effect constructor explicit:

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\varnothing \mathsf{effects}$

$\alpha \in \mathrm{\Delta }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\alpha \mathsf{effects}$

$\ell \in \mathrm{dom}(\mathrm{\Xi })$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\ell \mathsf{effects}$

$P(h)=\mathsf{F}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢h.\mathsf{lbl}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\mathsf{effects}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_2\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1,{\overline{e}}_2\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢1\mathsf{type}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathsf{Int}\mathsf{type}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\to [T{]}_{\overline{e}}\mathsf{type}$

$\mathrm{\Delta },\alpha \mid P\mid \mathrm{\Xi }⊢T\mathsf{type}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\forall }\alpha .T\mathsf{type}$

$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢T\mathsf{type}$$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\Pi }h:\mathsf{F}.[T{]}_{\overline{e}}\mathsf{type}$

For example, if $P(h)=\mathsf{F}$, then WF-HLabel, WF-Unit, and WF-Fun derive $$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢1\to [1{]}_{h.\mathsf{lbl}}\mathsf{type}.$$

The ordinary term rules are part of the selected local signature, not an implicit appeal to the simply typed lambda calculus:

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢():[1{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢n:[\mathsf{Int}{]}_{\varnothing }$

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

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢x:[T{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:S\mid \mathrm{\Xi }⊢t:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\lambda x:S.t:[S\to [T{]}_{\overline{e}}{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_1:[S\to [T{]}_{\overline{e}}{]}_{\overline{e}}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_2:[S{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_1{t}_2:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t_1:[S{]}_{\overline{e}}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:S\mid \mathrm{\Xi }⊢t_2:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\mathsf{let}x:S=t_1\mathsf{in}{t}_2:[T{]}_{\overline{e}}$

$\mathrm{\Delta },\alpha \mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\mathrm{\Lambda }\alpha .t:[\mathrm{\forall }\alpha .T{]}_{\varnothing }$

The compatibility family covers the displayed formation, ordinary typing, partial-order, and characteristic tunnelling rules. For T-Let, its compatibility case uses evaluation-context composition. Application and let use one common premise effect; the union-effect forms used later are derived by subsuming premises to a common join. Two preorders are part of the calculus. Type subtyping is the least transitive relation generated by

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢1\le 1$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathsf{Int}\le \mathsf{Int}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_2\le T_1$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢S_1\le S_2$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\to [S_1{]}_{{\overline{e}}_1}\le T_2\to [S_2{]}_{{\overline{e}}_2}$

$\mathrm{\Delta },\alpha \mid P\mid \mathrm{\Xi }⊢T_1\le T_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\forall }\alpha .T_1\le \mathrm{\forall }\alpha .T_2$

$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢T_1\le T_2$$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\mathrm{\Pi }h:\mathsf{F}.[T_1{]}_{{\overline{e}}_1}\le \mathrm{\Pi }h:\mathsf{F}.[T_2{]}_{{\overline{e}}_2}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\le T_2$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_2\le T_3$

$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\le T_3$

Effect inclusion is generated by $$\frac{\begin{array}{c}(\mathrm{\forall }j)(\mathrm{\exists }i).e_{1j}=e_{2i}\\ (\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢e_{2i}\mathsf{effects}{)}_i\end{array}}{\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2}\mathrm{Eff}-\mathrm{Sub},$$ where each $e_{2i}$ is read as a singleton effect sequence in the declared $\mathsf{effects}$ judgment. This formulation makes function domains contravariant, results and latent effects covariant, and both quantified forms pointwise. The term rule is $$\frac{\begin{array}{c}\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T_1{]}_{{\overline{e}}_1}\\ \mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T_1\le T_2\\ \mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢{\overline{e}}_1\le {\overline{e}}_2\end{array}}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T_2{]}_{{\overline{e}}_2}}\mathrm{T}-\mathrm{Sub}.$$ The judgments are declarative: Eff-Sub compares normalized finite sets, type subtyping is the reflexive–transitive closure of its structural generators, and T-Sub may occur at any typing boundary. These rules alone do not define a principal-type algorithm or a unique placement of subsumption. When the finite effect preorder has the join ${\overline{e}}^{\star }=\overline{e}\cup {\overline{e}}_1\cup {\overline{e}}_2$, subsume a function computation, its latent result effect, and its argument to ${\overline{e}}^{\star }$, then apply T-App; the conclusion has effect ${\overline{e}}^{\star }$. For sequencing, subsume both T-Let premises to $\overline{e}\cup {\overline{e}}_1\cup {\overline{e}}_2$ derives sequencing at that union effect. Neither union-effect rule is primitive. The purity premise of T-EAbs is the selected source calculus’s explicit restriction on computations directly quantified by an effect variable; a body with an immediate nonempty effect cannot be hidden by effect abstraction.

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[\mathrm{\forall }\alpha .T{]}_{{\overline{e}}_0}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t[\overline{e}]:[T[\overline{e}/\alpha ]{]}_{{\overline{e}}_0}$

$\mathrm{\Delta }\mid P,h:\mathsf{F}\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[T{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\lambda h:\mathsf{F}.t:[\mathrm{\Pi }h:\mathsf{F}.[T{]}_{\overline{e}}{]}_{\varnothing }$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[\mathrm{\Pi }h:\mathsf{F}.[T{]}_{\overline{e}}{]}_{{\overline{e}}_0}$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid e$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢th:[T[h]{]}_{\overline{e}[h],{\overline{e}}_0}$

Here $T[h]$ and $\overline{e}[h]$ replace the bound handler variable by its argument and replace $h.\mathsf{lbl}$ by the argument label. The four characteristic handler and tunnelling rules are

$P(h)=\mathsf{F}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid h.\mathsf{lbl}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid e$$\mathsf{op}(\mathsf{F})=T\to S$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\Uparrow h:[T\to [S{]}_e{]}_{\varnothing }$

$\mathrm{\Xi }(\ell )=[S{]}_{\overline{e}}$$\mathsf{op}(\mathsf{F})=T_1\to T_2$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:T_1,k:T_2\to [S{]}_{\overline{e}}\mid \mathrm{\Xi }⊢t:[S{]}_{\overline{e}}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢({\mathsf{handler}}^{\mathsf{F}}xk.t{)}^{\ell }:\mathsf{F}\mid \ell$

$\ell \notin \mathrm{dom}(\mathrm{\Xi })$$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi },\ell :[T{]}_{\overline{e}}⊢t:[T{]}_{\overline{e},\ell }$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢T\mathsf{type}$$\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢\overline{e}\mathsf{effects}$

$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢{\Downarrow }_{[T{]}_{\overline{e}}}^{\ell }t:[T{]}_{\overline{e}}$

The first side condition on T-Down states $\ell \notin \mathrm{dom}(\mathrm{\Xi })$. The two well-formedness premises are checked under $\mathrm{\Xi }$, which does not contain $\ell$; by WF-Label, they imply $\ell \notin \mathrm{fl}(T,\overline{e})$. This derived fact is the region-capability restriction: the fresh label may occur while the guarded term executes, but may not escape in the result type or residual effects.

For a complete use of both judgments, assume $P(h)=\mathsf{F}$ and $\mathsf{op}(\mathsf{F})=1\to \mathsf{Int}$. Then $$\frac{\begin{array}{c}\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢1\mathsf{type}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{P(h)=\mathsf{F}}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid h.\mathsf{lbl}}}\mathrm{T}-\mathrm{HVar}\\ \mathsf{op}(\mathsf{F})=1\to \mathsf{Int}\end{array}}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢\Uparrow h:[1\to [\mathsf{Int}{]}_{h.\mathsf{lbl}}{]}_{\varnothing }}}\mathrm{T}-\mathrm{Up}\\ 1\to [\mathsf{Int}{]}_{h.\mathsf{lbl}}\le 1\to [\mathsf{Int}{]}_{h.\mathsf{lbl}}\\ \varnothing \le h.\mathsf{lbl}\end{array}}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢\Uparrow h:[1\to [\mathsf{Int}{]}_{h.\mathsf{lbl}}{]}_{h.\mathsf{lbl}}}}\mathrm{T}-\mathrm{Sub}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{x:1\in \mathrm{\Gamma },x:1}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢x:[1{]}_{\varnothing }}}\mathrm{T}-\mathrm{Var}\\ 1\le 1\\ \varnothing \le h.\mathsf{lbl}\end{array}}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢x:[1{]}_{h.\mathsf{lbl}}}}\mathrm{T}-\mathrm{Sub}\end{array}}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢\Uparrow hx:[\mathsf{Int}{]}_{h.\mathsf{lbl}}}}\mathrm{T}-\mathrm{App}\end{array}}{\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\lambda x:1.\Uparrow hx:[1\to [\mathsf{Int}{]}_{h.\mathsf{lbl}}{]}_{\varnothing }}\mathrm{T}-\mathrm{Lam}.$$ The handler judgment derives the effect $h.\mathsf{lbl}$, the term judgment records it as a latent function effect, and the enclosing lambda itself is a value with no immediate effect.

A handler definition is paired with the label introduced by the surrounding $\Downarrow$. Substituting $H^{\ell }$ for a handler variable $h$ also substitutes $\ell$ for $h.\mathsf{lbl}$. Thus handler identity is lexical, not just an operation name.

A request crosses an intervening handler

In the operational displays below, the result annotation ${}_{[T{]}_{\overline{e}}}$ on a delimiter is suppressed when it is determined by the typing derivation. Values and evaluation contexts are Define the no-binding judgment $\ell ⇝̸K$ by structural recursion on this grammar: $$\begin{array}{c}\ell ⇝̸[],\\ \ell ⇝̸Kt,\ell ⇝̸vK,\ell ⇝̸K[\overline{\ell }],\ell ⇝̸K{H}^{{\ell }^{\prime }}\text{if }\ell ⇝̸K,\\ \ell ⇝̸\mathsf{let}x:T=K\mathsf{in}t\text{if }\ell ⇝̸K,\\ \ell ⇝̸{\Downarrow }^{{\ell }^{\prime }}K\text{if }\ell \ne {\ell }^{\prime }\text{ and }\ell ⇝̸K.\end{array}$$ These clauses are exhaustive: only the delimiter frame binds a runtime label. Reduction is compatible closure under $K$. Besides ordinary beta and let rules, the roots are where $H={\mathsf{handler}}^{\mathsf{F}}xk.t$, $\mathsf{op}(\mathsf{F})=T_1\to T_2$, and the context $K$ does not bind $\ell$. In particular, $K$ may contain ${\Downarrow }^{{\ell }^{\prime }}$ for ${\ell }^{\prime }\ne \ell$.

Let $$H_o={\mathsf{handler}}^{\mathsf{F}}xk.k(7),H_i={\mathsf{handler}}^{\mathsf{F}}xk.k(9),$$ and abbreviate the two-request body by $$B(h_o,h_i):=\mathsf{let}z:\mathsf{Int}=\Uparrow h_i()\mathsf{in}\Uparrow h_o().$$ The tunneled program first invokes the inner handler and then uses the outer handler authority while the inner delimiter is still dynamically active: Under $h_o:\mathsf{F},h_i:\mathsf{F}$, the two requests have effects $h_i.\mathsf{lbl}$ and $h_o.\mathsf{lbl}$, respectively. Thus the let body has effects $h_i.\mathsf{lbl},h_o.\mathsf{lbl}$. The inner handler application replaces $h_i.\mathsf{lbl}$ by ${\ell }_i$, and its delimiter discharges ${\ell }_i$, leaving the still-abstract effect $h_o.\mathsf{lbl}$. The outer T-HApp then replaces $h_o.\mathsf{lbl}$ by ${\ell }_o$, which the outer delimiter discharges. Hence $$\varnothing \mid \varnothing \mid \varnothing \mid \varnothing ⊢t_{\mathsf{tun}}:[\mathsf{Int}{]}_{\varnothing }.$$ Two handler-beta steps expose $${\Downarrow }^{{\ell }_o}({\Downarrow }^{{\ell }_i}(\mathsf{let}z:\mathsf{Int}=\Uparrow H_i^{{\ell }_i}()\mathsf{in}\Uparrow H_o^{{\ell }_o}())).$$ The inner request is handled first and resumes with $9$. After the let binding is discharged, the remaining request is $\Uparrow H_o^{{\ell }_o}()$ inside the ${\ell }_i$-delimiter. Since that delimiter binds ${\ell }_i$, not ${\ell }_o$, it belongs to the permitted context $K$ of Tun-Down-up. The outer request therefore crosses the intervening same-operation handler, reaches $H_o^{{\ell }_o}$, and returns $7$. Nearest-name lookup on the same dynamic stack handles the second request at $H_i^{{\ell }_i}$ and returns $9$. Tunnelling changes the matching key from the operation signature to lexical handler identity.

The tunnelling logical relation

A naive logical relation would define the handler interpretation by structural recursion on the operation signature. Recursive signatures defeat that plan. Let $$\mathsf{op}(\mathsf{F})=1\to \mathrm{\Pi }h:\mathsf{F}.[T{]}_{h.\mathsf{lbl}},R:=\lambda h:\mathsf{F}.(\Uparrow h())h,$$ and let $$H:={\mathsf{handler}}^{\mathsf{F}}xk.k(R).$$ Then the closed term ${\Downarrow }^{\ell }(R{H}^{\ell })$ repeats: The naive clause for $\mathcal{H}[[\mathsf{F}]]$ must interpret the handler-polymorphic result, whose $\mathcal{V}$-clause asks for $\mathcal{H}[[\mathsf{F}]]$ again. The recursive call is not on a smaller type. The source repairs exactly this failed definition with a step-indexed logic and the later modality $▹$. Recursive handler interpretations occur under one later; Löb induction allows $▹P$ as the hypothesis when proving $P$, and monotonicity removes one later from assumptions and conclusion together.

The observation relation is asymmetric termination approximation: For closed terms, evaluation contexts, and potentially effect-stuck terms, define the biorthogonal relations The smaller relation $\mathcal{S}$ is not an informal exception to biorthogonality. It has the exact closure condition Thus a pair of isolated requests may be stuck, but every related outcome must become a related computation after plugging it back into contexts that do not bind the request labels.

The structural value relation is The handler relation unfolds one clause under related arguments and related continuations:

Finally, the semantic effect relation records both request forms and their outcomes. For an effect variable, The primed sequences are the syntactic substitutions carried by $\delta$; the semantic component $\varphi$, rather than syntactic equality with those sequences, decides whether the currently exposed labels and outcomes are related. For a concrete capability effect $e\in \{\ell ,h.\mathsf{lbl}\}$, let ${\rho }_i(e)$ replace handler-label projections on side $i$ and leave a concrete label unchanged. Then The request clause is The context clause is deliberately asymmetric, matching the observation relation: Labels are interpreted by

Interpret the environments by Open term refinement is the exact closing-substitution lifting Handler refinement is

Proof of Lemma 32.19 — Delimiter compatibility

Proof. Choose one label ${\ell }_{\ast }$ fresh for $\mathrm{\Xi }$ and for the finite supports of both closing environments. Alpha-rename the bound label of T-Down to ${\ell }_{\ast }$ before applying either closing substitution. Both closed instances therefore use the same concrete name. Extend the one suppressed syntactic index on both sides by the one open entry $${\mathrm{\Xi }}^{+}:=\mathrm{\Xi },{\ell }_{\ast }:[T{]}_{\overline{e}};$$ do not form separate entries from the two closed instances of $T$ and $\overline{e}$. This common extension is required by the concrete-label clause $\mathcal{W}[[{\ell }_{\ast }]]$, which performs one lookup in ${\mathrm{\Xi }}^{+}$.

Use the premise relation at ${\mathrm{\Xi }}^{+}$. Fresh-label index weakening embeds related test contexts $K_1,K_2$ from $\mathrm{\Xi }$ into ${\mathrm{\Xi }}^{+}$. Bound labels in those contexts may be alpha-renamed away from ${\ell }_{\ast }$, so ${\ell }_{\ast }⇝̸K_i$ for both $i$. If both guarded terms terminate normally, the premise relation supplies related values at $T$, and Tun-Down-val removes the two occurrences of the common delimiter. If a guarded term exposes ${\ell }_{\ast }$, the two structural judgments above give the decomposition required by $\mathcal{S}$. Its concrete-effect clause has ${\overline{\ell }}_1={\overline{\ell }}_2=({\ell }_{\ast })$; the ${\mathcal{U}}_B$-clause contracts Tun-Down-up on both sides. The arguments use the request’s $\mathcal{V}$-premise, and the reified continuations are $\lambda y.{\Downarrow }^{{\ell }_{\ast }}{K}_i[y]$. The universally quantified outcome premise relates those continuations, and the leading $▹$ lowers the numerical index before the recursive $\mathcal{T}$-use.

The freshness discharge used in both alternatives is simultaneous strengthening of $\mathcal{T},\mathcal{K},\mathcal{S},\mathcal{V},\mathcal{U}$, and $\mathcal{W}$: if ${\ell }_{\ast }\notin \mathrm{fl}(T,\overline{e})$, restricting ${\mathrm{\Xi }}^{+}$ back to $\mathrm{\Xi }$ preserves the interpretation at $[T{]}_{\overline{e}}$. Prove it by induction on the displayed relation clauses and the numerical index. The only clause that inspects ${\mathrm{\Xi }}^{+}$ is $\mathcal{W}[[\ell ]]$. The result side condition excludes a literal ${\ell }_{\ast }$, and freshness for the supports of $\delta$ and $\rho$ excludes an effect-variable or handler-label instantiation to ${\ell }_{\ast }$; every lookup is therefore unchanged. Thus the normal-return and exposed-request alternatives establish exactly the two clauses of $\mathcal{O}$ at the original index $\mathrm{\Xi }$. ◻

Proof of Lemma 32.20 — Handler-definition compatibility

Proof. At numerical index $n$, define the candidate outcome relation $${\eta }_n(u_1,u_2):=\mathcal{T}[[[S{]}_{\overline{e}}{]]}_{\delta }^{\rho }(u_1,u_2)\text{at index }n.$$ Assume as Löb hypothesis that the two handler values satisfy $\mathcal{H}[[\mathsf{F}]]$ at every smaller index. To establish its clause at $n$, take related operation arguments $v_1,v_2$ and continuations $u_1,u_2$ preserving ${\eta }_n$ on related results. Extend the closing substitution by $x\mapsto (v_1,v_2)$ and $k\mapsto (u_1,u_2)$. The clause-body induction hypothesis yields ${\eta }_n(t_1[v_1/x,u_1/k],t_2[v_2/x,u_2/k])$. Any recursive request through the handler consults $\mathcal{W}[[\ell ]]$; its $▹\mathcal{H}$ premise asks only for index $n-1$, exactly the Löb hypothesis. This proves the displayed $\mathcal{H}$-clause and closes the induction on $n$. ◻

Proof of Lemma 32.21 — Compatibility mechanism

Proof. Proceed by induction on the typing derivation. Rule T-Unit uses the unit singleton clause, and T-Int uses the integer-equality clause; T-Var uses the related closing environment. Rule T-Sub uses type covariance and effect monotonicity: increasing the result type or effect weakens the observation required by the relation. Rule T-Lam uses the function clause of $\mathcal{V}$.

For the first nontrivial biorthogonal case, consider T-App. After fixing related closing substitutions, write $f_i$ and $u_i$ for the two closed instances of its function and argument premises. Their induction hypotheses give $$\mathcal{T}[[[S\to [T{]}_{\overline{e}}{]}_{\overline{e}}]](f_1,f_2),\mathcal{T}[[[S{]}_{\overline{e}}]](u_1,u_2).$$ To prove the conclusion, fix $K_1,K_2\in \mathcal{K}[[[T{]}_{\overline{e}}]]$. If related function values $g_1,g_2$ have already been obtained, the function clause of $\mathcal{V}$ says that $g_1{a}_1,g_2{a}_2$ are $\mathcal{T}[[[T{]}_{\overline{e}}]]$-related for every $\mathcal{V}[[S]]$-related pair $a_1,a_2$. Hence the contexts $K_i[g_i[]]$ satisfy both clauses of $\mathcal{K}[[[S{]}_{\overline{e}}]]$: the value clause uses the function relation, and the exposed-request clause is inherited by compatible closure. Applying the argument induction hypothesis gives $\mathcal{O}(K_1[g_1{u}_1],K_2[g_2{u}_2])$. Therefore the outer contexts $K_i[[]u_i]$ satisfy both clauses of $\mathcal{K}[[[S\to [T{]}_{\overline{e}}{]}_{\overline{e}}]]$. Applying the function induction hypothesis yields $\mathcal{O}(K_1[f_1{u}_1],K_2[f_2{u}_2])$, exactly the conclusion relation. This nested-context argument is the representative application pattern; it uses the common effect $\overline{e}$ in both premises.

For T-Let, related $t_1$ terms are placed in the evaluation context $\mathsf{let}x:S=[]\mathsf{in}{t}_2$; the induction hypothesis for $t_2$, under related substitutions extended at $x$, closes the context composition. Rules T-EAbs and T-EApp extend and instantiate $\delta$, while T-HAbs and T-HApp extend and instantiate $\rho$ using the quantified clauses of $\mathcal{V}$. Rule T-HVar is immediate from ${\mathcal{E}}_P$ and the $\mathcal{W}$-clause for $h.\mathsf{lbl}$.

For T-Up, related handlers and related arguments satisfy ${\mathcal{U}}_A$, hence $\mathcal{S}$; the inclusion $\mathcal{S}\subseteq \mathcal{T}$ closes the case. Lemma 32.19 supplies the complete T-Down case, including both outcome alternatives and the fresh-label discharge. Lemma 32.20 supplies the T-HDef case with its explicit candidate ${\eta }_n$ and numerical Löb descent. These cases cover every rule in the selected local signature. ◻

Proof of Lemma 32.23 — Adequacy

Source import. This is Lemma 6 (Adequacy), §5.4, article p. 5:22 (physical p. 22) of [ZM19a]. The identity contexts form a related pair in $\mathcal{K}[[[T{]}_{\varnothing }]]$: their value clause is immediate, and their $\mathcal{S}$-clause is vacuous because an empty effect sequence contains no effect that could witness an exposed related request. Unfolding $\mathcal{T}$ therefore gives the displayed observation. ◻

Proof of Corollary 32.24 — Tunnelling parametricity

Proof. Induction on the typing derivation applies lemma 32.21; the closing environments relate each bound variable to itself. The term and handler conclusions are the two displayed logical-refinement judgments. ◻

Proof of Theorem 32.25 — Tunnelling metatheorems

Source import. The two clauses map to Theorems 2–3, respectively, in §5.4, article p. 5:22 (physical p. 22) of [ZM19a]. The technical report states them in §5.4, pp. 21–22 and supplies the complete static signature and Compatibility Lemmas 7–19 in Appendix B [ZM19b].

1. Source Theorem 2 specializes the environments of corollary 32.24 to empty ones and the closed computation type $[T{]}_{\varnothing }$. Its parametricity and lemma 32.23 give the stated value-or-step alternative for every reduct.

2. Source Theorem 3 assumes the same open typing boundary on both sides. Its adequacy and congruence hypotheses quantify over the full program contexts of definition 32.22, yielding contextual refinement at that boundary and at arbitrary observation result type.

The step-indexed, biorthogonal relation and its environment interpretation are source imports; the preceding local compatibility proof establishes only that the displayed rules meet their premises. No later result in this book uses a stronger consequence. ◻

Control-flow linearity: source card.

Effect presence does not bound resumption use. For the comparison predicate, write $$\mathsf{uses}(r,M)\le q,q\in \{1,\omega \},$$ when every execution path of $M$ invokes resumption $r$ at most once for $q=1$, with no finite bound asserted for $q=\omega$. A handler that resumes twice separates this predicate from effect safety: both resumptions may target an active handler even though the linear-use judgment rejects the clause. Tang, Hillerström, Lindley, and Morris develop the source calculus and qualified-effect discipline in Soundly Handling Linearity [THLM24]. The display above is only the book’s distinguishing predicate. No syntax, rule, or theorem of that calculus is imported into System $\mathsf{Xi}$, Effekt, or ${\lambda }_{\mathsf{tun}}$.

Bidirectional control: Olaf source card.

A unidirectional operation sends an argument to its handler and receives a resumption result. Olaf permits the handler computation itself to raise statically tracked effects back toward the suspended requester. Its source judgment and configuration step are $$\mathrm{\Delta }\mid \mathrm{\Theta }\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢t:[\tau {]}_c,L;t⟶L^{\prime };t^{\prime }.$$ Lifetimes occur in effect sequences, and a continuation type records effects on both sides of control transfer. These are Olaf objects: $\mathrm{\Theta }$ is a lifetime-variable context here, $L$ is a lifetime store, and neither is the System-$\mathsf{Xi}$ translation abbreviation used above.

Theorem 32.26 — Olaf source metatheorems¶

At the exact Olaf signature, well-typed terms are logically related to themselves; closed well-typed programs are value-or-step safe at every reduct; and logical refinement implies contextual refinement.

Referenced from 2 locations

• Effect Capabilities and Tunnelling

Proof of Theorem 32.26 — Olaf source metatheorems

Source import. These are Theorems 1–3 in §6.2, article pp. 23–24 of [ZSM20]. Their hypotheses use Olaf’s worlds, fixpoint-handler relation, lifetime effects, and program contexts. They are not consequences of theorem 32.25, and they imply no translation between Olaf and System $\mathsf{Xi}$, Effekt, or ${\lambda }_{\mathsf{tun}}$. ◻

Locality: global-modality source card.

White’s locality calculus distinguishes ordinary bindings $\mathrm{\Gamma };x:\tau$ from global bindings $\mathrm{\Gamma };x{:}_{◻}\tau$. Context restriction keeps only the latter: $$\varnothing /◻=\varnothing ,(\mathrm{\Gamma };x:\tau )/◻=\mathrm{\Gamma }/◻,(\mathrm{\Gamma };x{:}_{◻}\tau )/◻=(\mathrm{\Gamma }/◻);x{:}_{◻}\tau .$$ The characteristic introduction premise is $$\frac{\mathrm{\Gamma }/◻{⊢}_{\mathsf{V}}v:\tau }{\mathrm{\Gamma }{⊢}_{\mathsf{V}}\mathsf{box}v:◻\tau }\mathrm{Loc}-\mathrm{Box}.$$ Thus a boxed value cannot retain an ordinary local binding. This is the source card of §3.2, Fig. 2, pp. 12–13 of [Whi26]; it is not System $\mathsf{Xi}$’s second-class block restriction and supplies no theorem about its runtime labels.

Effect reflection: source card.

For an algebraic signature $\mathrm{\Sigma }$, the source has a free-algebra type $W_{\mathrm{\Sigma }}(\tau )$ and a handler-mapping type $y(\mathrm{\Sigma })$. Reflection and reification have the characteristic rules $$\begin{array}{c}\frac{\begin{array}{c}\mathrm{\Gamma }{⊢}_{\mathsf{V}}{v}_1:y(\mathrm{\Sigma })\\ \mathsf{op}:{\tau }_1⇝{\tau }_2\in \mathrm{\Sigma }\\ \mathrm{\Gamma }{⊢}_{\mathsf{V}}{v}_2:◻{\tau }_1\\ \mathrm{\Gamma };x:◻{\tau }_2{⊢}_{\mathsf{C}}c:{\tau }_3\end{array}}{\mathrm{\Gamma }{⊢}_{\mathsf{C}}\mathsf{reflect}(v_1(\mathsf{op}))(v_2,x.c):{\tau }_3}\mathrm{Refl}-\mathrm{Up}\\ \frac{\mathrm{\Gamma };x:y(\mathrm{\Sigma }){⊢}_{\mathsf{C}}c:◻\tau }{\mathrm{\Gamma }{⊢}_{\mathsf{C}}{\mathsf{reify}}_{\mathrm{\Sigma }}(x.c):W_{\mathrm{\Sigma }}(◻\tau )}\mathrm{Refl}-\mathrm{Down}.\end{array}$$ These are §3.4, Fig. 4, pp. 14–15 of [Whi26]. The semantic comparison in §4.8, p. 23 derives the reification isomorphism from Lemma 4.8 and Yoneda. Because this recent source is retained only as a source-gated comparison, the present block imports neither subject reduction nor normalization. In particular, reflection is not the authority-token discipline of System $\mathsf{Xi}$ and is not the tunnelling request constructor.

Mechanism invariants and distinguishing tests

The distinctions can now be stated without relying on shared vocabulary. In this comparison only, an ownership capability is a permission whose typing tracks transfer or disposal of one resource; a capture set is the finite set of names a closure may mention; locality/effect reflection is a boundary discipline recording which effects are available inside, reflected outward, or confined; and control-flow linearity bounds the number of uses of a continuation or resumption. These are comparison predicates, not additional term formers or judgments of the three calculi developed above. A “region capability” in the exercise below means one member of a closure’s capture set that names a lexical region; no separate region calculus is assumed.

The first two columns state the static invariant; the third supplies a program shape that separates it from a neighboring invariant.

Sources.

System $\mathsf{Xi}$, Effekt, their translation, and source effect safety follow [BSO20]. The tunnelling calculus, logical relation, and fundamental, safety, and contextual-refinement theorems follow [ZM19a] and its technical report [ZM19b]. The final comparison cites Olaf’s bidirectional calculus [ZSM20].