Effects, Monads, CBPV, and Algebraic Operations

The equation $$(\lambda x.())M=()$$ is harmless when $M$ is a terminating pure term. It is false as an equation of programs as soon as evaluating $M$ can raise an exception or change a cell. Under call by value, $M$ runs before the function is entered; under call by name, the unused argument does not run at all. Evaluation order has become observable.

A computation with effects must record more than its final result. A well-founded operation tree has internal nodes that request operations and leaves that return values. Sequencing such trees will force the neutral-return and associative-sequencing equations rather than assume them.

Computations are not merely results

Fix a set $S$ of stores and a set $\mathsf{Exc}$ of exceptions, and write $1=\{\ast \}$ for a singleton set and $0=\varnothing$ for the empty set. Consider three operation symbols $$\mathsf{get}:1⇝S,\mathsf{put}:S⇝1,\mathsf{raise}:\mathsf{Exc}⇝0.$$ The set to the left of $⇝$ is the parameter sent to the outside world. The set on the right is the response returned to the continuation. Thus a read sends no information and receives a store; a write sends a new store and receives unit; an exception receives no response at all. This signature arrow is static.

Let $e_0:\mathsf{Exc}$ and let $s+1$ denote a fixed update of $s:S$. Define The notation $M\mathsf{to}x.N$ is a bind: it runs the request or computation $M$, names its returned value $x$, and continues as $N$. The last continuation is unreachable because $z:0$. Yet the preceding write is not thereby erased. Whether it remains visible depends on the order in which state and exception requests are interpreted.

The pure result type alone records none of this. Assigning the transaction an arbitrary result type $A$ says what a successful return would contain; it does not say that success is impossible, that a write occurs first, or that an enclosing interpreter may roll the write back. We need a mathematical object that retains both return leaves and operation requests.

The free operation tree

A finite operation signature $\mathrm{\Sigma }$ assigns to every operation symbol $\mathsf{op}$ a parameter set $P_{\mathsf{op}}$ and a response set $R_{\mathsf{op}}$. We write $\mathrm{\Sigma }(\mathsf{op})=P_{\mathsf{op}}⇝R_{\mathsf{op}}$. No equations between operations are assumed yet.

For an operation request, write the smart constructor $$\mathsf{op}(p):={\mathsf{Op}}_{\mathsf{op}}(p,\mathsf{Ret}).$$ Thus $\mathsf{op}(p)\mathsf{to}x.N$ expands to ${\mathsf{Op}}_{\mathsf{op}}(p,\lambda x.N)$: an operation node whose response selects the continuation branch. The transaction in the opening display is the corresponding surface notation for the tree expanded below.

If $\mathrm{\Sigma }\subseteq {\mathrm{\Sigma }}^{\prime }$ preserves the parameter and response sets of every old operation, define $T_{\mathrm{\Sigma }}A\hookrightarrow T_{{\mathrm{\Sigma }}^{\prime }}A$ by $\mathsf{Ret}(a)\mapsto \mathsf{Ret}(a)$ and ${\mathsf{Op}}_{\mathsf{op}}(p,k)\mapsto {\mathsf{Op}}_{\mathsf{op}}(p,\lambda r.\iota (k(r)))$.

The associated induction and recursion principles quantify over every response branch, even when there are infinitely many. To prove $P(t)$ for all $t:T_{\mathrm{\Sigma }}A$, it is enough to prove The recursion principle has the same premises, with recursively computed values supplied for every $k(r)$. These principles define the least set closed under the two constructors: infinite branching changes the number of induction hypotheses at a node, not the well-foundedness of its branches.

The response-indexed family $k$ is the rest of the computation. For example, the transaction is the tree $${\mathsf{Op}}_{\mathsf{get}}((),\lambda s.{\mathsf{Op}}_{\mathsf{put}}(s+1,\lambda \mathrm{\_}.{\mathsf{Op}}_{\mathsf{raise}}(e_0,{\mathsf{absurd}}_0))),$$ where ${\mathsf{absurd}}_0:0\to T_{\mathrm{\Sigma }}A$ is the unique empty function. This expression is well typed for every $A$, but it has no $\mathsf{Ret}$ leaf.

Sequencing must replace each successful return leaf of the first computation by the second computation, while retaining every pending operation.

Proof of Lemma 22.4 — Monad laws forced by sequencing

Proof. The left-unit equation is the first clause for bind. For right unit, induct on $t$. At a return leaf, $$\mathsf{Ret}(a)\gg =\mathsf{return}=\mathsf{Ret}(a).$$ At an operation node, the induction hypothesis gives $k(r)\gg =\mathsf{return}=k(r)$ for every response $r$, hence The final equality is the meta-level eta equation $\lambda r.k(r)=k$; pointwise equality of operation continuations then transports it through $\mathsf{Op}$.

For associativity, again induct on $t$. The return case is $$(\mathsf{Ret}(a)\gg =f)\gg =g=f(a)\gg =g=\mathsf{Ret}(a)\gg =(\lambda x.f(x)\gg =g).$$ For an operation node, calculate every line: The induction-hypothesis label is pointwise in every response $r$. ◻

The preceding calculation proves the monad laws for $T_{\mathrm{\Sigma }}$. For comparison, define $\mathsf{Maybe}(A)=A+1$ with $$\mathsf{return}(a)=\mathsf{some}(a),\mathsf{none}\gg =f=\mathsf{none},\mathsf{some}(a)\gg =f=f(a).$$ Put $h(a)=f(a)\gg =g$; then The last four rows prove associativity because the two sides reduce to the same result in each case. Nothing categorical is required for either calculation.

Proof of Proposition 22.5 — Algebraicity of a requested operation

Proof. This is the operation clause of definition 22.2. Its significance is that the equation is uniform in the result type and in $f$; it is not a special property checked separately for reads, writes, or exceptions. ◻

For a concrete failure, suppose a generator merely identifies two closed leaves $$\mathsf{Ret}(\mathsf{false})\approx \mathsf{Ret}(\mathsf{true}):T_{\mathrm{\Sigma }}\mathsf{Bool}.$$ Constructor congruence alone preserves that equation, but take $f(\mathsf{false})=\mathsf{Ret}(0)$ and $f(\mathsf{true})=\mathsf{Ret}(1)$. The two representatives bind to $$\mathsf{Ret}(\mathsf{false})\gg =f=\mathsf{Ret}(0)\text{and}\mathsf{Ret}(\mathsf{true})\gg =f=\mathsf{Ret}(1),$$ which that generator-only congruence need not identify. Bind is therefore not well-defined until the equation is closed under every Kleisli substitution. Familiar state equations such as reading twice being equivalent to reusing the first answer do not follow. To impose an effect theory $\mathcal{T}$, one must quotient trees by the least congruence containing its declared equations. A fold through that quotient must equalize every generating equation under every tree-valued instantiation of its computation and continuation variables and under every Kleisli substitution. Here a carrier is simply the fold’s target set, and its $\mathrm{\Sigma }$-algebra is the collection of functions chosen to interpret operation nodes; the return map is a separate assignment of the free generators. Definition 22.7 states these data formally. The stronger condition that the whole carrier algebra models $\mathcal{T}$ is sufficient, but is not necessary when the fold does not reach the whole carrier. Three claims are therefore separate: the monad laws follow from sequencing, algebraicity follows from the operation constructor, and state-specific equations require an explicit state theory.

For reference, a standard global-state theory contains the following four schemata, among equivalent presentations, for all appropriately typed continuations: These are equations of trees, not extra reduction rules. In particular, the first equation is the specific “read twice” law used in exercise 22.4.

Handlers are folds

To interpret a tree, choose what to do with returns and with every operation node. The continuation has already been recursively interpreted by the time the operation clause receives it.

Proof of Theorem 22.8 — Existence and uniqueness of handling

Proof. Existence is structural recursion on the well-founded tree. For uniqueness, prove $q(t)={\mathsf{fold}}_{\eta ,h}(t)$ by induction on $t$. At a return leaf, both sides are $\eta (a)$. At an operation node, the defining equation for $q$ and the induction hypothesis at every response $u$ give  ◻

This is the universal property of the free $\mathrm{\Sigma }$-algebra on $A$: $\mathsf{Ret}$ inserts the generators, and a map out of $T_{\mathrm{\Sigma }}A$ is uniquely determined by the generator assignment $\eta$ and the operation interpretations $h$.

An algebra may ignore a continuation, call it once, or call it several times. Exception handling ignores the impossible continuation of $\mathsf{raise}$. A nondeterminism handler can invoke both branches. What algebraicity forbids is inspecting a continuation as syntax or capturing a larger evaluation context that was not supplied as the response function.

By its second defining clause, every fold is a $\mathrm{\Sigma }$-algebra homomorphism extending $\eta$: $${\mathsf{fold}}_{\eta ,h}(\mathsf{Op}(p,k))=h_{\mathsf{op}}(p,\lambda q.{\mathsf{fold}}_{\eta ,h}(k(q))).$$

Proof of Lemma 28.9 — Fold after tree sequencing

Proof. Induct using the tree induction principle following definition 22.1. At a return, both sides are ${\mathsf{fold}}_{\eta ,h}(f(a))$. At an operation node, where the middle equality is the pointwise induction hypothesis. ◻

Proof of Corollary 22.9 — Quotient descent

Proof. First suppose the fold equalizes every tree-valued and Kleisli instance of every generator. Induct on the generated congruence with the strengthened hypothesis that, for every $f$, $${\mathsf{fold}}_{\eta ,h}(t\gg =f)={\mathsf{fold}}_{\eta ,h}(t^{\prime }\gg =f).$$ The return and operation clauses make the fold a homomorphism, so equality is preserved by every return or operation context. A sequencing context at a generator is one of the assumed Kleisli instances; above an operation node, lemma 28.9 pushes that context pointwise into the branches. Induction on the congruence derivation therefore shows that the fold equalizes the least congruence generated by those instances and is constant on quotient classes. Conversely, a fold which descends is constant on quotient classes; the two sides of each tree-valued generator instance represent one quotient class, so their images are equal. This proves the exact criterion.

Finally, if the whole carrier algebra satisfies every generator, interpret a tree-valued assignment by applying the fold to each assigned tree and each response branch. For a Kleisli instance, lemma 28.9 reduces both sides to the carrier equation with the generator assignment $a\mapsto {\mathsf{fold}}_{\eta ,h}(f(a))$. The carrier equation then says exactly that the two instantiated trees have equal fold images. Hence whole-algebra validity is sufficient. No converse is asserted: without a surjectivity or generation hypothesis, descent constrains only the carrier elements reached by the fold. ◻

State and exceptions in both orders

Let ${\mathrm{\Sigma }}_s$ be a signature disjoint from $\mathsf{get}$ and $\mathsf{put}$. A tempting definition gives one map ${\mathsf{State}}_s$ for every initial store $s$. That family does calculate the examples, but it is not one instance of definition 22.7: its $\mathsf{put}$ clause changes the subscript. Put the store in the carrier instead. Define $$\mathsf{State}:T_{\{\mathsf{get},\mathsf{put}\}\cup {\mathrm{\Sigma }}_s}A\to (S\to T_{{\mathrm{\Sigma }}_s}(A\times S))$$ as the fold with carrier $K_s:=S\to T_{{\mathrm{\Sigma }}_s}(A\times S)$ and algebra Here $k:R_{\mathsf{op}}\to K_s$ in every operation clause. In particular, the read clause computes $k(s)(s)$: the current store is both the response and the next state. The write clause computes $k(())(s^{\prime })$, discarding the old state. Expanding the fold gives the useful equations Thus parameter passing, rather than a hidden global store, accounts for the changing state.

Let $a_0:A$. For a signature ${\mathrm{\Sigma }}_e$ disjoint from $\mathsf{raise}$, define $${\mathsf{Catch}}_{a_0}:T_{\{\mathsf{raise}\}\cup {\mathrm{\Sigma }}_e}A\to T_{{\mathrm{\Sigma }}_e}A$$ by preserving returns, replacing every raise node by $\mathsf{Ret}(a_0)$, and forwarding operations in ${\mathrm{\Sigma }}_e$. These are folds; their omitted forwarding equations have exactly the last form above.

For the composed transaction below, fix a residual signature $\mathrm{\Theta }$ disjoint from all three named operations and instantiate the two generic handlers differently: $${\mathrm{\Sigma }}_s=\{\mathsf{raise}\}\cup \mathrm{\Theta },{\mathrm{\Sigma }}_e=\{\mathsf{get},\mathsf{put}\}\cup \mathrm{\Theta }.$$ Thus state handling may forward $\mathsf{raise}$, while exception handling may forward $\mathsf{get}$ and $\mathsf{put}$; the two residual signatures are intentionally not the same.

Now expand the transaction. Handling state first threads the updated store to the raise node and then forwards it: The first equality is the get clause, the second is the put clause evaluated at the new store $s_0+1$, and the last is residual-operation forwarding. The successful result type would have been $A\times S$, but no such leaf was produced. Catching outside it with fallback $(a_0,s_0)$ gives $${\mathsf{Catch}}_{(a_0,s_0)}(\mathsf{State}(\mathsf{transaction})(s_0))=\mathsf{Ret}(a_0,s_0).$$ The threaded update has disappeared: this order implements rollback.

In the other order, ${\mathsf{Catch}}_{a_0}$ forwards the read and write while placing itself around their continuations, then replaces the raise by a successful return: Consequently $$\mathsf{State}({\mathsf{Catch}}_{a_0}(\mathsf{transaction}))(s_0)=\mathsf{Ret}(a_0,s_0+1).$$ The update remains. The two results differ because folds need not commute, not because either fold violates a monad law.

A small call-by-push-value calculus

Operation trees explain sequencing but do not yet isolate why evaluation order changes a program. The effect-free calculus ${\mathsf{CBPV}}_0$ separates values from computations and contains exactly base values, thunks, returned values, sequencing, and functions from values to computations. The call-by-value and call-by-name translations use precisely those constructors. Read $FA$ as “do a computation and return an $A$,” and $UC$ as “be a suspended computation of type $C$.” The core is effect free: an $FA$-computation returns an $A$ and requests nothing. Operations are added after the two translations are proved, so that the value/computation distinction can be seen on its own.

There are two judgments, $\mathrm{\Gamma }{⊢}_{v}V:A$ and $\mathrm{\Gamma }{⊢}_{c}M:C$. Contexts contain value variables only. The complete rules are as follows.

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

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

$c:b\text{ is declared}$

$\mathrm{\Gamma }{⊢}_{v}c:b$

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

$\mathrm{\Gamma }{⊢}_v\mathsf{thunk}M:UC$

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

$\mathrm{\Gamma }{⊢}_c\mathsf{return}V:FA$

$\mathrm{\Gamma }{⊢}_{c}M:FA$$\mathrm{\Gamma },x:A{⊢}_{c}N:C$

$\mathrm{\Gamma }{⊢}_{c}M\mathsf{to}x.N:C$

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

$\mathrm{\Gamma }{⊢}_c\mathsf{force}V:C$

Rules C-Return and C-To are the syntactic counterparts of the unit and bind of definition 22.2: return creates a successful leaf, and sequencing places the second computation after the first. No monad equations for ${\mathsf{CBPV}}_0$ are claimed here; $U$ merely makes a computation into a value that can be delayed and duplicated. The later first-order reification theorem is the explicit connection back to operation-tree bind.

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

$\mathrm{\Gamma }{⊢}_c\lambda x.M:A\Rightarrow C$

$\mathrm{\Gamma }{⊢}_{c}M:A\Rightarrow C$$\mathrm{\Gamma }{⊢}_{v}V:A$

$\mathrm{\Gamma }{⊢}_{c}MV:C$

Weak evaluation does not enter a thunk or a lambda. Its frames and redexes are A terminal computation is $\mathsf{return}V$ or $\lambda x.M$. This definition makes the asymmetry visible: a thunk is a value, whereas forcing it starts a computation.

Proof of Lemma 22.12 — Structural lemmas for CBPV_0

Proof. Weakening is simultaneous induction over the two typing derivations. For substitution, induct simultaneously as well. The variable case either is $x$, when the conclusion is the assumed typing of $W$, or is a different variable, whose context lookup is unchanged. Constants contain no variables. The thunk case invokes the computation induction hypothesis. Return invokes the value hypothesis. Sequencing and lambda use $\alpha$-renaming to keep their bound variable fresh, then apply the appropriate computation hypothesis to each premise. Force applies the value hypothesis to its thunk premise; application applies the computation hypothesis to its operator and the value hypothesis to its argument. Variables, constants, thunks, returns, sequencing, lambdas, force, and application exhaust the two syntactic categories. ◻

Proof of Lemma 22.13 — Canonical terminal computations

Proof. Inspect the two terminal forms. Inversion of C-Return excludes a computation arrow, and inversion of C-Lam excludes $FA$. The remaining inversions give the stated premises. ◻

Proof of Theorem 22.14 — Safety of CBPV_0

Proof. For preservation, induct on the reduction derivation. In the three root cases, inversion of typing followed by lemma 22.12 types respectively $N[V/x]$, $M$, and $M[V/x]$. A frame case uses the induction hypothesis and reconstructs C-To or C-App.

For progress, induct on typing. Values need no evaluation theorem because they occur only in value positions. Return and lambda are terminal. Force has a closed value of type $UC$; inversion of value typing says it is a thunk, so Force applies. In sequencing, the first computation steps or is terminal. If terminal, lemma 22.13 proves that it has the form $\mathsf{return}V$, so To applies. The application case is identical, using the arrow half of the canonical-forms lemma. ◻

Call by value and call by name, factored

The source calculus is the simply typed lambda calculus over the same base types: $$\tau ::=b\mid \tau \to \sigma ,e::=x\mid c\mid \lambda x.e\mid ee.$$ Its typing judgment $\mathrm{\Gamma }⊢e:\tau$ is generated by the complete rules

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

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

$c:b\text{ is declared}$

$\mathrm{\Gamma }⊢c:b$

$\mathrm{\Gamma },x:\tau ⊢e:\sigma$

$\mathrm{\Gamma }⊢\lambda x.e:\tau \to \sigma$

$\mathrm{\Gamma }⊢e_1:\tau \to \sigma$$\mathrm{\Gamma }⊢e_2:\tau$

$\mathrm{\Gamma }⊢e_1{e}_2:\sigma$

For example, if $c:b$ is declared, the application used below is typed by No effect or evaluation-order premise is hidden in these rules. The two evaluations differ only at application. Writing $w$ for a constant or lambda, call by value has

$w{\Downarrow }_{v}w$

$e_1{\Downarrow }_v\lambda x.e$$e_2{\Downarrow }_v{w}_2$$e[w_2/x]{\Downarrow }_{v}w$

$e_1{e}_2{\Downarrow }_{v}w$

whereas call by name has

$w{\Downarrow }_{n}w$

$e_1{\Downarrow }_n\lambda x.e$$e[e_2/x]{\Downarrow }_{n}w$

$e_1{e}_2{\Downarrow }_{n}w$

Thus the call-by-name premise substitutes an unevaluated expression.

The call-by-value translation

Source types translate to CBPV value types: $$b^v=b,(\tau \to \sigma {)}^v=U({\tau }^v\Rightarrow F{\sigma }^v).$$ Values have a value translation $w_v^{†}$, while all terms have a computation translation $e^v$: Application makes the sequencing order explicit: $$(e_1{e}_2{)}^v=e_1^v\mathsf{to}f.e_2^v\mathsf{to}a.(\mathsf{force}f)a.$$ The order of the two sequencings is the order of source evaluation.

The call-by-name translation

Call-by-name source types translate to CBPV computation types: $$b^n=Fb,(\tau \to \sigma {)}^n=U({\tau }^n)\Rightarrow {\sigma }^n.$$ A source variable $x:\tau$ is therefore represented by a thunk $x:U({\tau }^n)$. Terms translate by The argument is suspended before the function is entered. It is run only if an occurrence of $x$ executes $\mathsf{force}x$.

Proof of Lemma 22.15 — Typing of both translations

Proof. Induct on the source typing derivation. Variables and constants use C-Return in the value translation and respectively C-Force and C-Return in the name translation.

For an abstraction $\lambda x.e:\tau \to \sigma$, the induction hypothesis gives $${\mathrm{\Gamma }}^v,x:{\tau }^v{⊢}_c{e}^v:F{\sigma }^v.$$ Rules C-Lam, V-Thunk, and C-Return therefore give the call-by-value type $F(U({\tau }^v\Rightarrow F{\sigma }^v))$. In the name translation the induction hypothesis is under $x:U({\tau }^n)$, so C-Lam gives $U({\tau }^n)\Rightarrow {\sigma }^n$ directly.

For application, the value induction hypotheses are $$e_1^v:F(U({\tau }^v\Rightarrow F{\sigma }^v)),e_2^v:F{\tau }^v.$$ Two uses of C-To, followed by C-Force and C-App, give $F{\sigma }^v$. The name hypotheses give $e_1^n:U({\tau }^n)\Rightarrow {\sigma }^n$ and $\mathsf{thunk}{e}_2^n:U({\tau }^n)$, so one use of C-App finishes. Variables, constants, abstractions, and applications exhaust the source typing rules. The value claim is the variable, constant, and abstraction subcalculation just used. ◻

Call-by-value substitution is literal: $$(e[w/x]{)}^v=e^v[w_v^{†}/x].$$ Call-by-name substitution has one administrative force. Let ${⇝}_a$ be the compatible closure, including positions below thunks and lambdas, of $$\mathsf{force}(\mathsf{thunk}M){⇝}_{a}M.$$ This subscripted relation is distinct from the static signature arrow $⇝$: its operands are terms, and it contracts administrative redexes rather than declaring operation parameters and responses. Write $M^a$ for the result of contracting all such redexes, and write $M{\equiv }_{a}N$ when $M^a=N^a$ up to alpha-equivalence. This is the least congruence containing the symmetric administrative equation. It is used to compare translations; ${⇝}_a$ is not an additional weak evaluation rule.

Proof of Lemma 22.16 — Translation and substitution

Proof. Both claims are inductions on $e$, after renaming binders away from $x$ and the free variables of the substituend. Only the matching-variable case is different. In the value translation both sides are $\mathsf{return}{w}_v^{†}$. In the name translation the right side is $\mathsf{force}(\mathsf{thunk}{u}^n)$ and the left side is $u^n$; these are the generating administrative equation. For application, the induction hypotheses give $$(e_1[u/x]{)}^n{\equiv }_a{e}_1^n[\mathsf{thunk}{u}^n/x],(e_2[u/x]{)}^n{\equiv }_a{e}_2^n[\mathsf{thunk}{u}^n/x].$$ Congruence places the first equality in function position and the second inside the thunked argument. Abstraction uses the body induction hypothesis beneath a freshly renamed binder. ◻

We write $M\Downarrow W$ when CBPV weak reduction reaches a terminal computation $W$.

The name translation needs an operational fact stronger than congruence of ${\equiv }_a$. An administrative equation may lie under a lambda, where weak evaluation cannot contract it, and become active after application. Lemma 22.17 transports weak evaluation across exactly that administrative equivalence.

Proof of Lemma 28.18 — Administrative normal forms and substitution

Proof. Every administrative contraction deletes one occurrence of $\mathsf{force}$ and one occurrence of $\mathsf{thunk}$, so no infinite contraction sequence exists. Two one-step contractions are either at disjoint positions, where they commute, or one lies inside the argument $P$ of a redex $\mathsf{force}(\mathsf{thunk}P)$. Contracting the outer redex first leaves $P$; contracting the inner one first leaves the corresponding contraction of $P$. The two results join in one step. Thus local confluence and termination give a unique normal form $M^a$.

Prove the displayed substitution equation by induction on $M$. Variable and constant cases are immediate, and constructors pass the induction hypotheses to their subterms. In the only exceptional case, substitution makes a value in force position into $\mathsf{thunk}P$; the final normalization on the right contracts the newly formed force–thunk redex, just as normalization of $M[V/x]$ does on the left. ◻

Proof of Lemma 28.19 — Weak steps across administrative normalization

Proof. A simultaneous induction on the weak-reduction derivation and its active frame proves the two displayed implications.

Weak step to normalized step. For the first implication, an administrative Force root is a stutter: take $Q=M^a=(M_1{)}^a$. The To and Beta roots use the substitution equation just proved. A sequencing or application frame reconstructs the corresponding weak step until the source root is exposed; take its weak reduct as $Q$. Administrative redexes newly exposed below a lambda may remain in $Q$, but normalization gives $Q^a=(M_1{)}^a$; weak reduction is not claimed to enter that lambda.

Normalized step to weak trace. For the reverse implication, fix a normalization sequence $M{{⇝}_a}^{\ast }{M}^a$ and induct on its length, with an inner structural induction on the active weak-evaluation frame of the step from $M^a$. If the first administrative contraction is disjoint from that frame, commute it past the intended weak root and invoke the outer induction hypothesis on the shorter normalization suffix. If it is strictly nested in the frame’s substituend, the substitution equation replaces that nested contraction by the corresponding normalized substitution, after which the same suffix is shorter. If the active frame strictly contains the administrative redex, the inner frame induction removes its outer sequencing or application constructor and reconstructs it after the recursive call. The remaining case has the administrative redex at the active position: replay its Force step before the root exposed by normalization. For example, with $$M=(\mathsf{force}(\mathsf{thunk}(\lambda x.N)))V,$$ the normalized term takes one Beta step, while the original takes $$M⟶(\lambda x.N)V⟶N[V/x].$$ The substitution equation gives $(N[V/x]{)}^a=(N^a[V^a/x]{)}^a$, so the endpoints required by the second implication agree. These Force, To, Beta, sequencing-frame, and application-frame cases exhaust active weak reductions. No weak step occurs below a thunk or lambda, so those two constructors contribute no additional case. ◻

Proof of Lemma 22.17 — Administrative transport for weak CBPV evaluation

Proof. Induction on the length of the weak trace, using lemma 28.19 and $Q^a=(M_1{)}^a$ to start the next normalized phase, shows that $M$ terminates exactly when $M^a$ terminates, with administratively equal terminal results. If $M{\equiv }_{a}N$, lemma 28.18 gives both terms the same administrative normal form; transport the evaluation through that common term to obtain $W^{\prime }$. Finally, administrative contraction below a terminal return or lambda cannot change its outer constructor. ◻

For a source call-by-name value put $$c_n^{†}=\mathsf{return}c,(\lambda x.e{)}_n^{†}=\lambda x.e^n.$$

The reflection direction needs the phases of a target trace, not merely its final term. Weak CBPV reduction is deterministic because at most one root redex lies in the unique active frame. For a terminating $M$, let $\ell (M)$ be the length of this unique weak trace. For the name translation we use the administration-invariant cost $${\ell }_a(M):=\ell (M^a).$$ Both $\ell$ and ${\ell }_a$ are measures on ${\mathsf{CBPV}}_0$ only; the handler proofs below use neither. The transport lemma shows that this cost and the terminal administrative class depend only on the class of $M$.

Proof of Lemma 22.18 — Translated trace decomposition

Proof. For the value translation, the only active path through $(e_1{e}_2{)}^v$ first lies in $e_1^v$. Typing and canonical forms prove that its terminal value has the form $\mathsf{thunk}(\lambda x.P)$. One To step exposes $e_2^v$; its terminal form is a returned value. The second To, then Force and Beta, expose $P[V/x]$. Determinism gives the displayed factorization and strictness of the three subtraces.

For the name translation, administrative normalization can change terms inside the operator or its thunked argument, but cannot remove the outer application. Its unique active path therefore first evaluates an operator administratively equivalent to $e_1^n$. Administrative transport replaces that phase by the displayed evaluation of $e_1^n$. Canonical forms prove that the terminal operator has the form $\lambda x.P$. The following Beta step exposes a term administratively equivalent to $P[\mathsf{thunk}{e}_2^n/x]$; the substitution equation in lemma 22.17 gives $L{\equiv }_{a}P[\mathsf{thunk}{e}_2^n/x]$ and $L\Downarrow W^{\prime }$. Deleting the nonempty operator phase and beta step leaves the two proper subtraces, so and .

Finally, first prove by induction on every source term $e$ that $e\mapsto (e^n{)}^a$ is injective up to alpha-equivalence. Variables, constants, abstractions, and applications are distinguished by their outer constructors; the recursive calls recover their immediate subterms. Now inspect terminal forms. Return, thunk, and lambda constructors are injective. Administrative contraction can occur inside a translated lambda body but cannot change its binder or outer constructor. The all-terms injectivity lemma recovers that body, and induction on the source value recovers the unique source value, up to the alpha-renaming already built into the syntax. ◻

Proof of Theorem 22.19 — Evaluation-order simulations

Proof. Call-by-value preservation. Induct on the displayed call-by-value source evaluation. A value is already translated to its stated terminal form. In the call-by-value application case, the first induction hypothesis reduces $e_1^v$ to a returned thunk. The outer To step exposes the translation of $e_2$; the second hypothesis reduces it to $\mathsf{return}(w_2{)}_v^{†}$. The second To, Force, and Beta steps leave $$e^v[(w_2{)}_v^{†}/x]=(e[w_2/x]{)}^v.$$ The third hypothesis reaches the required returned value.

Call-by-name preservation. For a call-by-name application, the operator hypothesis reaches $\lambda x.P$ with $P{\equiv }_a{e}^n$. One Beta step leaves $P[\mathsf{thunk}{e}_2^n/x]$. Since $P{\equiv }_a{e}^n$, congruence and lemma 22.16 give $$P[\mathsf{thunk}{e}_2^n/x]{\equiv }_a(e[e_2/x]{)}^n.$$ The final source induction hypothesis evaluates the latter term. Administrative transport gives an evaluation of the former one with an equivalent terminal result.

Call-by-value reflection. Induct on the natural number $\ell (e^v)$. A translated source value has only the terminal form stated above. For an application, the first clause of lemma 22.18 gives three strictly shorter subtraces. The first two induction hypotheses give $e_1{\Downarrow }_v\lambda x.e$ and $e_2{\Downarrow }_v{w}_2$; injectivity of value translation identifies the terminal thunk and argument with $(\lambda x.e{)}_v^{†}$ and $(w_2{)}_v^{†}$. The substitution equation turns the third subtrace into an evaluation of $(e[w_2/x]{)}^v$, so the final induction hypothesis and V-App give $e_1{e}_2{\Downarrow }_{v}w$.

Call-by-name reflection. Strengthen the claim as follows: $$M{\equiv }_a{e}^n\text{and}M\Downarrow W⟹\text{there is }w\text{ with }e{\Downarrow }_{n}w\text{ and }W{\equiv }_a{w}_n^{†}.$$ Induct on the administration-invariant natural number ${\ell }_a(M)$. Constants are immediate. A translated lambda is terminal, and terminal-constructor invariance recovers that lambda. For an application, the second clause of lemma 22.18 gives and . The operator induction hypothesis gives a source value; its target terminal is a lambda, so injectivity proves that the source value is $\lambda x.e$ and that $P{\equiv }_a{e}^n$. Hence $$L{\equiv }_{a}P[\mathsf{thunk}{e}_2^n/x]{\equiv }_a(e[e_2/x]{)}^n$$ by translation and substitution. The second induction hypothesis gives $e[e_2/x]{\Downarrow }_{n}w$, and N-App gives $e_1{e}_2{\Downarrow }_{n}w$. This proves the strengthened claim. Applying its terminal injectivity clause to the specified $w$ proves the stated reflection direction. The source grammar has no further cases. ◻

Once operations are added in section 22.6, the opening obstruction can be stated inside the calculus. At the present effect-free stage, the simulation theorems fix the two evaluation orders and support the following informal reading. If $\mathsf{tick}()$ is represented by an operation request, its call-by-value translation occurs before the first sequencing can return the function result. Its call-by-name translation lies inside a thunk replacing $x$; when $x$ is absent from the body, no force is generated and the request is never made.

Operations in CBPV

The operation signature is a finite map $$\mathrm{\Sigma }(\mathsf{op})=P_{\mathsf{op}}⇝R_{\mathsf{op}},$$ but $P_{\mathsf{op}}$ and $R_{\mathsf{op}}$ are CBPV value types. Effects are finite sets $\mathcal{E}$ of operation names. A judgment $$\mathrm{\Gamma }{⊢}_{c}M:C!\mathcal{E}$$ says that every operation exposed by evaluating $M$ belongs to $\mathcal{E}$. It is an upper bound: unused members are permitted. This choice makes weakening explicit and avoids pretending that the set is an inferred principal effect. This is deliberately not the row syntax of chapter 4: sets are idempotent and admit ordinary subset weakening, whereas the unique-label record rows of that chapter use a lacks constraint to prevent duplicates. The duplicate-sensitive effect-row alternative is developed next.

Latent effects must remain in types when a computation is suspended or a function is returned. The annotated types are $$A::=b\mid U_{\mathcal{E}}C,C::=FA\mid A{\Rightarrow }^{\mathcal{E}}C.$$ We recover the effect-free notation by writing $UC$ and $A\Rightarrow C$ when the annotation is empty.

The term grammar gains an operation request $$\mathsf{op}V(x.M)$$ and a handler application $\mathsf{handle}M\mathsf{with}H$. The request sends $V:P_{\mathsf{op}}$ and binds the eventual response $x:R_{\mathsf{op}}$ in $M$. For computations returning $A$, a handler has the form $$H=\{\mathsf{return}x\mapsto N_r;{\mathsf{op}}_i(p_i;k_i)\mapsto N_i{\}}_{i\in I}.$$ Let $\mathsf{handled}(H)=\{{\mathsf{op}}_i\mid i\in I\}$; operation names in a handler are distinct. The binder $k_i$ denotes the resumed, already handled continuation.

The opening equation can now be settled inside the calculus. Add $\mathrm{\Sigma }(\mathsf{tick})=1⇝1$ and abbreviate $$T=\mathsf{tick}()(u.\mathsf{return}u).$$ Extend both source translations by $\mathsf{tick}({)}^v=T$ and $\mathsf{tick}({)}^n=T$. For the source term $(\lambda x:1.())\mathsf{tick}()$, call by value exposes the request: This exposed term has type $F1!\{\mathsf{tick}\}$. Call by name places the request in the unused argument thunk and erases it by beta: $$(\lambda x.\mathsf{return}())(\mathsf{thunk}T)\stackrel{Beta}{⟶}\mathsf{return}(),\cdot {⊢}_c\mathsf{return}():F1!\varnothing .$$ Thus the two translations calculate the two observations with which the chapter began.

The displayed judgment is declarative. A selected checker takes all value types, including latent effects in thunk and function types, as annotations. Value checking preserves those annotations; computation checking synthesizes only the least immediate effect. Write the concrete synthesis as ${\mathsf{out}}_{\mathrm{\Xi }}(M)$, where $\mathrm{\Xi }$ records annotated variable types and hence the latent effects of forced thunks. This operation returns an effect or a type error.

Away from handlers, the checker is simultaneous structural recursion on values and computations. Return synthesizes $\varnothing$. Force and application read their effects from the checked thunk or function type; sequencing takes the union of the two synthesized effects; and an operation takes $\{\mathsf{op}\}$ union the effect synthesized for its continuation body. Two rules cross an annotated computation boundary. To check $\mathsf{thunk}M$ at $U_{\mathcal{D}}C$, synthesize ${\mathcal{D}}_0={\mathsf{out}}_{\mathrm{\Xi }}(M)$ and require ${\mathcal{D}}_0\subseteq \mathcal{D}$. To check $\lambda x.M$ at $A{\Rightarrow }^{\mathcal{D}}C$, impose the corresponding inclusion for the body under $x:A$. These inclusions check fixed latent annotations; they do not enlarge the enclosing computation’s immediate effect.

A handler cannot be checked by repeatedly calling this concrete operation at guesses for its output effect. The guessed set occurs inside each resumption’s value type, so a guess can make value checking fail even when a larger or different set is forced by a type annotation. Instead assign one effect unknown ${\epsilon }_h$ to every handler occurrence $h$ in the checked term. For the operation clauses of $h$, run the same structural recursion symbolically under $$k_i:U_{\varnothing }(R_i{\Rightarrow }^{{\epsilon }_h}FB).$$ A checked term has finitely many such unknowns; call their set $J$. A symbolic immediate effect is a monotone map $$\mathrm{\Psi }:\mathcal{P}(\mathrm{\Sigma }{)}^J⟶\mathcal{P}(\mathrm{\Sigma }).$$ Constants, projections ${\epsilon }_h$, union, and difference by a fixed handled set supply the maps produced by the recursion.

The symbolic pass returns three finite collections. Structural comparison of annotated value and computation types returns either a constructor clash, no condition, an equation ${\epsilon }_h={\epsilon }_{h^{\prime }}$, or a pin ${\epsilon }_h=\mathcal{D}$. In particular, comparing $U_{\varnothing }(R{\Rightarrow }^{{\epsilon }_h}FB)$ with $U_{\varnothing }(R{\Rightarrow }^{\mathcal{D}}FB)$ produces that pin; repeated comparisons in the same equality class must produce the same $\mathcal{D}$. Checking a symbolic body against a thunk or arrow annotation records an inclusion. If the expected latent annotation is an unknown ${\epsilon }_h$, the inclusion is another lower-bound constraint on $E_h$ and is added to ${\mathrm{\Phi }}_h$. If the expected annotation is a fixed set $\mathcal{D}$, record the boundary condition $$\begin{array}{}\text{(}B\text{)}& \mathrm{\Theta }(\overline{E})\subseteq \mathcal{D}\end{array}$$ with monotone $\mathrm{\Theta }$. Finally, for each handler occurrence $h$, let ${\mathrm{\Psi }}_{\mathrm{in},h}$, ${\mathrm{\Psi }}_{r,h}$, and ${\mathrm{\Psi }}_{i,h}$ be the symbolic immediate effects of its handled computation, return clause, and operation clauses. Define $$\begin{array}{}\text{(}H\text{)}& {\mathrm{\Phi }}_h(\overline{E}):=({\mathrm{\Psi }}_{\mathrm{in},h}(\overline{E})\setminus {\mathcal{H}}_h)\cup {\mathrm{\Psi }}_{r,h}(\overline{E})\cup \bigcup _{i\in I_h}{\mathrm{\Psi }}_{i,h}(\overline{E}).\end{array}$$ The constraint for $h$ is ${\mathrm{\Phi }}_h(\overline{E})\subseteq E_h$, where ${\mathrm{\Phi }}_h$ also includes all symbolic boundary lower bounds whose right side is ${\epsilon }_h$. Every ${\mathrm{\Phi }}_h$ is monotone because projections, finite unions, and difference by a fixed set are monotone.

Normalize the effect equations by quotienting $J$ into equality classes. Conflicting pins in one class reject. Hold every pinned class at its named set. On the product of the remaining, unpinned classes, start with the empty assignment and iterate simultaneously $$\begin{array}{}\text{(}I\text{)}& E_Q^{n+1}=E_Q^n\cup \bigcup _{h\in Q}{\mathrm{\Phi }}_h({\overline{E}}^n)(Q\text{ unpinned}).\end{array}$$ For one unpinned outer handler whose handled computation has already been synthesized, the first stage contains ${\mathcal{E}}_{\mathrm{in}}\setminus \mathcal{H}$. Clause bodies and boundary lower bounds may contribute further effects at that same stage. At the product fixed point, verify every pinned handler constraint and every boundary condition. Return the component belonging to the checked computation’s outer handler, or its symbolic immediate effect evaluated at the solved assignment. The symbolic pass reports type-constructor clashes before solving.

Proof of Lemma 28.25 — Soundness and completeness of handler constraints

Proof. Proceed simultaneously by structural induction on values, computations, and handler clauses. A variable reads one annotated type from $\mathrm{\Xi }$. At force and application, invert the required thunk, arrow, argument, and result types. Recursive structural comparison either matches their constructors or reports the same mismatch as declarative inversion. At an effect annotation, comparison with resumption types is literal equality after replacing every ${\epsilon }_h$ by $E_h$; this is exactly the generated equality or pin.

Return, sequencing, operation, force, and application reproduce the immediate effects in their typing rules, so union gives both soundness and minimality. An existing C-Weaken changes none of the generated expressions; it only composes the synthesized inclusion with the rule’s inclusion. At a thunk or lambda boundary, the induction hypothesis synthesizes $\mathrm{\Theta }(\overline{E})$. If the expected annotation is fixed at $\mathcal{D}$, the declarative premise exists exactly when $\mathrm{\Theta }(\overline{E})\subseteq \mathcal{D}$, which is condition $(\mathrm{B})$. If it is ${\epsilon }_h$, the same inversion yields the lower bound $\mathrm{\Theta }(\overline{E})\subseteq E_h$ placed in ${\mathrm{\Phi }}_h$. One C-Weaken constructs the premise when either inclusion is strict.

For a handler $h$, use the induction hypotheses for its handled computation and every clause. Its forwarded-input premise is precisely ${\mathrm{\Psi }}_{\mathrm{in},h}(\overline{E})\setminus {\mathcal{H}}_h\subseteq E_h$ after normalization. Indeed, if the original input annotation is ${\mathcal{E}}_{\mathrm{in}}$, the induction hypothesis gives ${\mathrm{\Psi }}_{\mathrm{in},h}(\overline{E})\subseteq {\mathcal{E}}_{\mathrm{in}}$; monotonicity of difference by ${\mathcal{H}}_h$ transports the original forwarding inclusion. Conversely, the synthesized input derivation supplies the smaller annotation ${\mathrm{\Psi }}_{\mathrm{in},h}(\overline{E})$ directly. The return and operation premises are precisely ${\mathrm{\Psi }}_{r,h}(\overline{E})\subseteq E_h$ and ${\mathrm{\Psi }}_{i,h}(\overline{E})\subseteq E_h$. Their conjunction is ${\mathrm{\Phi }}_h(\overline{E})\subseteq E_h$. The operation-premise environment substitutes the same $E_h$ for every occurrence of ${\epsilon }_h$, so the structural induction accounts for the resumption effect inside arbitrary value types, not merely forces of the resumption. Nested handlers are strict subterms and receive distinct unknowns; equations between their resumption types are retained in the same finite constraint system. These cases exhaust the grammar and prove both directions. ◻

Proof of Lemma 28.26 — Boundary normalization of effect weakening

Proof. Prove simultaneously, by structural induction on values, computations, and handler clauses, that the checker constructs a declarative derivation in the stated boundary form and that its synthesized immediate effect is contained in the conclusion effect of every declarative derivation with the same fixed value-type annotations. For return, force, application, sequencing, and operation, rebuild the rule from the smaller immediate effects. Each conclusion is the displayed union, which is contained in the corresponding union of the original premise effects. A C-Weaken in the original derivation merely composes this containment with its displayed inclusion.

For V-Thunk, the induction hypothesis gives an inner derivation at its synthesized effect ${\mathcal{D}}_0$. Since the original thunk type fixes $\mathcal{D}$, inversion of its premise gives ${\mathcal{D}}_0\subseteq \mathcal{D}$. Insert one C-Weaken immediately above that premise when the inclusion is strict, then apply V-Thunk. The C-Lam case uses the corresponding construction with the fixed arrow effect: raise the body effect at the lambda boundary, while the lambda itself still has immediate effect $\varnothing$. These two boundary steps cannot in general be moved to the root because their annotations occur in the result value type.

For a handler, generate the constraints of lemma 28.25. A given declarative output assignment ${\overline{E}}_{\mathrm{out}}$ satisfies them. A pinned equality class has the same component in every satisfying assignment. On the unpinned classes, simultaneous induction on $(\mathrm{I})$ and monotonicity of every ${\mathrm{\Phi }}_h$ give ${\overline{E}}_{\ast }\subseteq {\overline{E}}_{\mathrm{out}}$ componentwise. Each boundary expression $\mathrm{\Theta }$ is monotone, so $\mathrm{\Theta }({\overline{E}}_{\mathrm{out}})\subseteq \mathcal{D}$ implies $\mathrm{\Theta }({\overline{E}}_{\ast })\subseteq \mathcal{D}$. Thus the least assignment passes every boundary check. Constraint completeness supplies normalized clause derivations whose resumptions carry their handler components $E_{\ast ,h}$. Put one C-Weaken at a clause boundary when its synthesized immediate effect is strictly smaller than $E_{\ast ,h}$, and apply C-Handle. For the handler currently being normalized, put $E_{\ast ,h}\subseteq E_{\mathrm{out},h}$ at the root when its equality class is unpinned; a pinned class has equality there. This establishes the stated normal form and its shared handler-output invariant. ◻

Proof of Proposition 22.22 — Least synthesized effect

Proof. Induct on the checked computation. By lemma 28.26, compare at each annotated boundary with a declarative derivation having the same fixed value types. Boundary weakening checks a latent annotation and does not contribute to the enclosing immediate effect. Every non-handler computation rule takes the union of the operation named at its root and the least immediate effects returned by the induction hypotheses, so any declarative annotation for that term contains the synthesized union.

In a handler case, symbolic generation terminates by structural recursion, because the set of handler occurrences and every generated constraint are finite. Equality-class normalization is finite. Monotonicity of all ${\mathrm{\Phi }}_h$ proves that the unpinned product assignment grows componentwise in $(\mathrm{I})$. If there are $m$ unpinned classes, the finite product lattice permits at most $m|\mathrm{\Sigma }|$ strict single-operation additions. Every declarative assignment satisfies the same pins and is a prefixed point of the unpinned system, so induction on $n$ puts the iterates below it. Hence ${\overline{E}}_{\ast }$ is the least assignment compatible with the pins and handler lower bounds. If a boundary test $\mathrm{\Theta }({\overline{E}}_{\ast })\subseteq \mathcal{D}$ fails, monotonicity shows that it also fails at every larger satisfying assignment; rejection is complete. A pinned class has the same concrete set in every satisfying assignment, so checking its handler constraints after iteration is also complete: if ${\mathrm{\Phi }}_h({\overline{E}}_{\ast })⊈E_h$, monotonicity makes the same inclusion fail at every larger assignment while the pinned right side remains fixed. In every accepted case, lemma 28.25 constructs the three handler premises. ◻

The pin branch is necessary even for a pure clause. Put $$K_E:=U_{\varnothing }(R{\Rightarrow }^{E}F1)$$ and consider an operation clause whose resumption has type $k:K_E$ in an environment containing $$g:U_{\varnothing }(K_{\mathcal{D}}{\Rightarrow }^{\varnothing }F1).$$ Let its body be $(\mathsf{force}g)k$, and let the return clause and the forwarded input be pure. Checking the argument of $\mathsf{force}g$ compares $K_E$ with $K_{\mathcal{D}}$ and generates the pin $E=\mathcal{D}$. The body’s symbolic immediate effect is $\varnothing$, so the remaining check is $\varnothing \subseteq \mathcal{D}$. The checker returns $\mathcal{D}$, exactly the declarative handler output. Iterating the old concrete clause checker from $\varnothing$ would instead encounter a type mismatch whenever $\mathcal{D}\ne \varnothing$; it would reject before discovering the forced output annotation.

The distinction between latent and immediate effects is necessary. Fix the result annotation of $$\mathsf{return}(\mathsf{thunk}(\mathsf{return}()))$$ to be $F(U_{\mathcal{D}}(F1))$. The inner return synthesizes $\varnothing$; checking the thunk requires $\varnothing \subseteq \mathcal{D}$ and, when $\mathcal{D}\ne \varnothing$, one boundary C-Weaken below V-Thunk. The outer return nevertheless synthesizes the least immediate effect $\varnothing$. Moving the inner weakening to the root would change an immediate effect but would not establish the fixed latent annotation $\mathcal{D}$.

Thus the repeated set in C-Handle is a checked invariant, not a circular input to the implementation.

For example, an exception handler from $A$ to $A$ with a pure fallback uses the repeated annotations $$\begin{array}{c}{\mathcal{E}}_{\mathrm{in}}=\{\mathsf{raise}\}\cup \mathcal{D},\mathcal{D}\subseteq {\mathcal{E}}_{\mathrm{out}},\\ k:U_{\varnothing }(0{\Rightarrow }^{{\mathcal{E}}_{\mathrm{out}}}FA),N_{\mathsf{raise}}:FA!{\mathcal{E}}_{\mathrm{out}}.\end{array}$$ The continuation variable is uncallable because its domain is $0$. The ambient set $\mathcal{D}$ nevertheless appears in the input, the output, each clause judgment, and the continuation type. Nothing computes it: the programmer writes the same set four times.

The running transaction is now an actual annotated term. Declare $S,\mathsf{Exc},1,0$ as base types, with $():1$, $e_0:\mathsf{Exc}$, and no closed constant of type $0$. Also admit a fixed pure base-value update: if $V:S$, then $V^{+}:S$. It denotes the same update written $s+1$ in the opening tree. Its complete typing rule is $$\frac{\mathrm{\Gamma }{⊢}_{v}V:S}{\mathrm{\Gamma }{⊢}_v{V}^{+}:S}\mathrm{V}-\mathrm{Next}.$$ Put Its successful result type is $0$. The complete bottom-up derivation is the following chain of rule instances: Here ${\mathcal{E}}_{pr}=\{\mathsf{put},\mathsf{raise}\}$ and ${\mathcal{E}}_{gpr}=\{\mathsf{get},\mathsf{put},\mathsf{raise}\}$. The side premises in the last three rows are exactly the declared parameter types and the continuation judgment displayed in the preceding row. Thus no invocation is assigned an effect smaller than its operation name.

Now let $H_{\mathsf{abort}}$ have return clause $x\mapsto \mathsf{return}()$ and the single operation clause $\mathsf{raise}(p;k)\mapsto \mathsf{return}()$. It discards the successful value and catches an exception, but forwards state operations. With ${\mathcal{E}}_s=\{\mathsf{get},\mathsf{put}\}$, the complete handler instance is $$\frac{\begin{array}{c}\cdot {⊢}_c{M}_{\mathsf{tx}}:F0!{\mathcal{E}}_{gpr}\\ {\displaystyle \frac{\begin{array}{c}{\mathcal{E}}_{gpr}\setminus \{\mathsf{raise}\}\subseteq {\mathcal{E}}_s\\ x:0{⊢}_c\mathsf{return}():F1!{\mathcal{E}}_s\\ p:\mathsf{Exc},k:U_{\varnothing }(0{\Rightarrow }^{{\mathcal{E}}_s}F1){⊢}_c\mathsf{return}():F1!{\mathcal{E}}_s\end{array}}{\cdot {⊢}_h{H}_{\mathsf{abort}}:0[{\mathcal{E}}_{gpr}]⟹1[{\mathcal{E}}_s]}}\mathrm{Handler}\end{array}}{\cdot {⊢}_c\mathsf{handle}{M}_{\mathsf{tx}}\mathsf{with}{H}_{\mathsf{abort}}:F1!{\mathcal{E}}_s}\mathrm{C}-\mathrm{Handle}.$$ The two clause-body premises use C-Return${}^{\mathrm{\Sigma }}$ followed by C-Weaken; the set-difference premise is equality.

Deep handling and forwarding

The old evaluation frames are extended by $\mathsf{handle}K\mathsf{with}H$. For a fixed operation $\mathsf{op}$, a handler-free $\mathsf{op}$-open context is generated by $$X_{\mathsf{op}}::=[]\mid X_{\mathsf{op}}\mathsf{to}x.N.$$ There is no application frame: an exposed request has type $FA$, not a function computation type. Because $X_{\mathsf{op}}$ contains no handler, an intervening handler without an $\mathsf{op}$-clause must take Handle-Forward before an outer handler can match the request. This positive grammar, together with the ordinary evaluation-context grammar, selects the nearest handler without a negative “cannot step” premise. For example, if an inner $H_0$ has no $\mathsf{op}$-clause, then $\mathsf{handle}(\mathsf{op}V(x.N))\mathsf{with}{H}_0$ first forwards the request; only the resulting outer request can be caught by an enclosing handler that has such a clause. Induction on contexts gives unique decomposition into an ordinary redex, a return at its nearest handler, or a request in one such $X_{\mathsf{op}}$. The convention is separate from the trace length $\ell$, which was defined only for ${\mathsf{CBPV}}_0$.

Suppose $$H=\{\mathsf{return}x\mapsto N_r;\dots ;\mathsf{op}(p;k)\mapsto N_{\mathsf{op}};\dots \}.$$ The two handling reductions are Handle-Return, and Handle-Op, where $$\hat{k}=\mathsf{thunk}(\lambda y.\mathsf{handle}{X}_{\mathsf{op}}[M[y/x]]\mathsf{with}H).$$ The same $H$ occurs inside $\hat{k}$. A call $(\mathsf{force}k)W$ therefore resumes under the same handler. This is the defining difference between a deep handler and a shallow one. A shallow variant substitutes instead $${\hat{k}}_{\mathsf{shallow}}=\mathsf{thunk}(\lambda y.X_{\mathsf{op}}[M[y/x]]),$$ so operations exposed after resumption escape this occurrence of $H$.

If $\mathsf{op}\notin \mathsf{handled}(H)$, the handler forwards the request: Forwarding rebuilds the operation with a handled continuation. It neither discards the request nor treats it as a returned value.

For the transaction and abort handler above, the first two requests are therefore visibly forwarded. If an enclosing state interpreter answers $\mathsf{get}$ with $s_0$ and resumes $\mathsf{put}$ with $()$, the selected roots are The write is forwarded before the exception is caught; this handler therefore does not roll state back.

The operation case calculated

Assume $\mathrm{\Sigma }(\mathsf{choose})=1⇝\mathsf{Bool}$ and let $H_{\mathsf{twice}}$ have return clause $x\mapsto \mathsf{return}x$ and choose clause $$\mathsf{choose}(p;k)\mapsto (\mathsf{force}k)\mathsf{false}\mathsf{to}\mathrm{\_}.(\mathsf{force}k)\mathsf{true}.$$ The first result is deliberately discarded; the second is returned. For $$M=\mathsf{choose}()(b.\mathsf{return}b),$$ the handler step substitutes $$\hat{k}=\mathsf{thunk}(\lambda b.\mathsf{handle}(\mathsf{return}b)\mathsf{with}{H}_{\mathsf{twice}}).$$ The two resumptions can be read directly from the annotated calculation Both resumptions contain the handler again. Under a shallow rule, a later choice in the resumed continuation would escape instead of being collected.

This calculus gives resumptions multi-shot semantics: $k$ is an ordinary thunked value, so $H_{\mathsf{twice}}$ may force it twice. A one-shot runtime instead consumes a continuation at its first resumption and reports an error on the second; that policy permits the continuation to be represented by a movable stack segment. A direct tree implementation of $\hat{k}$ instead retains or copies the captured $X_{\mathsf{op}}$, with cost proportional to that context unless it is shared persistently. Thus $H_{\mathsf{twice}}$ intentionally marks the boundary between the free-model semantics proved here and a one-shot runtime; porting it requires explicit continuation cloning or a different handler.

The transaction $M_{\mathsf{tx}}$ belongs to the first-order reification fragment of section 22.9, as does the $H_{\mathsf{twice}}$ clause once its two calls are written with the abbreviation $\mathsf{resume}kV:=(\mathsf{force}k)V$. A state handler that returns the final state, however, needs a product or a state-indexed function carrier, neither of which occurs in the deliberately small annotated grammar. Consequently this section does not pretend to give a direct operational rollback trace in an inexpressive carrier. The two state/exception-order calculations of subsection 22.3.1 are the complete account for this core; adding products yields the standard operational handler without changing the handling roots.

Safety with exposed operations

An operation request awaiting an enclosing interpreter is not a malformed program. Progress must therefore name it. Treating such a request as ordinary stuckness would make every modular effectful computation unsafe; treating it as a value would make the handler rule false.

Proof of Lemma 22.23 — Substitution and replacement

Proof. Weakening and substitution extend the simultaneous induction of lemma 22.12. In C-Op, substitute in the parameter value and in the continuation premise. In handler clauses, rename the parameter and continuation binders first; the continuation is an ordinary value variable of the displayed thunk type, so the value-substitution case applies.

For replacement, induct from the marked subderivation to the root. At every old frame, reconstruct C-To${}^{\mathrm{\Sigma }}$ or C-App${}^{\mathrm{\Sigma }}$; their unions are unchanged because the replacement has the same effect annotation. At a handler frame, reconstruct C-Handle with the same handler judgment. If the path crosses C-Weaken, restore it with the same inclusion; this case may occur at any height between the marked hole and the root. No other evaluation frame exists. ◻

Proof of Lemma 22.24 — Typed operation decomposition

Proof. Induct outward through $X_{\mathsf{op}}$. At the hole, C-Op contributes $\mathsf{op}$ to its effect; C-Weaken can only enlarge the set. The only inductive context clause is sequencing, whose effect union retains it. There is no application or handler case in the grammar of $X_{\mathsf{op}}$. Inversion at C-Op gives $\mathrm{\Gamma }{⊢}_{v}V:P_{\mathsf{op}}$ and $\mathrm{\Gamma },x:R_{\mathsf{op}}{⊢}_{c}M:FA!{\mathcal{E}}_0$ for its continuation result type and effect. ◻

Proof of Theorem 22.25 — Preservation

Proof. The three old root reductions use substitution exactly as in theorem 22.14; frame reductions use replacement.

For a return-handler reduction, inversion gives $\mathrm{\Gamma },x:A{⊢}_c{N}_r:FB!{\mathcal{E}}_{\mathrm{out}}$ and $\mathrm{\Gamma }{⊢}_{v}V:A$. Substitution types $N_r[V/x]$.

For a handled operation, invert the typed decomposition of the exposed request inside $X_{\mathsf{op}}$. For a fresh response variable $y:R_{\mathsf{op}}$, response substitution first gives $M[y/x]:FA!{\mathcal{E}}_0$. Rule C-Weaken enlarges this annotation to $\{\mathsf{op}\}\cup {\mathcal{E}}_0$, exactly the annotation of the operation hole. Replacement now types the continuation $X_{\mathsf{op}}[M[y/x]]$ at the handled input type. Rule C-Handle then gives Rules C-Lam${}^{\mathrm{\Sigma }}$ and V-Thunk${}^{\mathrm{\Sigma }}$ type $\hat{k}$ as $U_{\varnothing }(R_{\mathsf{op}}{\Rightarrow }^{{\mathcal{E}}_{\mathrm{out}}}FB)$. The operation-clause premise and two substitutions now type the reduct.

For forwarding, the same substitution–weakening–replacement calculation types the continuation of the rebuilt operation. The set-difference premise ensures that its operation name is in ${\mathcal{E}}_{\mathrm{out}}$; idempotence of union and, if needed, effect weakening derive the exact displayed output annotation. ◻

Proof of Theorem 22.26 — Progress up to an exposed operation

Proof. Induct on typing, stripping final uses of C-Weaken. Return and lambda are terminal. A well-typed force has a thunk value by canonical forms and takes Force; it cannot expose an operation. A well-typed application either evaluates its function or has a lambda and takes Beta; its active computation has function type, not (F A), so it cannot be the exposed request in item 3. Sequencing evaluates an (F A) premise; only in this case does an exposed request extend its open context by the current sequencing frame.

The two new term forms add no canonical value case: an operation request is nonterminal and produces the exposed-operation outcome, while a handler is nonterminal until its body returns, steps, or exposes a request. Thus the old canonical forms for thunks, lambdas, and returned values are unchanged rather than silently being assumed for new values.

An operation request is the third outcome with the empty context. For a handler, apply the induction hypothesis to its body. A return triggers the return rule. A step lifts through the handler frame. An exposed operation either has a clause, when the handled-operation rule applies, or lacks one, when forwarding applies. A lambda cannot type as the handler’s input $FA$. The operation membership assertion is lemma 22.24. ◻

Proof of Corollary 22.27 — Fully handled safety

Proof. Preservation keeps the empty effect annotation. The third progress outcome would require $\mathsf{op}\in \varnothing$. Hence a finite maximal reduction can stop only at a terminal computation, which preservation keeps at type $C$. ◻

This is a partial-correctness theorem. The calculus in this chapter has no fixpoint, but a handler may resume more than once and can generate larger finite computations; adding general recursion would require a divergence case. No termination claim is smuggled into effect safety.

The syntax implements the tree fold

For this section an $\mathsf{op}$-open first-order context is $$X_{\mathsf{op}}^{\mathsf{fo}}::=[]\mid X_{\mathsf{op}}^{\mathsf{fo}}\mathsf{to}x.L\mid \mathsf{handle}{X}_{\mathsf{op}}^{\mathsf{fo}}\mathsf{with}G,\mathsf{op}\notin \mathsf{handled}(G).$$ In particular, it has no general application frame. The only applications admitted above are administrative resumptions.

Proof of Lemma 22.29 — Reification through an open context

Proof. Write $X$ for the displayed $X_{\mathsf{op}}^{\mathsf{fo}}$ inside this proof and induct on it. The empty context is the operation clause of reification. For $X=X^{\prime }\mathsf{to}z.N$, apply the induction hypothesis and then the operation clause for bind: $$\mathsf{Op}(p,g)\gg =f=\mathsf{Op}(p,\lambda r.g(r)\gg =f).$$ The right side is the required reification of $X^{\prime }[L]\mathsf{to}z.N$. For $X=\mathsf{handle}{X}^{\prime }\mathsf{with}G$, the induction hypothesis rewrites the reification of $X^{\prime }[\mathsf{op}V(x.L)]$ to ${\mathsf{Op}}_{\mathsf{op}}(p,g)$ with the parameter and branch function from the lemma statement. Since $G$ has no clause for $\mathsf{op}$, its algebra sends $(p,g)$ to ${\mathsf{Op}}_{\mathsf{op}}(p,g)$. The fold equation therefore rebuilds the node and places the fold around every response branch, which is the displayed equality. ◻

The operational rule substitutes a thunked continuation for $k$, whereas the algebra reads $k$ from an environment. Lemma 22.30 proves equality of the two reifications.

Proof of Lemma 22.30 — Administrative reification of a deep continuation

Proof. Both equations are inductions on $N$. Return, operation, handler, and sequencing cases follow by applying the induction hypotheses to their immediate subterms; sequencing also uses the defining bind equation. The only new continuation case becomes short if we put $R(y):=\mathsf{handle}X[L[y/x]]\mathsf{with}H$: $$(\mathsf{force}\hat{k})V\text{reifies as}(\lambda y.R(y))V\text{reifies as}R(V).$$ Its reification is $g([[V{]]}_{\rho })$ by base-value substitution, exactly the meaning assigned to $\mathsf{resume}kV$ by $\kappa [k\mapsto g]$. ◻

For a closed term, write $[[P]]$ for its denotation at the unique empty value and continuation environments.

Proof of Theorem 22.31 — Handler/tree agreement

Proof. For a return-handler step, base-value substitution gives $$[[N_r[V/x]]]=r_H([[V]]),$$ which is the return equation of the fold.

For a handled operation, apply lemma 22.29. The left side of the operational rule reifies to $$h_{H,\mathsf{op}}(p,\lambda r.[[\mathsf{handle}X[L]\mathsf{with}H{]]}_{\rho [x\mapsto r],\kappa }).$$ The right side reifies to the same tree by parameter substitution and lemma 22.30. If the operation is unhandled, the algebra equation instead makes both sides $${\mathsf{Op}}_{\mathsf{op}}(p,\lambda r.[[\mathsf{handle}X[L]\mathsf{with}H{]]}_{\rho [x\mapsto r],\kappa }),$$ which proves the forwarding case.

For sequencing, reification turns the left side into $\mathsf{Ret}(a)\gg =f=f(a)$, and base-value substitution identifies this with the right side. The two continuation steps preserve reification by its two administrative clauses. A sequencing frame applies tree bind to equal trees; a handler frame applies the same fold to equal trees. Sequencing, the two continuation contractions, sequencing frames, and handler frames exhaust the reductions allowed by the lemma, and each preserves the reified tree in one step.

Induction on the reduction sequence now gives $$[[\mathsf{handle}M\mathsf{with}H]]=[[Q]].$$ Expanding the structural reification clause for the initial handler gives the claimed fold equation. ◻

The theorem is deliberately silent about general application frames, higher-order CBPV programs, and recursive computations. It also does not say that a syntactically definable handler respects an additional effect theory. That last obligation is the quotient-correctness condition following corollary 22.9.

Where algebraicity stops

An algebraic operation commutes with a surrounding sequencing context. In tree notation this was proposition 22.5; operationally it says that a context which runs after the response can be pushed into every response branch. Capturing the surrounding context is different.

One isolated calculation suffices. Suppose a delimiter and a capture form obey $$\mathsf{reset}(E[\mathsf{shift}k.M])⟶\mathsf{reset}(M[(\lambda x.\mathsf{reset}(E[x]))/k]).$$ For this boundary calculation only, evaluation also has ordinary call-by-value beta reduction, arithmetic on numerals, and $\mathsf{reset}(n)⟶n$ for a numeral $n$. Let $v$ range over numerals and lambda abstractions. Delimiter-free capture contexts and full evaluation contexts are Thus $E$ cannot cross a reset, while $D$ lets ordinary root reductions run beneath a delimiter. Besides the displayed shift and reset roots, use $(\lambda x.M)v⟶M[v/x]$, the usual numeral arithmetic roots, and the frame rule $$\frac{M⟶M^{\prime }}{D[M]⟶D[M^{\prime }]}.$$ These clauses define the entire untyped control fragment considered here. In the absence of a typing judgment or answer-type index, they imply no type preservation or answer-type theorem. Take the arithmetic context $E=1+[]$ and a body which ignores $k$. Then $$\mathsf{reset}(1+\mathsf{shift}k.0){⟶}^{\ast }0,$$ whereas moving the context into the body gives $$\mathsf{reset}(\mathsf{shift}k.(1+0)){⟶}^{\ast }1.$$ The two sides of the would-be commutation law differ. The capture form observes the context which an algebraic operation must treat uniformly.

This is not yet a control calculus. No typing rule, answer type, or general translation for $\mathsf{shift}$ is being imported. Those choices belong to the later control development. The calculation establishes only the needed boundary: a fixed operation signature and its fold do not account for an operator whose behavior depends on capturing the ambient continuation.

Closed sets expose the row problem

The closed annotation system proves the safety theorem it claims, but it does not provide modular inference. Consider a higher-order function $\mathsf{twice}$ which applies an effectful callback twice. Its useful CBPV type has the schematic form $$U_{\varnothing }(A{\Rightarrow }^{\epsilon }FA){\Rightarrow }^{\varnothing }(A{\Rightarrow }^{\epsilon }FA).$$ The callback’s unknown effect $\epsilon$ must reappear as the latent effect of the returned function. In the grammar of definition 22.20, however, an annotation is a concrete finite set. Writing one metavariable on the page does not define its formation, equality, generalization, or unification rules.

Local interpretation needs more. A state handler should express a family like $$\mathrm{\forall }\epsilon .U_{\{\mathsf{get},\mathsf{put}\}\cup \epsilon }(FA){\Rightarrow }^{\epsilon }(S{\Rightarrow }^{\epsilon }FA),$$ where the returned function accepts the initial state, the ambient effects pass through, and one handled layer of state is removed. Closed sets can instantiate this statement separately for each chosen $\epsilon$, but cannot infer or generalize the family. Because sets are idempotent, they also cannot distinguish two scoped occurrences of the same operation name; removing the name removes every occurrence.

Polymorphic handlers require open effect collections, equations that expose one chosen label through an unknown tail, removal of one occurrence, and most-general unification. Unique-label record rows enforce a lacks constraint; effect rows instead permit duplicate labels, so removing one occurrence requires different equality and unification laws.

Suggested first pass.

Begin with exercise 22.14, exercise 22.17, exercise 22.18; then use the remaining problems to test deep resumption, forwarding, control, and duplicate-label boundaries.

Exercise 22.14¶

★★☆ Repeat both transaction calculations with a successful return after $\mathsf{put}$. Then move the raise before the write. Display the two handler orders for each modified program and state which of these four outcomes differ.

Referenced from 4 locations

• Effects, Monads, CBPV, and Algebraic Operations
• ch:algebraic-effects: ch:algebraic-effects

Exercise 22.15¶

★★☆ Delete the handler around $X_{\mathsf{op}}[M[y/x]]$ in $\hat{k}$. Evaluate $$\mathsf{choose}()(b_1.\mathsf{choose}()(b_2.\mathsf{return}{b}_2))$$ under $H_{\mathsf{twice}}$. Identify the first request which becomes exposed and the exact missing handler occurrence that would capture it.

Referenced from 3 locations

• Effects, Monads, CBPV, and Algebraic Operations
• ch:algebraic-effects: ch:algebraic-effects

Exercise 22.16¶

★☆☆ Put a state request inside an exception handler which has no state clauses. Use Handle-Forward once, then place the result inside a state handler with a $\mathsf{get}$ clause. Display the rebuilt continuation and the nearest handler which captures the request.

Referenced from 3 locations

• Effects, Monads, CBPV, and Algebraic Operations
• ch:algebraic-effects: ch:algebraic-effects

Exercise 22.17¶

★★☆ Reconstruct the handled-operation case of preservation for $\mathsf{choose}$, including the type of $\hat{k}$. Mark response substitution, effect weakening, replacement, parameter substitution, and continuation substitution separately.

Referenced from 4 locations

• Effects, Monads, CBPV, and Algebraic Operations
• ch:algebraic-effects: ch:algebraic-effects

Exercise 22.18¶

★★☆ Reify the complete $H_{\mathsf{twice}}$ calculation and identify the return and operation components of its algebra. Verify theorem 22.31 at its single choice node and at both resumption steps.

Referenced from 4 locations

• Effects, Monads, CBPV, and Algebraic Operations
• ch:algebraic-effects: ch:algebraic-effects

Exercise 22.19¶

★★☆ Use exactly the boundary rules displayed in section 22.10 and $E=2\times []$. Compare the original and context-pushed terms first with body $k3$ and then with body $k(k3)$. Calculate all four normal forms. Identify the equality in the one-invocation case and the failure caused by invoking the captured doubling context twice.

Referenced from 3 locations

• Effects, Monads, CBPV, and Algebraic Operations
• ch:algebraic-effects: ch:algebraic-effects

Exercise 22.20¶

★★☆ Let $H$ be a pure handler for $\mathsf{op}$, and compare $$\mathsf{handle}(\mathsf{op}()(x.\mathsf{return}x))\mathsf{with}H$$ with the term obtained by placing a second copy of the same handler around that whole term. For each C-Handle instance, calculate ${\mathcal{E}}_{\mathrm{in}}$ and ${\mathcal{E}}_{\mathrm{out}}$: the inner body has $\{\mathsf{op}\}$, its result has $\varnothing$, and the outer handler therefore receives $\varnothing$. Then represent one and two available scoped layers by the proposed set annotations $\{\mathsf{op}\}$ and $\{\mathsf{op}\}\cup \{\mathsf{op}\}$. Prove that they are equal and state the one-occurrence removal question that this annotation alone cannot answer.

Referenced from 3 locations

• Effects, Monads, CBPV, and Algebraic Operations
• ch:algebraic-effects: ch:algebraic-effects

Exercise 22.21¶

★★★ Practical project.handler-forwarding-machine Implement a finite evaluator for the annotated handler calculus. Maintain the invariant that forwarding retains a continuation recursively wrapped by the same deep handler, while a handled request invokes its clause with that reinstalled continuation. The eight cases must cover state/exception order, state forwarding, nested choice, and handler/fold agreement, ending with All 8 effects corpus cases passed.; the audit must be empty. Test three deliberately incorrect evaluators: make choice shallow, retain the old state after $\mathsf{put}$, and discard a forwarded $\mathsf{get}$. Each variant must remain executable and fail at least one of the eight expected outcomes. These finite tests are implementation evidence, not a proof of handler safety or contextual equivalence.

Referenced from 4 locations

• Effects, Monads, CBPV, and Algebraic Operations
• Object calculus checker and evaluator
• ch:algebraic-effects: ch:algebraic-effects

Sources.

Return and bind use Moggi’s Kleisli triple (Definition 1.2) and monad correspondence (Proposition 1.6) [Mog91]. Levy gives the CBPV decomposition and translations in Sections 3.7.1–3.7.2 [Lev01]. The effect-free Coq development gives the translations in Figures 5 and 8, translation support lemmas in Lemmas 2.2–2.12, and weak simulations in Section 3 [FSSS19]; it does not prove handler safety. Plotkin and Pretnar give syntax in Sections 2.1–2.4, rollback in Section 3.5, and free-model correctness in Section 4, while explicitly omitting formal operational semantics [PP13]. Thus the safety and agreement proofs are local. Bauer and Pretnar describe their prototype in Section 5 and supply executable examples in Section 6, not these metatheorems [BP15].