ch:algebraic-effects: ch:algebraic-effects

Let the initial counter be $n$. Call by value evaluates the argument before beta reduction: $$(\lambda x.())\mathsf{tick}()⟶(\lambda x.())()⟶(),n⟼n+1.$$ Call by name substitutes the unevaluated argument: $$(\lambda x.())\mathsf{tick}()⟶(),n⟼n.$$ The traces first differ at argument evaluation: the value strategy performs the tick before beta reduction, while the name strategy takes beta first and the absent occurrence of $x$ discards the argument.

A raise request never receives a response, so its response-indexed family is the unique map ${\mathsf{absurd}}_0:0\to T_{\mathrm{\Sigma }}A$. Giving it response type $1$ would supply a branch $k(()):T_{\mathrm{\Sigma }}A$. That branch falsely depicts an execution in which the outside world acknowledges the exception and the computation after the raise continues.

Let $k:R_{\mathsf{op}}\to T_{\mathrm{\Sigma }}A$, $f:A\to T_{\mathrm{\Sigma }}B$, and $g:B\to T_{\mathrm{\Sigma }}C$. Then The middle equality uses the induction hypothesis at every $r:R_{\mathsf{op}}$. By the branch equality stipulated in definition 22.1, those pointwise equalities are exactly equality of the two continuation branches; no additional function-extensionality axiom is used.

With result $S$, take $$t_1={\mathsf{Op}}_{\mathsf{get}}((),\lambda s.{\mathsf{Op}}_{\mathsf{get}}((),\lambda \mathrm{\_}.\mathsf{Ret}(s)))$$ and $t_2={\mathsf{Op}}_{\mathsf{get}}((),\lambda s.\mathsf{Ret}(s))$. A usual state theory identifies them: the second read, with no intervening write, returns the same store as the first. They are unequal raw trees. After constructor injectivity removes their common outer get node, the branch of $t_1$ begins with another operation node whereas the corresponding branch of $t_2$ is a return node; distinct constructors cannot be equal.

Use carrier $\mathsf{List}(A)$ and $$r(a)=[a],h_{\mathsf{choose}}((),k)=k(\mathsf{false})++k(\mathsf{true}),$$ where $++$ is list concatenation. The fold equation is therefore $$\mathsf{fold}({\mathsf{Op}}_{\mathsf{choose}}((),k))=\mathsf{fold}(k(\mathsf{false}))++\mathsf{fold}(k(\mathsf{true})),$$ so every false subtree is explored before its corresponding true subtree. Well-foundedness makes each result list finite.

If a closed terminal $M$ has type $FA$, inversion of terminal canonical forms gives $M=\mathsf{return}V$. If it has type $A^{\prime }\Rightarrow C$, the same lemma gives $M=\lambda x.N$. Hence one fixed well-typed terminal cannot have both shapes. The decisive facts are inversion of C-Return and C-Lam: the former concludes only an $F$ type and the latter only a computation arrow.

For $c:b$, the translation is The binders have types Two To steps, Force, and Beta expose the body. Its two To steps bind $g=i$ and $a=c$; two more Force/Beta steps reduce the identity call to $\mathsf{return}c$.

Rename binders fresh. For abstraction, For application, congruence and the two induction hypotheses give Weak reduction does not enter the lambda in the first calculation. It therefore cannot contract a force–thunk redex created in its body; ${\equiv }_a$, whose compatible closure includes lambda bodies, is necessary.

The outer application translates to $$(\lambda x.h^n(\mathsf{thunk}(\mathsf{force}x))(\mathsf{thunk}(\mathsf{force}x)))(\mathsf{thunk}{u}^n),$$ where each displayed source application uses the call-by-name application clause and the curried type of $h$ determines the parentheses. Beta reduction yields $$h^n(\mathsf{thunk}(\mathsf{force}(\mathsf{thunk}{u}^n)))(\mathsf{thunk}(\mathsf{force}(\mathsf{thunk}{u}^n))).$$ Thus the substituted thunk for $u$ occurs twice, once below each thunk passed to $h$; the two occurrences of $x^n=\mathsf{force}x$ are the two forces. Each is run only if the corresponding argument of $h$ is demanded.

In context $x:1$, the operation rule gives $$\mathsf{raise}{e}_0(z.\mathsf{return}z):F0!\{\mathsf{raise}\}.$$ Hence C-Lam${}^{\mathrm{\Sigma }}$ gives $$\lambda x.\mathsf{raise}{e}_0(z.\mathsf{return}z):1{\Rightarrow }^{\{\mathsf{raise}\}}F0!\varnothing ,$$ and V-Thunk${}^{\mathrm{\Sigma }}$ gives the value type $$U_{\varnothing }(1{\Rightarrow }^{\{\mathsf{raise}\}}F0).$$ The thunk has no immediate computation effect because it is a value; the lambda computation also has empty immediate effect; entering the arrow body has latent effect $\{\mathsf{raise}\}$.

Let $\mathrm{\Sigma }(\mathsf{choose})=1⇝\mathsf{Bool}$ and let the handler preserve result type $A$. Put ${\mathcal{E}}_{\mathrm{in}}=\{\mathsf{choose}\}\cup \mathcal{D}$ and choose $\mathcal{D}\subseteq {\mathcal{E}}_{\mathrm{out}}$. Its return premise is $$\mathrm{\Gamma },x:A{⊢}_c\mathsf{return}x:FA!{\mathcal{E}}_{\mathrm{out}},$$ using C-Weaken. In the choose clause, $$p:1,k:U_{\varnothing }(\mathsf{Bool}{\Rightarrow }^{{\mathcal{E}}_{\mathrm{out}}}FA).$$ Both $(\mathsf{force}k)\mathsf{false}$ and $(\mathsf{force}k)\mathsf{true}$ have $FA!{\mathcal{E}}_{\mathrm{out}}$ by C-Force${}^{\mathrm{\Sigma }}$ and C-App${}^{\mathrm{\Sigma }}$; their sequencing has the same annotation. The two occurrences on the continuation arrow are exactly the output effect that types the two resumptions. Finally ${\mathcal{E}}_{\mathrm{in}}\setminus \{\mathsf{choose}\}\subseteq {\mathcal{E}}_{\mathrm{out}}$ is the forwarding premise.

Under the proposed side condition, every input effect must also be an output effect. Hence an exception handler with ${\mathcal{E}}_{\mathrm{in}}=\{\mathsf{raise}\}$ can receive only an output annotation satisfying $$\{\mathsf{raise}\}\subseteq {\mathcal{E}}_{\mathrm{out}}.$$ The smallest inferred-looking result is therefore $$\mathsf{handle}M\mathsf{with}{H}_E:FA!\{\mathsf{raise}\},$$ even though $H_E$ has a well-typed raise clause and no raise can escape. The rule remains safe because it forgets no possible operation; progress may still expose only names retained in the output. It fails as an elimination rule because handling $\mathsf{raise}$ can never remove that name.

For example, instantiate the callback effect separately at $\varnothing$, $\{\mathsf{raise}\}$, and $\{\mathsf{get},\mathsf{put}\}$: $$\begin{array}{l}{U}_{\varnothing }(A{\Rightarrow }^{\varnothing }FA){\Rightarrow }^{\varnothing }(A{\Rightarrow }^{\varnothing }FA),\\ U_{\varnothing }(A{\Rightarrow }^{\{\mathsf{raise}\}}FA){\Rightarrow }^{\varnothing }(A{\Rightarrow }^{\{\mathsf{raise}\}}FA),\\ U_{\varnothing }(A{\Rightarrow }^{\{\mathsf{get},\mathsf{put}\}}FA){\Rightarrow }^{\varnothing }(A{\Rightarrow }^{\{\mathsf{get},\mathsf{put}\}}FA).\end{array}$$ The same callback effect appears on the input arrow and the returned arrow; the surrounding thunk and outer arrow remain pure. A quantified effect variable must abstract exactly those two repeated finite sets.

If the program reads $s$, writes $s+1$, and returns $a$, no raise occurs. Both orders give $$\mathsf{Catch}(\mathsf{State}(t)(s_0))=\mathsf{Ret}(a,s_0+1)=\mathsf{State}(\mathsf{Catch}(t))(s_0).$$ If the raise is moved before the write, that write lies in the impossible continuation. State first forwards the raise before changing the store and the outside catch returns $(a_0,s_0)$; catch first replaces the raise by $\mathsf{Ret}(a_0)$ before state sees any write. Thus both orders give $\mathsf{Ret}(a_0,s_0)$. Neither modified program distinguishes the two orders. Only the original write-then-raise program distinguishes rollback $\mathsf{Ret}(a_0,s_0)$ from commit $\mathsf{Ret}(a_0,s_0+1)$.

The outer choose is handled and the clause first resumes at $b_1=\mathsf{false}$. With the erroneous shallow continuation, that resumption is $$\mathsf{choose}()(b_2.\mathsf{return}{b}_2)$$ without an enclosing $H_{\mathsf{twice}}$. This inner choose is the first exposed request. The deleted occurrence $\mathsf{handle}X[M[y/x]]\mathsf{with}{H}_{\mathsf{twice}}$ inside $\hat{k}$ is precisely the handler which would capture it. Reinstalling only around the clause, rather than inside each resumption, is too late.

Let $H_E$ have exception and return clauses but no get clause. One forwarding step is The rebuilt continuation is $y.\mathsf{handle}(\mathsf{return}y)\mathsf{with}{H}_E$; it retains the exception handler. Put this term under a state handler $H_S$. The get node is now captured by that nearest $H_S$, which supplies the current store to $y$; the preserved continuation then returns that value through $H_E$.

Suppose $\mathrm{\Gamma }{⊢}_{c}X[\mathsf{choose}()(x.M)]:FA!{\mathcal{E}}_{\mathrm{in}}$ and the handler produces $FB!{\mathcal{E}}_{\mathrm{out}}$. Decomposition gives $$\mathrm{\Gamma },x:\mathsf{Bool}{⊢}_{c}M:FA!{\mathcal{E}}_0.$$ For fresh $y$, response substitution gives $\mathrm{\Gamma },y:\mathsf{Bool}{⊢}_{c}M[y/x]:FA!{\mathcal{E}}_0$. Effect weakening gives the same term annotation $\{\mathsf{choose}\}\cup {\mathcal{E}}_0$, the annotation of the hole. Replacement therefore types $X[M[y/x]]$ at the handler input. Applying C-Handle, then C-Lam${}^{\mathrm{\Sigma }}$ and V-Thunk${}^{\mathrm{\Sigma }}$, gives $$\mathrm{\Gamma }{⊢}_v\hat{k}:U_{\varnothing }(\mathsf{Bool}{\Rightarrow }^{{\mathcal{E}}_{\mathrm{out}}}FB).$$ Parameter substitution replaces $p:1$ by $()$ in the choose-clause premise; continuation substitution then replaces $k$ by $\hat{k}$. The resulting clause body has exactly $FB!{\mathcal{E}}_{\mathrm{out}}$, the type of the reduct.

For $H_{\mathsf{twice}}$ the return component is $r(a)=\mathsf{Ret}(a)$ and its choose component is $$h_{\mathsf{choose}}((),g)=g(\mathsf{false})\gg =(\lambda \mathrm{\_}.g(\mathsf{true})).$$ The input reifies as ${\mathsf{Op}}_{\mathsf{choose}}((),\lambda b.\mathsf{Ret}(b))$. The handled-operation step reifies on both sides as $$\mathsf{Ret}(\mathsf{false})\gg =(\lambda \mathrm{\_}.\mathsf{Ret}(\mathsf{true}))=\mathsf{Ret}(\mathsf{true}).$$ At each resumption, $\mathsf{force}(\mathsf{thunk}(\lambda b.P))V$ and then $(\lambda b.P)V$ both reify as $P[V/b]$ by the two administrative clauses. Thus the operation step and both steps at each resume satisfy the theorem’s one-step equality, and the final operational result reifies as the fold.

For $E=2\times []$ and body $k3$, the original term captures the doubling context: $$\mathsf{reset}(2\times \mathsf{shift}k.k3)⟶\mathsf{reset}((\lambda x.\mathsf{reset}(2x))3){⟶}^{\ast }6.$$ After pushing the context into the body, the captured context is empty: $$\mathsf{reset}(\mathsf{shift}k.2\times (k3))⟶\mathsf{reset}(2\times ((\lambda x.\mathsf{reset}(x))3)){⟶}^{\ast }6.$$ So this one-invocation instance happens to be equal. With body $k(k3)$, the original term invokes the captured doubling context twice and gives $$\mathsf{reset}((\lambda x.\mathsf{reset}(2x))((\lambda x.\mathsf{reset}(2x))3)){⟶}^{\ast }12.$$ The pushed term captures only the empty context and gives $$\mathsf{reset}(2\times ((\lambda x.\mathsf{reset}(x))((\lambda x.\mathsf{reset}(x))3))){⟶}^{\ast }6.$$ Thus the would-be commutation law fails when the captured context is invoked twice.

For the one-handler term, C-Op gives its body input ${\mathcal{E}}_{\mathrm{in}}=\{\mathsf{op}\}$, and the pure clauses let C-Handle choose ${\mathcal{E}}_{\mathrm{out}}=\varnothing$. In the two-handler term, the inner instance has the same two annotations. Its handled result is therefore typed with input $\varnothing$ at the outer instance, whose output is again $\varnothing$.

If scoped availability itself is represented by a finite set, one layer is $\{\mathsf{op}\}$ and two layers are $\{\mathsf{op}\}\cup \{\mathsf{op}\}$. Finite-set idempotence gives $$\{\mathsf{op}\}\cup \{\mathsf{op}\}=\{\mathsf{op}\}.$$ Consequently the annotation cannot answer whether eliminating the nearest handler occurrence should leave another scoped occurrence of $\mathsf{op}$ behind. Set subtraction removes the only recorded name in both cases, so it cannot express one-occurrence removal.