ch:higher-order-effects: ch:higher-order-effects

If the raw source computations are stored in the operation tag, the catch component must be polymorphic in the result type of the whole folded tree. Its shape is The continuation has already been folded, but the two arguments still have type ${\mathsf{Syntax}}_H(A)$, not $G(A)$. To use them, the component would need an additional polymorphic argument $${\tau }_X:{\mathsf{Syntax}}_H(X)⟶G(X)\text{for every }X.$$ This is a translator for the complete source signature $H$. It cannot be supplied by the catch component alone, because either source computation may contain any operation of $H$. Adding a new summand to $H$ therefore changes the argument expected by the catch clause, which is exactly the lost modularity.

Let $\mathbf{3}=\{0,1,2\}$. Define one operation $\mathsf{first}(t)$ for each $t:\mathsf{Ty}$, and put For $M_i:{\mathsf{Hefty}}_H(\mathsf{Val}(t))$, the smart constructor is $$\mathsf{first}(M_0,M_1,M_2)=\mathsf{impure}(\mathsf{first}(t),\psi ,\mathsf{pure}),$$ where $$\psi (0)=M_0,\psi (1)=M_1,\psi (2)=M_2.$$ Every fork component has the result index demanded by its position, and the operation continuation receives the selected value.

With the correct bind, the branches of $C$ remain pure and the continuation is $g$. The selected branch returns $\star$, the continuation emits one $\mathsf{tick}$, and $\mathsf{readTicks}$ therefore returns $1$: $$C\gg {=}_{\mathsf{H}}g{\gg }_{\mathsf{H}}\mathsf{readTicks}⟶\mathsf{tick}\gg \mathsf{readTicks}⟶1.$$ For the structural bind (24.3), the selected branch is first changed from $\mathsf{pure}(\star )$ to $\mathsf{tick}$, and the node continuation is also $g$. After the branch tick returns, the continuation emits the second tick: $$C{\mathsf{bind}}^{\times }g{\gg }_{\mathsf{H}}\mathsf{readTicks}⟶\mathsf{tick}\gg \mathsf{tick}\gg \mathsf{readTicks}⟶2.$$ Both programs remain well typed. The count exposes the misplaced recursive call.

Expanding the definition through (24.6) gives The identity law is the right-unit equation of theorem 24.8: $${\mathsf{fmap}}_{\mathsf{H}}(\mathsf{id},M)=M\gg {=}_{\mathsf{H}}\mathsf{pure}=M.$$ For composition, associativity and the left unit give

Work in the fixed-type catch fragment specified in the exercise. Choose $x\ne y:A$ and a constant $g:A⟶{\mathsf{Hefty}}_H(B)$, say $g(a)=\mathsf{pure}(b_0)$. Put $$C_x=\mathsf{catch}(\mathsf{pure}(x),\mathsf{pure}(x)),C_y=\mathsf{catch}(\mathsf{pure}(y),\mathsf{pure}(y)).$$ A structural catamorphism with generator $g$ presents the same data to its operation algebra in both cases. The operation tag is the same, each folded fork component is $$g(x)=\mathsf{pure}(b_0)=g(y),$$ and the folded continuation is $g$ in both trees. Hence a fixed component ${\beta }_g$ must return the same result for $C_x$ and $C_y$.

Correct bind does not return the same result. Equation (24.3) gives Their forks differ because $x\ne y$. Thus no algebra which sees only the recursively folded fields can define hefty bind for every $g$.

The source smart constructor has an empty fork. Its operation continuation returns the source response after the transport supplied by the higher-order insertion witness; that transport is definitionally trivial for the front summand. Applying (24.5), then (24.5.1), gives $${\mathsf{elaborate}}_{E_{\mathsf{lift},w}}(\uparrow o)=\mathsf{impure}({\iota }_w^{\ell }(o),\mathsf{pure}\circ q_{w,o}^{\ell }).$$ A target response has type $$r:{\mathsf{Ret}}_{\mathrm{\Delta }}({\iota }_w^{\ell }(o)).$$ The transport $$q_{w,o}^{\ell }(r):{\mathsf{Ret}}_{{\mathrm{\Delta }}_0}(o)$$ converts it to the response expected by the source operation continuation, and $\mathsf{pure}$ returns that response in the target tree.

Correct hefty bind leaves both catch branches unchanged and replaces the catch continuation by $f$. After the catamorphism, the clause data are $$\hat{\psi }(\mathsf{tt})=\mathsf{throw},\hat{\psi }(\mathsf{ff})={\mathsf{elaborate}}_E(M),\hat{k}={\mathsf{elaborate}}_E\circ f.$$ Put $$N={\mathsf{elaborate}}_E(M),K={\mathsf{elaborate}}_E\circ f.$$ Substitution into (24.18) yields The translated continuation occurs once, as the continuation sequenced after the fallback result. It was not pushed into the fallback before the catch clause was interpreted.

The canonical reassociation sends operation tags by Its inverse is determined by reversing these three equations. The fork and return families on corresponding tags are definitionally the same component families, so transport changes only the nested sum tag.

For $o_1$, both composite algebras dispatch to $E_1$; for $o_2$, both dispatch to $E_2$; for $o_3$, both dispatch to $E_3$. In every case the fork and continuation arguments are passed through unchanged. Hence the algebras agree after transport along reassociation.

Without transport, the left algebra has domain $(H_1⊞H_2)⊞H_3$, while the right algebra has domain $H_1⊞(H_2⊞H_3)$. Literal equality would compare terms of different types.

The alternative component retains only the protected branch and sequences its result into the operation continuation. For (24.8), that continuation is the translation of $\mathsf{get}$. Thus The last equality uses the empty response type of throw: no continuation branch can reach get. The state handler, started at zero, performs $0\mapsto 1\mapsto 2$ and then forwards the throw. The outer throw handler maps that node to $\mathsf{none}$. The final state is not returned by the chosen state handler, but the update to $2$ occurs before the abort.

For $S:{\mathsf{Free}}_{\epsilon }(\mathsf{Maybe}(A))$, define $$q_S=\mathsf{maybe}(\mathsf{pure}\circ \mathsf{some},S).$$ Then (24.29) says that observable catch is $C(R,S)=R\gg =q_S$. Hence If $z=\mathsf{some}(x)$, the function in the last line returns $\mathsf{pure}(\mathsf{some}(x))$. If $z=\mathsf{none}$, it returns $R_2\gg =q_{R_3}=C(R_2,R_3)$. Therefore it is pointwise $q_{C(R_2,R_3)}$, and $$C(C(R_1,R_2),R_3)=C(R_1,C(R_2,R_3)).$$ Substitute $R_i=\mathsf{run}(M_i)$ and apply (24.29) in both directions. The proof concerns observed results; the two nested source trees have different constructor shapes.

1. This is exactly theorem 24.13.

2. This is a clause of theorem 24.30, not a consequence of typing alone.

3. Neither theorem supplies it. One needs a source operational semantics, a target step relation modulo administrative equations, and a simulation relation.

4. Neither theorem supplies it. One needs a closed-program effect invariant and a progress or handler-completeness theorem for the target.

5. Neither theorem supplies it. One needs a surface elaboration or typechecking algorithm and a soundness theorem relating its output to ${\mathsf{Hefty}}_H$.

Write $m_i=\hat{\psi }(i)$ and let $h={\mathsf{runThrow}}_w$. Put $$r_i={\mathsf{mask}}_w(h(m_i)).$$ A left-to-right component is Each $m_i$ has type ${\mathsf{Free}}_{\mathrm{\Delta }}(\mathsf{Val}(t))$. Therefore $$h(m_i):{\mathsf{Free}}_{{\mathrm{\Delta }}^{\prime }}(\mathsf{Maybe}(\mathsf{Val}(t)))$$ and $${\mathsf{mask}}_w(h(m_i)):{\mathsf{Free}}_{\mathrm{\Delta }}(\mathsf{Maybe}(\mathsf{Val}(t))).$$ The continuation has type $\hat{k}:\mathsf{Val}(t)⟶{\mathsf{Free}}_{\mathrm{\Delta }}(A)$, while the innermost target throw has type ${\mathsf{Free}}_{\mathrm{\Delta }}(A)$. Hence every $\mathsf{maybe}$ is a function from $\mathsf{Maybe}(\mathsf{Val}(t))$ to ${\mathsf{Free}}_{\mathrm{\Delta }}(A)$, and every displayed bind returns ${\mathsf{Free}}_{\mathrm{\Delta }}(A)$.

On the given input, handling the first branch produces $\mathsf{pure}(\mathsf{none})$, so evaluation continues to the second. The second branch produces $\mathsf{pure}(\mathsf{some}(2))$. Hence its $\mathsf{maybe}$ invokes $\hat{k}(2)$. For the smart constructor, $\hat{k}=\mathsf{pure}$, so the result is $\mathsf{pure}(2)$. The third branch is not inserted into the target tree.

Let $h={\mathsf{runThrow}}_w$ and let ${\mathsf{mask}}_w$ be the masking map of equation 24.2. Let $\mathsf{throw}$ denote the target throw tree. The required induction predicate is $$P(m):h({\mathsf{mask}}_w(h(m))\gg =\mathsf{maybe}(\mathsf{pure},\mathsf{throw}))=h(m).$$ This is the target equality obtained by expanding $\mathsf{run}(\mathsf{catch}(M,{\mathsf{throw}}^{\mathsf{H}}))$.

If $m=\mathsf{pure}(x)$, then $$h(m)=\mathsf{pure}(\mathsf{some}(x)).$$ The masked tree binds through the some branch to $\mathsf{pure}(x)$. The outer handler returns the displayed value, which is $h(m)$.

If $m=\mathsf{throw}$, then $h(m)=\mathsf{pure}(\mathsf{none})$. The maybe function selects target throw, and the outer handler returns $\mathsf{pure}(\mathsf{none})=h(m)$.

If $m=\mathsf{impure}(o,k)$ for a residual operation $o$, then the inner handler, masking, bind, and outer handler all forward $o$. The left side of (B.1) is $$\mathsf{impure}(o,\lambda r.h({\mathsf{mask}}_w(h(k(r)))\gg =\mathsf{maybe}(\mathsf{pure},\mathsf{throw}))),$$ while the right side is $\mathsf{impure}(o,h\circ k)$. They agree pointwise by the induction hypothesis.

This direct proof fuses three traversals into one induction predicate. The factorized chapter proof isolates handler–bind distribution. It also isolates handler–mask interaction, then obtains catch–throw${}_2$ from the ordinary right-unit law. The direct proof is shorter for this law; the factorized proof also supplies observable catch and congruence.

The catch calculation is independent of the final-state observation. By (24.8), both runs receive the same target tree $T_{\mathsf{tr}}$, where $$T_{\mathsf{tr}}:=\mathsf{put}(1)\gg \mathsf{put}(2)\gg \mathsf{get}.$$ The discard-state equations of (24.4) give The outer throw handler therefore returns $\mathsf{pure}(\mathsf{some}(2))$, and empty-signature elimination yields $\mathsf{some}(2)$.

The pair-returning handler takes the same two state transitions and the same get response. Only its pure equation differs: After $\mathsf{runThrow}$ and empty-signature elimination, the result is $\mathsf{some}(2,2)$. Both handlers observe the committed update $0\mapsto 1\mapsto 2$; the second merely exposes the final store. Thus the comparison changes the result interface, not the catch elaborator or its rollback policy.

Represent a parenthesized sum by a binary tree whose leaves are the ordered signatures $[H_1,\dots ,H_n]$. Define $\mathsf{flatten}$ by concatenating the leaf lists. An operation tag in the tree determines a unique leaf index $i$ and a component operation $o:{\mathsf{Op}}_{H_i}^{\mathsf{H}}$: descend left or right according to its sum injections and count the leaves skipped on right descents. Conversely, a leaf index and component operation rebuild a unique tag by following the tree. These maps are inverse by induction on the binary tree.

Transport the fork and return families by the same recursion. At a leaf they are the component families. At an internal node, a left or right tag reduces to the corresponding child family, so transport introduces no new data beyond the equality identifying the selected leaf.

Now associate to each ordered list of elaborators $[E_1,\dots ,E_n]$ the flattened dispatcher which sends leaf index $i$ to $E_i$. Induction on either parenthesization shows that its iterated $⋎$-composition transports to this dispatcher. Hence any two parenthesizations agree after both are transported to the common flattened signature.

A permutation changes the leaf index assigned to an operation. Proving invariance under it requires an explicit permutation of operation tags and a corresponding reordering of component elaborators. Reassociation preserves the ordered list and therefore cannot supply that theorem.

Abbreviate Write $$⟨s,M⟩RT⟺T{=}_{\mathrm{adm}}{T}_s(M),$$ where ${=}_{\mathrm{adm}}$ is generated by the free-monad units and associativity together with the displayed handler and mask equations. The five source roots have the following nonempty target calculations. For return sequencing, preservation of source bind by the catamorphism and target left unit give the following result. The embedding clauses used here are $$\mathcal{E}(\mathsf{get}(x.M))=\mathsf{get}\gg =(\lambda x.\mathcal{E}(M)),\mathcal{E}(M;N)=\mathcal{E}(M)\gg \mathcal{E}(N).$$ Thus get consumes its returned value by bind, whereas source sequencing discards its left result. The return calculation is

For put, For get, Thus the last tree is related to $⟨s,M[s/x]⟩$.

For a successful catch, the pure equation of the throw handler is $$\mathsf{runThrow}(\mathsf{pure}(n))=\mathsf{pure}(\mathsf{some}(n)).$$ Masking and target bind then select the success continuation: For a thrown protected branch, For completeness, the congruence obligation is the following compatibility lemma, proved by induction on the one-step derivation (sequencing and catch are the two context cases): if $⟨s,P⟩{⟼}_{\mathsf{H}}⟨s^{\prime },P^{\prime }⟩$, then substituting $\mathcal{E}(P)$ by its nonempty admissible calculation to $\mathcal{E}(P^{\prime })$ inside either the sequencing continuation or the displayed catch context—including $\mathsf{mask}(\mathsf{runThrow}([]))\gg =F_N$—gives the related tree at state $s^{\prime }$. Compatibility of target bind, $\mathsf{runThrow}$, mask, and $\mathsf{runState}$ with their displayed equations proves each induction step; the state parameter changes only in the put case already calculated above. This is the needed lemma, rather than an unstated appeal to ordinary term congruence.

This proves the requested root simulation for the finite grammar. It does not supply surface type inference, a theorem for arbitrary higher-order sums, or absence of unhandled operations in an arbitrary target tree.