Higher-Order Algebraic Effects and Modular Elaboration

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

A first-order operation node contains an operation and the continuation which receives its response. This is enough for reading state, raising an exception, or choosing a Boolean. It is not enough for $$\mathsf{catch}(M_1,M_2),$$ because both arguments are computations. An implementation of catch must inspect the completed translation of $M_1$, and it must retain the completed translation of $M_2$ for the failure case. A first-order fold recursively translates only the response continuation. Neither computation argument has a place in which that recursion can occur.

One repair is a global translation that pattern matches on every source constructor, but then adding an operation requires editing the translator. A modular representation instead associates a translation clause with each operation and composes independently defined clauses.

Two recursive operations are distinct. For a higher-order node with fork family $\psi$ and continuation $k$, monadic bind changes only $k(r)$ to $k(r)\gg =f$. Elaboration applies its recursive map to every $\psi (s)$ and every $k(r)$. Hence bind recursion ranges over responses, while elaboration recursion ranges over forks and responses.

The missing recursive positions

Recall the first-order signature used in chapter 22. It is a pair $$\mathrm{\Delta }=({\mathsf{Op}}_{\mathrm{\Delta }},{\mathsf{Ret}}_{\mathrm{\Delta }}),{\mathsf{Ret}}_{\mathrm{\Delta }}:{\mathsf{Op}}_{\mathrm{\Delta }}\to \mathbf{Set}.$$ Its free tree is generated by For a family $G:\mathbf{Set}\to \mathbf{Set}$, a generator $g:A\to G(A)$, and an ordinary algebra $$a_o:({\mathsf{Ret}}_{\mathrm{\Delta }}(o)\to G(A))\to G(A),$$ the fold equations are The recursive calls in the second line are indexed by responses to $o$. There is no other recursive position.

Suppose we try to add a catch operation at result type $A$. The most direct first-order arity would be $${\mathsf{catch}}_A:({\mathsf{Free}}_{\mathrm{\Delta }}(A)\times {\mathsf{Free}}_{\mathrm{\Delta }}(A))⇝A.$$ This is not an ordinary operation signature of the form (24.1). Its parameter type mentions both the ambient target signature $\mathrm{\Delta }$ and the result type $A$. Worse, even if the pair in (24.1) were admitted as an opaque parameter, the fold in (24.1) would receive the two trees without recursively folded results. The catch clause would then have to invoke the global translator itself.

A second attempt stores source syntax rather than target trees: $${\mathsf{catch}}_A:({\mathsf{Syntax}}_H(A)\times {\mathsf{Syntax}}_H(A))⇝A.$$ Now the signature mentions the entire source signature $H$, and every target algebra which handles catch must know how to translate arbitrary ${\mathsf{Syntax}}_H$-trees. The operation-specific clause is no longer modular. Equations (24.1) and (24.1) expose the same defect from opposite sides: the recursively translated computation arguments are absent from the first-order node interface.

Proof of Proposition 24.1 — First-order fold obstruction

Proof. The fold’s operation clause receives only $o$ and the family ${\mathsf{fold}}_{g,a}\circ k$. Every recursive result available to the algebra is therefore the image of some response branch $k(r)$. If $M$ is not one of these branches, its folded value is absent. Putting $M$ into $k$ makes it a computation selected by an operation response and followed by the surrounding continuation; that is not the role of an independently scoped argument. Otherwise the only way for the clause to obtain a folded value of $M$ is to call a translator not supplied by (24.1). Such a translator is indexed by the whole source signature, so the clause ceases to be modular. ◻

Higher-order signatures

The missing information is not an untyped list of child trees. Different computation arguments may return different types, and their number and result types may depend on the operation. We therefore index the recursive positions by an ordinary effect signature.

Write $\mathsf{Effect}$ for the class of small ordinary signatures $\mathrm{\Delta }=({\mathsf{Op}}_{\mathrm{\Delta }},{\mathsf{Ret}}_{\mathrm{\Delta }})$, where ${\mathsf{Op}}_{\mathrm{\Delta }}:\mathbf{Set}$ and ${\mathsf{Ret}}_{\mathrm{\Delta }}:{\mathsf{Op}}_{\mathrm{\Delta }}\to \mathbf{Set}$. Thus ${\mathsf{Fork}}_H(o):\mathsf{Effect}$ below is an ordinary signature, not an effectful computation or an additional universe of terms.

The word fork refers to the family of nested computations; it is not a parallel-evaluation claim. The signature specifies their shape, not an execution order.

Higher-order signatures have a disjoint sum. We write $H_1⊞H_2$ for the signature defined by The symbol $⊞$ is used only for this higher-order signature sum. For ordinary signatures ${\mathrm{\Delta }}_i=({\mathsf{Op}}_{{\mathrm{\Delta }}_i},{\mathsf{Ret}}_{{\mathrm{\Delta }}_i})$, define their disjoint sum ${\mathrm{\Delta }}_1{\oplus }_{\mathsf{sig}}{\mathrm{\Delta }}_2$ by Thus ${\oplus }_{\mathsf{sig}}$ composes first-order target operations, whereas $⊞$ also composes their fork signatures. Unparenthesized chains of either signature-sum symbol associate to the right; this parsing convention does not make the two nestings definitionally equal.

The two function fields in (24.3) play different roles. The family $\psi$ contains computations owned by the operation. The function $k$ contains the computation which follows the operation’s result. This distinction will control bind.

Catch as a typed fork

To make operations polymorphic in their result type, fix a small universe of codes $\mathsf{Ty}$ with interpretation $\mathsf{Val}:\mathsf{Ty}\to \mathbf{Set}$. No closure property of this universe is used below; it may contain only the codes required by the examples.

First take the head-summand row $H=\mathsf{Catch}⊞H^{\prime }$. For $M_1,M_2:{\mathsf{Hefty}}_H(\mathsf{Val}(t))$, define The fork stores the protected and fallback computations. The continuation is $\mathsf{pure}$ because the operation itself returns whichever branch value is selected. A surrounding bind will replace this continuation without altering either branch.

The container shape (24.3) is deliberately specific. It represents a family of strictly positive recursive positions indexed by an ordinary signature. A semantically describable higher-order operator whose syntax places the recursive family negatively is not admitted merely because one can write a set-theoretic endofunctor for it.

Sequencing is not structural recursion

For an ordinary free tree, bind can be defined by the fold because every recursive child is a continuation branch. In a hefty tree, the fork contains computations which lie inside the operation’s scope. Sequencing after the operation must not be pushed into them.

The tempting equation is a full structural recursion: For a general hefty node, the second line is not even well typed. If the whole node has result type $A$, then $g$ has domain $A$, whereas $\psi (s)$ returns ${\mathsf{Ret}}_{{\mathsf{Fork}}_H(o)}(s)$, which need not be $A$. Equation (24.3) is typeable only in a homogeneous special case where every fork result in the node is $A$. The catch smart constructor (24.2.1) is such a case. There the equation typechecks and is still semantically wrong: it pushes $g$ into both branches and also places $g$ in the operation continuation: Any elaborator which runs one branch and then invokes the continuation will therefore run $g$ twice.

For catch, equation (24.6) gives $$\mathsf{catch}(M_1,M_2)\gg {=}_{\mathsf{H}}g=\mathsf{impure}(\mathsf{catch}(t),\lambda b.\mathsf{if}b\mathsf{then}{M}_1\mathsf{else}{M}_2,g).$$ The branch selected as successful produces a value for $g$ exactly once.

Proof of Theorem 24.8 — Monad equations for hefty bind

Proof. The first equation is definitional. For the right unit, induct on $M$. The pure case is immediate. In the operation case, The fork is unchanged, so no induction hypothesis is required there.

For associativity, the pure case is definitional. In the operation case, expand the left side twice: Pointwise equality of the continuation fields gives constructor equality. ◻

The structural catamorphism

Elaboration has the opposite recursive requirement. It must translate every nested computation before the operation-specific clause is invoked. The algebra therefore receives already-translated forks and continuations.

Equation (24.10) traverses both recursive fields. A bind with $g:A\to {\mathsf{Hefty}}_H(B)$ cannot supply the polymorphic generator required at arbitrary fork-result types. Even in the homogeneous catch fragment, where those types coincide with $A$, structural recursion would transform the forks and recreate the semantic defect of (24.3).

Proof of Lemma 24.11 — Unique structural solution

Proof. Apply the displayed induction principle of definition 24.3 to the simultaneously quantified predicate $${\mathcal{P}}_X(M)⟺f_X(M)={\mathsf{cata}}_{g,\alpha ,X}^{\mathsf{H}}(M).$$ The pure case is the common generator equation. In the operation case, the hypotheses give $f_{Y_s}(\psi (s))={\mathsf{cata}}_{Y_s}(\psi (s))$ for each fork and $f_X(k(x))={\mathsf{cata}}_X(k(x))$ for each response. Function extensionality equates both function fields, and the common algebra equation equates the results. ◻

Elaboration into first-order trees

The target of elaboration is an ordinary free tree. The source operation clause may arrange, handle, duplicate, or discard the translated computation arguments, but it cannot receive an ill-typed one.

Unfolding the definition gives These are the generic elaboration equations. An operation-specific clause is written against translated subcomputations, not raw source syntax.

Proof of Theorem 24.13 — Typing by construction

Proof. Induct on $M$. A pure node is translated by the target constructor $\mathsf{pure}:A\to {\mathsf{Free}}_{\mathrm{\Delta }}(A)$. For an operation node, the induction hypotheses give (24.13) pointwise for the fork and continuation. The component $E_A(o,-,-)$ has exactly these two families as its premises and returns ${\mathsf{Free}}_{\mathrm{\Delta }}(A)$. This establishes (24.13). ◻

The theorem says neither that an untyped source parser produces a hefty tree nor that elaboration simulates a source operational semantics. It says that once source syntax is represented by the indexed family ${\mathsf{Hefty}}_H$, every well-typed algebra clause produces a target tree with the same result index.

Lifting ordinary operations

Let $\mathsf{Nil}$ be the empty ordinary signature. An ordinary signature ${\mathrm{\Delta }}_0$ embeds into a higher-order signature $\mathsf{Lift}({\mathrm{\Delta }}_0)$ by A lifted operation has no nested computation arguments.

The witness of definition 24.14 extends a head injection. That injection appears in (24.2.1). The witness selects one occurrence of $\mathsf{Catch}$ and supplies the required fork and response transports.

For example, the throw summand in the transaction row has the concrete witness $$\frac{{\displaystyle \frac{\phantom{X}}{\mathsf{Ins}(\mathsf{Throw}{\oplus }_{\mathsf{sig}}\mathsf{Nil};\mathsf{Throw},\mathsf{Nil})}}}{\mathsf{Ins}(\mathsf{State}{\oplus }_{\mathsf{sig}}(\mathsf{Throw}{\oplus }_{\mathsf{sig}}\mathsf{Nil});\mathsf{Throw},\mathsf{State}{\oplus }_{\mathsf{sig}}\mathsf{Nil})}.$$ The outer rule skips $\mathsf{State}$; the inner base rule selects $\mathsf{Throw}$. The catch summand of the higher-order transaction row requires two skips. Put $$H_2:=\mathsf{Catch}⊞\mathsf{Lift}(\mathsf{Nil}),H_1:=\mathsf{Lift}(\mathsf{Throw})⊞H_2.$$ Its exact witness is $$\frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{\mathsf{HIns}(H_2;\mathsf{Catch},\mathsf{Lift}(\mathsf{Nil}))}}}{\mathsf{HIns}(H_1;\mathsf{Catch},\mathsf{Lift}(\mathsf{Throw})⊞\mathsf{Lift}(\mathsf{Nil}))}}}{\mathsf{HIns}(\mathsf{Lift}(\mathsf{State})⊞H_1;\mathsf{Catch},\mathsf{Lift}(\mathsf{State})⊞\mathsf{Lift}(\mathsf{Throw})⊞\mathsf{Lift}(\mathsf{Nil}))}.$$ The two outer rules skip the lifted state and throw summands; the base rule selects $\mathsf{Catch}$. This is the witness suppressed later in (24.8).

Insertion witnesses are proof relevant. Consequently the implementation infers a witness from its indices only for a duplicate-free ordered row of atomic summands. On such rows, induction on the row proves that $\mathsf{Ins}$ and $\mathsf{HIns}$ have at most one derivation at fixed indices. If a row repeats a summand, the witness must remain explicit: different witnesses can select different occurrences, and this chapter claims no coherence theorem identifying their elaborations.

Proof of Proposition 24.15 — Canonical insertion on duplicate-free rows

Proof. Induct on the ordered row. The empty row has no derivation. If its head is the requested atomic summand, the base rule yields the tail as residual. A step derivation would require a second occurrence in the tail, which duplicate freeness excludes. If the head differs, the base rule is impossible and every derivation uses the step rule; the induction hypothesis uniquely determines both the tail residual and the tail derivation, hence also the residual with the skipped head restored. For $\mathsf{HIns}$, induct on the ordered row $H$. The empty row has no derivation. If the head is $H_0$, the base constructor determines the residual $H^{\prime }$ as the tail; an HIns-Step derivation would require another $H_0$ in that tail and contradict duplicate freeness. If the head differs from $H_0$, HIns-Base cannot apply, so both candidate derivations end in HIns-Step. Their premises have the form $\mathsf{HIns}(H_{\mathrm{tail}};H_0,H_{\mathrm{tail}}^{\prime })$; the induction hypothesis identifies both the tail residual and its derivation, after which the common skipped head identifies $H^{\prime }$ and the two outer derivations. ◻

For $w:\mathsf{Ins}(\mathrm{\Delta };{\mathrm{\Delta }}_0,{\mathrm{\Delta }}^{\prime })$, the ordinary-operation elaborator is $$E_{\mathsf{lift},w}(o,\psi ,k)=\mathsf{impure}({\iota }_w^{\ell }(o),k\circ q_{w,o}^{\ell }),$$ where $q_{w,o}^{\ell }:{\mathsf{Ret}}_{\mathrm{\Delta }}({\iota }_w^{\ell }(o))\to {\mathsf{Ret}}_{{\mathrm{\Delta }}_0}(o)$ is the response transport. The fork $\psi$ has empty domain by (24.5.1). Equation (24.5.1) simply reproduces the ordinary operation in the target row. The empty lifted signature has the unique algebra $E_{\mathsf{nil}}$, because there is no operation case to define.

A modular catch elaborator

The target signature contains an ordinary exception operation $$\mathsf{throw}:\mathbf{1}⇝\mathbf{0}.$$

We also use $$\mathsf{maybe}(f,N)(\mathsf{some}(x))=f(x),\mathsf{maybe}(f,N)(\mathsf{none})=N.$$

The first branch is interpreted as protected computation. Its throw effect is handled locally, producing a possible result in the residual target row; mask then places that residual tree back in the full target row. On $\mathsf{some}(x)$, the operation continuation receives $x$. On $\mathsf{none}$, the fallback runs and its result is supplied to the same continuation.

Proof of Proposition 24.19 — Typing of the catch clause

Proof. The fork type is the first family of (24.9), specialized by (24.4). Equations (24.16) and (24.16) type the two nested transformations. The second family of (24.9) types the continuation, and ordinary free-monad bind types $\hat{\psi }(\mathsf{ff})\gg =\hat{k}$. Both branches of (24.6) have type ${\mathsf{Free}}_{\mathrm{\Delta }}(A)$. Therefore $$\mathsf{maybe}(\hat{k},\hat{\psi }(\mathsf{ff})\gg =\hat{k}):\mathsf{Maybe}(\mathsf{Val}(t))\to {\mathsf{Free}}_{\mathrm{\Delta }}(A).$$ Binding the masked computation to this function has type ${\mathsf{Free}}_{\mathrm{\Delta }}(A)$. ◻

Thus the catch algebra is well typed, which is the operation case of theorem 24.13. No separate preservation proof is needed because the branch and continuation result indices are arguments of the clause type itself.

Composition by disjoint cases

A global elaborator should contain no clause which knows how many other operations exist. Disjoint signature sum makes that requirement a case split.

Proof of Theorem 24.23 — Modular elaboration equations

Proof. The algebra type follows from (24.2): every operation is either an $H_1$-operation or an $H_2$-operation, and its fork and return types reduce to those of the selected summand. Expand (24.5), then apply the corresponding equation of (24.22). No other case occurs. ◻

For three higher-order signatures, define the reassociation bijection on operation tags by Its inverse uses the three equations in reverse. Case reduction in section 24.2 gives, for every tag $u$, canonical bijections $${\mathsf{Op}}_{{\mathsf{Fork}}_{(H_1⊞H_2)⊞H_3}(u)}\cong {\mathsf{Op}}_{{\mathsf{Fork}}_{H_1⊞(H_2⊞H_3)}(\rho u)}$$ and equal response sets at corresponding fork tags, together with $${\mathsf{Ret}}_{(H_1⊞H_2)⊞H_3}^{\mathsf{H}}(u)\cong {\mathsf{Ret}}_{H_1⊞(H_2⊞H_3)}^{\mathsf{H}}(\rho u).$$ These maps are the identity after the relevant $H_i$-case is selected. The reassociation transport sends an operation by $\rho$, reindexes each fork along the first bijection and its response equality, and reindexes the continuation along the last bijection. These are the three transports used below.

Proof of Proposition 24.24 — Composition coherence under reassociation

Proof. Case-analyze the transported operation tag. An $H_1$-tag dispatches to $E_1$ on both sides, an $H_2$-tag to $E_2$, and an $H_3$-tag to $E_3$. In every case the fork and continuation are recursively translated by the same combined elaborator. Pointwise equality at every fork and response index, followed by function extensionality, equates the two transported function fields. ◻

State, throw, and catch in one tree

Let $\mathsf{State}$ be the ordinary signature with operations $$\mathsf{put}:\mathbb{N}⇝\mathbf{1},\mathsf{get}:\mathbf{1}⇝\mathbb{N}.$$ Thus $\mathsf{put}(n)$ is the operation instance carrying parameter $n:\mathbb{N}$; its response is $\star :\mathbf{1}$. Consider the source and target signatures The component elaborators compose as $$E_{\mathsf{tr}}:=E_{\mathsf{lift}\mathsf{,}\mathsf{State}}⋎E_{\mathsf{lift}\mathsf{,}\mathsf{Throw}}⋎E_{\mathsf{catch}}⋎E_{\mathsf{nil}}.$$ The displayed rows are duplicate free, so proposition 24.15 gives one insertion witness at each component boundary. Equation (24.8) records the semantic order of the four components.

The transaction is The catch handles the throw, but its target clause forwards state. Hence the state update to $2$ survives the failed protected branch.

This is the finite model’s $\mathsf{hSt}$ observation. The handler of chapter 22 that returns $(x,s)$ is a different interface; substituting it would change the proposition’s result type.

Proof of Proposition 24.26 — Global-state transaction calculation

Proof. First expose the catch clause. The protected target tree is $\mathsf{put}(2)\gg \mathsf{throw}$. The local throw handler forwards the put and handles the following throw: Masking reinjects this residual state tree into ${\mathrm{\Delta }}_{\mathsf{tr}}$. Expose the $\mathsf{none}$ branch, fallback bind, and unit conversions separately. Abbreviate the forwarded target and the fallback by Then the remaining calculation fits on one semantic step per line: Now use the four equations of equation 24.4; no state transition is hidden in prose: Consequently $${\mathsf{runState}}_0({\mathsf{elaborate}}_{E_{\mathsf{tr}}}(\mathsf{transact}))=\mathsf{pure}(2).$$ Finally, the pure equation of equation 24.1 gives $$\mathsf{runThrow}(\mathsf{pure}(2))=\mathsf{pure}(\mathsf{some}(2)),\mathsf{un}(\mathsf{pure}(\mathsf{some}(2)))=\mathsf{some}(2),$$ which is the displayed result. ◻

The source operation is an interface, not a fixed semantics. Replace only the catch component by $$E_{\mathsf{protected}}(\mathsf{catch}(t),\psi ,k):=\psi (\mathsf{tt})\gg =k.$$ This component always runs the protected branch and never handles its throw. All other components in (24.8) remain unchanged. The same source transaction then reaches the outer throw handler and returns $\mathsf{none}$. The change is local to one algebra clause.

Lawfulness is stated after observation

Intrinsic typing ensures that the catch clause returns a target tree of the right result type. It does not ensure that the clause behaves like exception catch. Lawfulness is an equational obligation on the interpretation obtained after elaboration and handling.

For this section put the target throw signature at the front: $\mathsf{Throw}{\oplus }_{\mathsf{sig}}\epsilon$. Let $$h_A:{\mathsf{Free}}_{\mathsf{Throw}{\oplus }_{\mathsf{sig}}\epsilon }(A)\to {\mathsf{Free}}_{\epsilon }(\mathsf{Maybe}(A))$$ be the throw handler, and let $${\mathsf{mask}}_A:{\mathsf{Free}}_{\epsilon }(A)\to {\mathsf{Free}}_{\mathsf{Throw}{\oplus }_{\mathsf{sig}}\epsilon }(A)$$ be masking. These are the front-summand instances of ${\mathsf{runThrow}}_w$ and ${\mathsf{mask}}_w$ from (24.1), (24.2); this section suppresses the unique canonical witness and writes $h$ and $\mathsf{mask}$ to keep the law equations legible. Let $$E_0:\mathsf{Elaboration}(H,\mathsf{Throw}{\oplus }_{\mathsf{sig}}\epsilon )$$ be any elaboration for the remaining higher-order operations, and define Thus $$\mathsf{run}:{\mathsf{Hefty}}_{\mathsf{Lift}(\mathsf{Throw})⊞\mathsf{Catch}⊞H}(A)\to {\mathsf{Free}}_{\epsilon }(\mathsf{Maybe}(A)).$$

Two structural facts about the target handler contain the proof mechanism.

Proof of Lemma 24.27 — Throw handling distributes through bind

Proof. Induct on $m$. If $m=\mathsf{pure}(x)$, both sides are $h(f(x))$. If $m$ is throw, both sides are $\mathsf{pure}(\mathsf{none})$. If $m$ is a residual operation $\mathsf{impure}(o,k)$, handling and bind both forward it. The two sides are operation nodes with continuation families $$r\mapsto h(k(r)\gg =f)\text{and}r\mapsto h(k(r))\gg =\mathsf{maybe}(h\circ f,\mathsf{pure}(\mathsf{none})),$$ which agree pointwise by the induction hypothesis. ◻

Proof of Lemma 24.28 — Handling a masked tree

Proof. Induct on $n$. A pure value is mapped to $\mathsf{pure}(\mathsf{some}(x))$ on both sides. A residual operation is forwarded by $\mathsf{mask}$, then forwarded by $h$; ordinary bind also forwards it. The continuation families agree by the induction hypothesis. ◻

These lemmas reduce the higher-order catch operation to an ordinary equation on handled results.

Proof of Proposition 24.29 — Observable catch equation

Proof. Write $m_i={\mathsf{elaborate}}_E(M_i)$, and abbreviate $$q_2=\mathsf{maybe}(\mathsf{pure},m_2),Q_2=\mathsf{maybe}(h\circ q_2,\mathsf{pure}(\mathsf{none})).$$ Expand the smart constructor, then the catch algebra, and only then use the right unit: Apply lemma 24.27 and then lemma 24.28: $$h(\mathsf{mask}(h(m_1))):{\mathsf{Free}}_{\epsilon }(\mathsf{Maybe}(\mathsf{Maybe}(A))),z:\mathsf{Maybe}(A).$$ The outer $\mathsf{Maybe}$ records the result of handling the masked tree; the inner one is the result already produced by $h(m_1)$. For $z=\mathsf{some}(x)$, the final function returns $\mathsf{pure}(\mathsf{some}(x))$; for $z=\mathsf{none}$, it returns $h(m_2)$. Substituting $R_i=h(m_i)$ gives (24.29). ◻

Proof of Theorem 24.30 — Lawfulness equations for modular catch

Proof. A lifted throw has no response. Hefty bind changes only its impossible continuation, so bind–throw is immediate after elaboration and handling.

For the remaining equations use (24.29). Since $$\mathsf{run}(\mathsf{pure}(x))=\mathsf{pure}(\mathsf{some}(x)),\mathsf{run}({\mathsf{throw}}^{\mathsf{H}})=\mathsf{pure}(\mathsf{none}),$$ catch–return and catch–throw${}_1$ are the two left-unit cases of (24.29). For catch–throw${}_2$, the branch function becomes $$\mathsf{maybe}(\mathsf{pure}\circ \mathsf{some},\mathsf{pure}(\mathsf{none}))=\mathsf{pure},$$ pointwise on $\mathsf{Maybe}(A)$. Equation (24.29) therefore reduces to the right unit of target bind.

For (24.30), substitute the first assumed equality for the left operand of the bind in (24.29). The second assumed equality says that the two branch functions agree at every returned value. Function extensionality equates those functions, and congruence of target bind gives the result. ◻

The equalities are deliberately stated after $\mathsf{run}$. Two source trees may elaborate to different target trees yet become equal after the throw handler observes them. Replacing (24.30) by raw syntactic equality would state a stronger and generally false interface.

Three syntaxes, three invariants

Scoped syntax and hefty trees both add recursive positions beyond an ordinary continuation, but enforce different invariants:

A scoped signature distinguishes one particular binding pattern and carries explicit substitution equations. A hefty signature records a dependent family of computation arguments and leaves their target arrangement to the elaboration clause. A translation must map the scoped body and continuation to explicit fork and response indices, and it must commute with scoped substitution: translating after substitution must equal target bind after translation. The constructor shapes alone establish none of these equations.

Mechanized boundary.

The published Agda development formalizes the indexed definitions, modular composition, catch equations, and concrete transaction normalizations used here. Its lawfulness interface assumes function extensionality, and its bind-throw field proves the homogeneous result-code instance; the heterogeneous form in theorem 24.30 is proved locally. The finite Kappa capsule checks the displayed elaboration equations. Neither artifact contains a source operational semantics or a source–target simulation theorem; appendix E records the exact archive and executable boundaries.

The definitions and selected examples in this chapter follow Poulsen and van der Rest’s intrinsically typed Agda development and its accompanying paper [PvdR23]. The proofs are reconstructed locally at the signatures displayed here; the citation supplies provenance, not omitted premises.

Suggested first pass.

Begin with exercise 24.12, exercise 24.13, continue with exercise 24.14, and finish with the practical project exercise 24.17.

Exercise 24.12¶

★★★ For the three-branch signature of exercise 24.2, take $${\mathsf{Fork}}_{\mathsf{First}}(\mathsf{first}(t))=(\{0,1,2\},\lambda \mathrm{\_}.\mathsf{Val}(t)),{\mathsf{Ret}}_{\mathsf{First}}^{\mathsf{H}}(\mathsf{first}(t))=\mathsf{Val}(t).$$ Thus this exercise is independent of the earlier exercise’s answer. Define an elaborator which runs the branches from left to right, treating target throw as failure and returning the first successful value. If all three branches throw, emit one target throw. Give the complete algebra clause, including every mask, handler, bind, and $\mathsf{maybe}$; then derive the types of all intermediate terms. Calculate its action on $$\mathsf{first}({\mathsf{throw}}^{\mathsf{H}},\mathsf{pure}(2),\mathsf{pure}(3)).$$

Referenced from 4 locations

• Higher-Order Algebraic Effects and Modular Elaboration
• ch:higher-order-effects: ch:higher-order-effects

Exercise 24.13¶

★★☆ Starting from (24.18), reprove catch–throw${}_2$ directly by structural induction on the elaborated target tree, without using proposition 24.29. State the induction predicate, and give the pure, throw, and forwarded-operation cases. Compare the resulting proof with the factorized proof through lemma 24.27, lemma 24.28.

Referenced from 4 locations

• Higher-Order Algebraic Effects and Modular Elaboration
• ch:higher-order-effects: ch:higher-order-effects

Exercise 24.14 — (*)¶

★★☆ Define the pair-returning observation ${\mathsf{runState}}_s^{\times }$. Replace only the pure equation of equation 24.4 with $${\mathsf{runState}}_s^{\times }(\mathsf{pure}(x))=\mathsf{pure}(x,s)$$ and retaining the put, get, and forwarding equations. Put $$T:={\mathsf{elaborate}}_{E_{\mathsf{tr}}}(\mathsf{transact}).$$ Calculate $$\mathsf{runThrow}({\mathsf{runState}}_0(T))\text{and}\mathsf{runThrow}({\mathsf{runState}}_0^{\times }(T)).$$ Explain why the results are $\mathsf{some}(2)$ and $\mathsf{some}(2,2)$, respectively, and why this comparison changes only the observation of final state, not catch’s rollback policy.

Referenced from 4 locations

• Higher-Order Algebraic Effects and Modular Elaboration
• ch:higher-order-effects: ch:higher-order-effects

Exercise 24.15 — (*)¶

★★★ Generalize exercise 24.8 to a finite binary tree of higher-order signature sums. Define a canonical flattening to a list of summands, transport every operation, fork, and return index along the flattening, and prove that any two parenthesizations of the same ordered list of component elaborators agree after transport. Explain why permutation of the list is an additional theorem rather than part of reassociation.

Referenced from 3 locations

• Higher-Order Algebraic Effects and Modular Elaboration
• ch:higher-order-effects: ch:higher-order-effects

Exercise 24.16¶

★★★ Consider the finite source grammar $$M::=\mathsf{return}(n)\mid \mathsf{put}(n)\mid \mathsf{get}(x.M)\mid \mathsf{throw}\mid \mathsf{catch}(M,M)\mid M;M$$ and configurations $⟨s,M⟩$. Read this as a sorted grammar: $\mathsf{put}(n):\mathbf{1}$, $\mathsf{get}:\mathbb{N}$, catch’s branches have one result sort, and sequencing discards its left result. Define the embedding $\lceil -\rceil$ into the intrinsically sorted hefty syntax by The transaction from (24.8) is now expressible using the final sequencing clause. The root steps are plus left congruence under catch and sequencing. Relate $⟨s,M⟩$ to the target tree $${\mathsf{runState}}_s({\mathsf{elaborate}}_{E_{\mathsf{tr}}}(\lceil M\rceil )).$$ For each of the five roots, show a nonempty target calculation to the tree related to the source reduct; in the catch–throw case expose the catch clause before using equation 24.1, equation 24.2. Then state one property still outside this finite simulation (for example, inference into intrinsically typed hefty syntax or absence of unhandled operations for arbitrary sums).

Referenced from 4 locations

• Higher-Order Algebraic Effects and Modular Elaboration
• ch:higher-order-effects: ch:higher-order-effects
• Higher-order signatures and modular elaboration

Exercise 24.17¶

★★★ Practical project.hefty-elaboration Implement the finite source and target fragments used in example 24.7, proposition 24.26. The source must represent pure nodes, lifted state and throw operations, a catch node with two computation arguments, the correct bind (24.6), the incorrect structural bind (24.3), the catamorphic elaborator (24.5), and composition by operation-tag dispatch. The target must implement free-tree bind, state handling, throw handling, and empty-signature elimination.

Maintain this invariant: every node carries a result-type tag; both catch branches have the operation’s declared branch type; the operation continuation returns the node’s result type; and each source operation tag is accepted by exactly one elaboration component. Produce four decidable checks:

1. the global transaction returns $\mathsf{some}(2)$;

2. replacing only the catch component by (24.8) returns $\mathsf{none}$;

3. the correct bind makes the counted example return $1$, while (24.3) makes it return $2$;

4. constructing a catch whose branches have different result tags is rejected before elaboration.

The accepted run must report all four outcomes and terminate unsuccessfully if any expected value changes.

Referenced from 5 locations

• Higher-Order Algebraic Effects and Modular Elaboration
• Object calculus checker and evaluator
• ch:higher-order-effects: ch:higher-order-effects