ch:effect-capabilities: ch:effect-capabilities

Each request body has effect $\{\mathsf{ask}\}$. Before the surrounding outer handler is applied, the first displayed phrase still has residual effect $\{\mathsf{ask}\}$, while the inner handler in each of the latter two phrases discharges that request and leaves empty residual effect. After the active $H_{\mathsf{out}}$ is wrapped around each whole phrase, all three complete programs have empty residual effect.

For the first phrase, nearest-name lookup finds the surrounding $H_{\mathsf{out}}$. For the second, the dynamically nearer $H_{\mathsf{in}}$ handles the request before the outer handler is reached. For the third, $\mathsf{underInner}$ invokes the closure under $H_{\mathsf{in}}$, so nearest-name lookup again selects $H_{\mathsf{in}}$.

After replacing each request by $\mathsf{ask}@H_{\mathsf{out}}()$, all three requests carry the same explicit authority and therefore select $H_{\mathsf{out}}$; the inner same-operation handler is skipped in the latter two programs. Thus identical request effects and identical empty residual effects coexist with different handler identities under nearest-name lookup. Effect presence does not encode the authority used to resolve the request.

The exercise assumption gives $\mathrm{\Omega }(F)=1\to \mathsf{Int}$, fixing the operation types required by X-Handle. Let the answer type of the whole handler be $\mathsf{Int}$. In the handled body, $F:1\to \mathsf{Int}$, hence $$\varnothing \mid F:1\to \mathsf{Int}\mid \varnothing ⊢F(()):\mathsf{Int}.$$ Rule X-Var gives $x:\mathsf{Int}⊢x:\mathsf{Int}$; X-Expr lifts that expression to a statement judgment, and X-Val therefore gives $$\varnothing \mid F:1\to \mathsf{Int}\mid \varnothing ⊢\mathsf{val}x=F(());x:\mathsf{Int}.$$ In the clause, the operation argument has type $1$, and the continuation block has type $$k:\mathsf{Int}\to \mathsf{Int}.$$ The numeral $7$ has type $\mathsf{Int}$, so X-Call gives $$u:1\mid k:\mathsf{Int}\to \mathsf{Int}\mid \varnothing ⊢k(7):\mathsf{Int}.$$ Rule X-Handle now concludes the displayed handler has type $\mathsf{Int}$. The four answer-type occurrences are: the handled body, the handler clause, the continuation codomain, and the entire handler; all are $\mathsf{Int}$.

The restriction occurs at three mutually reinforcing points.

1. Value types $\tau$ do not contain block types $\sigma$.

2. The value context $\mathrm{\Gamma }$ stores only bindings $x:\tau$; block bindings occur only in $\mathrm{\Delta }$.

3. The expression grammar contains values and value variables, but not block variables or block abstractions.

Consequently $$\mathsf{val}x=F;x$$ has no derivation: X-Val requires a statement premise, while X-BVar concludes only a block judgment. The block abstraction $\{()\Rightarrow F\}$ fails for the same reason in the body premise of X-Block. Finally, in $G(F,F)$, the first occurrence of $F$ is in a value-argument position and would require an expression judgment; only the second occurrence is a legal block argument. By contrast, $$G((),F)$$ is derivable by X-Call: $():1$ is the value argument and $F:1\to \mathsf{Int}$ is the block argument. The call is well typed while the matching delimiter is active, but no rule turns its block argument into a returnable value.

Write ${\mathrm{\Xi }}_0$ for the label context outside the matching delimiter. Inversion of the redex typing gives For the displayed context and fresh $y:{\tau }_0$, typed context replacement gives $$\mathrm{\Gamma },y:{\tau }_0\mid \mathrm{\Delta }\mid {\mathrm{\Xi }}_0⊢{\mathrm{\#}}_{\ell }\{\mathsf{val}z=y;z\}:\tau .$$ Rule X-Block therefore gives the reified continuation type $$\mathrm{\Gamma }\mid \mathrm{\Delta }\mid {\mathrm{\Xi }}_0⊢\{(y:{\tau }_0)\Rightarrow {\mathrm{\#}}_{\ell }\{\mathsf{val}z=y;z\}\}:{\tau }_0\to \tau .$$ Value substitution replaces $x$ by $v$, and block substitution replaces $k$ by this continuation, so the handler body remains typed at $\tau$ in the outer context ${\mathrm{\Xi }}_0$. If $H_{\ell }$ contained an inner delimiter ${\mathrm{\#}}_{\ell }$, it would not belong to the no-$\ell$-binding grammar $H_{\ell }$; the context-replacement premise used to reconstruct the unique matching delimiter would therefore be unavailable. By contrast, a crossed ${\mathrm{\#}}_{{\ell }^{\prime }}$ with ${\ell }^{\prime }\ne \ell$ belongs to the later suffix ${\mathrm{\Xi }}_{+}$. It is retained inside the reified continuation and is absent from the handler body’s birth-prefix derivation under ${\mathrm{\Xi }}_0$.

Under nearest-name lookup the call stack is $$H_{\mathsf{in}}::H_{\mathsf{out}}::\cdots .$$ Invoking $q$ produces a request named $\mathsf{ask}$. The first matching stack entry is $H_{\mathsf{in}}$, so the execution returns $9$, even though the closure was created under $H_{\mathsf{out}}$.

In capability-passing style write $$q(F):=F(()),\mathsf{underInner}(q,F_{\mathsf{out}}):={\mathsf{handle}}_{H_{\mathsf{in}}}(q(F_{\mathsf{out}})).$$ The block argument $F_{\mathsf{out}}$ names the outer capability. The inner handler does not replace the argument, so the request reaches $H_{\mathsf{out}}$ and returns $7$.

Assume $\mathrm{\Sigma }(\mathsf{Ask})=1\to \mathsf{Int}$ and $\mathrm{\Sigma }(\mathsf{Log})=\mathsf{Int}\to 1$. The block parameter translates as $$\mathsf{CapTy}(1\to \mathsf{Int}/\{\mathsf{Ask}\})=(1,1\to \mathsf{Int})\to \mathsf{Int}.$$ Since $q$’s declared effect is $\{\mathsf{Log}\}$, its translated type is $$((1,1\to \mathsf{Int})\to \mathsf{Int},\mathsf{Int}\to 1)\to \mathsf{Int}.$$ Under the fixed canonical ordering, the second parameter position of the inner type corresponds to $\mathsf{Ask}$, and the final parameter position of the outer type corresponds to $\mathsf{Log}$. The direct $\mathsf{Ask}$ requirement in the body is not in the declared set of $q$; rule E-Def therefore makes it a definition-site capability. Writing that closed-over capability as ${\mathsf{Ask}}_{\mathsf{def}}$, the target has the shape A call is $q(g,{\mathsf{Log}}_{\mathsf{call}})$. Thus the capability passed to $g$ is ${\mathsf{Ask}}_{\mathsf{def}}$, while the capability required by $q$’s own declared effect is ${\mathsf{Log}}_{\mathsf{call}}$.

Rule T-HVar gives $$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢h:\mathsf{F}\mid h.\mathsf{lbl}.$$ Then T-Up gives the pure operation value $$\Uparrow h:[1\to [\mathsf{Int}{]}_{h.\mathsf{lbl}}{]}_{\varnothing }.$$ Rule T-Sub widens its immediate effect from $\varnothing$ to $h.\mathsf{lbl}$, using reflexive type subtyping. A second use of T-Sub widens $x:[1{]}_{\varnothing }$ to $x:[1{]}_{h.\mathsf{lbl}}$. The two premises and the latent result effect now have the one common effect required by T-App, which yields $$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma },x:1\mid \mathrm{\Xi }⊢\Uparrow hx:[\mathsf{Int}{]}_{h.\mathsf{lbl}}.$$ Rule WF-Unit supplies $\mathrm{\Delta }\mid P\mid \mathrm{\Xi }⊢1\mathsf{type}$. Finally T-Lam gives $$\mathrm{\Delta }\mid P\mid \mathrm{\Gamma }\mid \mathrm{\Xi }⊢\lambda x:1.\Uparrow hx:[1\to [\mathsf{Int}{]}_{h.\mathsf{lbl}}{]}_{\varnothing }.$$ If $h$ is instantiated by $H^{\ell }$, the latent effect becomes $\ell$. A delimiter cannot discharge it while returning that function, because T-Down requires $\ell \notin \mathrm{fl}(T,\overline{e})$; here $\ell$ occurs inside the returned function type.

After the two handler-beta steps, the inner delimiter contains $$K_i=\mathsf{let}z:\mathsf{Int}=[]\mathsf{in}\Uparrow H_o^{{\ell }_o}(),K_i[\Uparrow H_i^{{\ell }_i}()].$$ The context $K_i$ does not bind ${\ell }_i$. Rule Tun-Down-up therefore substitutes $$x\mapsto (),k\mapsto \lambda y:\mathsf{Int}.{\Downarrow }^{{\ell }_i}(\mathsf{let}z:\mathsf{Int}=y\mathsf{in}\Uparrow H_o^{{\ell }_o}())$$ into the body of $H_i$. Since that body is $k(9)$, the inner step gives $$(\lambda y:\mathsf{Int}.{\Downarrow }^{{\ell }_i}(\mathsf{let}z:\mathsf{Int}=y\mathsf{in}\Uparrow H_o^{{\ell }_o}()))9,$$ which reduces to $${\Downarrow }^{{\ell }_i}(\Uparrow H_o^{{\ell }_o}()).$$ The outer delimiter now sees $$K_o={\Downarrow }^{{\ell }_i}[],K_o[\Uparrow H_o^{{\ell }_o}()].$$ Because ${\ell }_i\ne {\ell }_o$, $K_o$ does not bind ${\ell }_o$. The second Tun-Down-up step substitutes $$x\mapsto (),k\mapsto \lambda y:\mathsf{Int}.{\Downarrow }^{{\ell }_o}({\Downarrow }^{{\ell }_i}y)$$ into the body of $H_o$. Since that body is $k(7)$, the immediate reduct is $$(\lambda y:\mathsf{Int}.{\Downarrow }^{{\ell }_o}({\Downarrow }^{{\ell }_i}y))7,$$ which reduces to $7$ after both value delimiters disappear. If ${\ell }_i={\ell }_o$, then $K_o$ itself binds the target label, so it is not an admissible no-binding context for the outer rule. The dynamically inner matching delimiter must handle the request instead.

The function clause requires related unit arguments $u_1,u_2$: $$\mathcal{V}[[1]](u_1,u_2),$$ which unfolds to $u_1=()\wedge u_2=()$. It must then establish $$\mathcal{T}[[[1{]}_{h.\mathsf{lbl}}{]]}_{\delta }^{\rho }(v_1{u}_1,v_2{u}_2).$$ When the bodies invoke $\Uparrow h$, the relevant semantic effect clause is ${\mathcal{U}}_A$. The handler environment has the form $$\rho (h)=⟨H_1^{{\ell }_1},H_2^{{\ell }_2},\eta ⟩.$$ It supplies both concrete handlers and the relation $\eta$. The label interpretation $\mathcal{W}[[h.\mathsf{lbl}]]$ is exactly $\eta$, and ${\mathcal{U}}_A$ requires the two requests to use $H_1^{{\ell }_1}$ and $H_2^{{\ell }_2}$, to have related unit arguments, and to produce outcomes related at unit. Thus the handler identity enters through $\rho$, not through operation-name equality.

1. Both $H_{\mathsf{out}}$ and $H_{\mathsf{in}}$ handle $\mathsf{ask}$, so the row $\{\mathsf{ask}\}$ is present in either case, but the handlers return $7$ and $9$. Missing premise: a handler identity or authority relation.

2. A capability block for $\mathsf{ask}$ grants authority to invoke that handler. It says nothing about a separately allocated mutable cell and does not prevent aliases to that cell. Missing premise: an ownership or separation invariant for memory.

3. The two closed handlers that always return $7$ and $9$ are both effect-safe, yet a context observes different integers. Missing premise: a relational abstraction or noninterference condition.

4. Let source terms $t_1,t_2$ be logically related. A faulty compiler may translate $t_1$ correctly and translate $t_2$ to divergence. Source logical relatedness says nothing about that arbitrary mapping. Missing premise: a compiler simulation or semantic-preservation theorem.

The handler step chooses fresh $\ell$ and gives $${\mathrm{\#}}_{\ell }\{\mathsf{val}x={\mathsf{cap}}_{\ell }\{(x,k)\Rightarrow k(x)\}(3);x\}.$$ The capability redex reifies $$k_c=\{(y:\mathsf{Int})\Rightarrow {\mathrm{\#}}_{\ell }\{\mathsf{val}x=y;x\}\}:\mathsf{Int}\to \mathsf{Int}$$ and substitutes $3$ for the clause parameter, yielding $k_c(3)$. Block beta gives ${\mathrm{\#}}_{\ell }\{\mathsf{val}x=3;x\}$; value beta gives ${\mathrm{\#}}_{\ell }\{3\}$; delimiter return gives $3$. Every term is typed at $\mathsf{Int}$ under the label context appropriate to its delimiter.

Replacing the body by the block variable $F$ fails before runtime. The handled-body premise of X-Handle requires a statement judgment; X-BVar derives only a block judgment. Thus no inversion case gives $F$ a value type that could escape the handler.

For E-Def, let the annotated effect set be ${\epsilon }_0=\{F_1,\dots ,F_n\}$ in its canonical order. The induction hypothesis types the translated body under $$\mathsf{CapTy}(\mathrm{\Delta },\overline{g}:\overline{\sigma }),\mathsf{CapEff}({\epsilon }_0^{\prime }).$$ Keep the definition-site capabilities $\mathsf{CapEff}({\epsilon }_0^{\prime }\setminus {\epsilon }_0)$ in the surrounding block context and add every annotated capability in ${\epsilon }_0$ as an ordered formal parameter. Their union contains all capabilities in ${\epsilon }_0^{\prime }$; if an annotation is unused, target weakening supplies its formal binding. Abstracting over the ordinary parameters, translated block parameters, and $F_1,\dots ,F_n$ therefore gives exactly $\mathsf{CapTy}((\overline{\tau },\overline{\sigma })\to {\tau }_0/{\epsilon }_0)$. The continuation induction hypothesis is weakened to the union of its own capabilities and the retained definition-site capabilities, after which X-Def applies.

For E-Try, put $$\mathrm{\Theta }=\mathsf{CapTy}(\mathrm{\Delta }),\mathsf{CapEff}((\epsilon \setminus \{F\})\cup {\epsilon }_h).$$ The translated handled statement weakens to $\mathrm{\Theta },F:{\tau }_1\to {\tau }_0$, where the terminal binding is the capability introduced by the handler and shadows any outer $F$ required by the clause. The translated clause weakens to $\mathrm{\Theta },\mathsf{resume}:{\tau }_0\to \tau$. Rule X-Handle then produces the target statement at $\tau$ under exactly $\mathrm{\Theta }$. Thus source set subtraction corresponds to binding the handled occurrence of $F$, while an occurrence of $F$ in ${\epsilon }_h$ remains available to the clause as an outer capability.

If one occurrence ordered $\{F,G\}$ as $(F,G)$ and another as $(G,F)$, the same source block type would translate to two different positional block types and calls could swap capabilities. A fixed canonical order is therefore part of the syntax translation and of the induction invariant.

In the T-Down case, its first premise gives $\ell \notin \mathrm{dom}(\mathrm{\Xi })$. Choose one label ${\ell }_{\ast }$ fresh for $\mathrm{\Xi }$ and for both closing environments, alpha-rename the bound label before either closing substitution, and use the common extension $${\mathrm{\Xi }}^{+}=\mathrm{\Xi },{\ell }_{\ast }:[T{]}_{\overline{e}}.$$ The induction hypothesis relates the guarded bodies at effects containing that common label. For a pair of related evaluation contexts in $\mathcal{K}$, the semantic stuck relation $\mathcal{S}$ requires ${\ell }_{\ast }⇝̸K_i$. Its concrete-effect decomposition has ${\overline{\ell }}_1={\overline{\ell }}_2=({\ell }_{\ast })$. A matching pair of tunneled requests is classified by ${\mathcal{U}}_B$; Tun-Down-up contracts both sides, and the outcome relation is fed back through the reified continuations $\lambda y.{\Downarrow }^{{\ell }_{\ast }}{K}_i[y]$. The leading later modality lowers the numerical index before the recursive $\mathcal{T}$-use.

Because the type and effect well-formedness premises are checked under $\mathrm{\Xi }$, which lacks ${\ell }_{\ast }$, rule WF-Label derives ${\ell }_{\ast }\notin \mathrm{fl}(T,\overline{e})$. Neither the result type nor the residual effect interpretation can therefore mention the fresh label. Restricting ${\mathrm{\Xi }}^{+}$ back to $\mathrm{\Xi }$ yields the delimiter conclusion. No separate Kripke future-world restriction is involved.

For the first pair, use two closed programs that each handle their only $\mathsf{ask}$ request, one with $H_{\mathsf{out}}$ and one with $H_{\mathsf{in}}$. Both are effect-safe: neither can become stuck on an unhandled request. They return $7$ and $9$, so an integer-observing context distinguishes them. This refutes “effect safety implies contextual equivalence”.

For the second pair, take two beta-equivalent pure terms, for example $(\lambda x.x)()$ and $()$. They are contextually equivalent in the source. Define a deliberately faulty compiler that maps the first to the target value $()$ and the second to divergence. The target programs differ, so source equivalence alone does not imply compiler correctness. The missing premise is a semantic-preservation or simulation theorem for the compiler.

1. Ownership: a file token needs exclusive state-transition authority, not merely an effect name.

2. Tunnelling: the request must cross an unrelated same-operation handler and match its lexical handler identity.

3. Effect rows: the requirement concerns the set of possible exception operations, not one handler instance.

4. Control-flow linearity: the invariant counts resumption uses.

5. Capture sets: the property is which capability value the closure may mention.

6. Explicit capabilities with a label scope: the call must be rejected once the matching delimiter has left the dynamic context.

Effect rows are insufficient for item 2 because they do not distinguish the inner and outer handler instances. A capture set is insufficient for item 4: knowing that a closure mentions a resumption does not limit the number of calls to it.