Higher-order algebraic effects and modular elaboration

The source is the intrinsically indexed family ${\mathsf{Hefty}}_H(A)$ for a strictly positive higher-order signature $H$. Each operation has an ordinary fork signature for its owned nested computations and a separate ordinary response type for its continuation. The target is the ordinary free tree ${\mathsf{Free}}_{\mathrm{\Delta }}(A)$. Ordinary signature sum ${\oplus }_{\mathsf{sig}}$ and higher-order signature sum $⊞$ are distinct operations with distinct operand sorts.

Source bind traverses only an operation’s continuation. It satisfies left unit, right unit, and associativity by theorem 24.8. The structural catamorphism instead traverses both the fork and continuation families. Its pointwise family uniqueness is lemma 24.11. The homogeneous bad-bind calculation is a counterexample to identifying these two traversals.

An elaboration is a hefty algebra into $G(X)={\mathsf{Free}}_{\mathrm{\Delta }}(X)$ with generator $\mathsf{pure}$. Typing by construction is exactly theorem 24.13: an already indexed source tree is mapped to a target tree at the same result index. Operation-tag dispatch composes two algebra components by theorem 24.23. Associativity of this composition is only after transport along the canonical reassociation of signature sums, as stated in proposition 24.24. Duplicate-free ordered rows have canonical insertion witnesses by proposition 24.15; repeated summands keep their witnesses explicit and have no claimed coherence theorem.

The catch component first handles target throw in the protected translated tree, reinjects residual operations by ${\mathsf{mask}}_w$, and chooses between the ordinary continuation and the translated fallback. The observable catch equation and its four scoped laws are proposition 24.29, theorem 24.30. The state handler in proposition 24.26 discards the final state and computes $\mathsf{just}(2)$; the pair-returning state observation is a different result interface.

The archived Agda development is at commit 539a2a6bcdf1c3d9ad9a4e186c39302ea365b6ab. Its reusable catch-law module src/Law/Hefty/Catch.agda imports function extensionality from src/Postulate/Extensionality.agda. The concrete transaction equations in src/Example/Hefty/Catch+Throw+State.agda close by refl; the general function-equality interface is relative to the postulate. Its published bind-throw field is homogeneous: although it names two result codes, the continuation begins and ends at the first code. The heterogeneous bind–throw clause of theorem 24.30 is a local theorem proved from the displayed source-bind and throw equations, not an exact field of that interface.

Intrinsic result indices do not provide a surface parser, type inference, operational simulation, progress, termination, or absence of unhandled target operations. The local finite simulation exercise proves only its displayed five-root fragment. The Kappa companion checks tagged finite observations and finite per-tag component dispatch; it is neither a mechanization of the indexed definitions nor evidence for the chapter’s universal theorems.