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

Problem, result, and invariant. Implement the finite catch, throw, and state fragment used by example 24.7, proposition 24.26. The finished Kappa program must distinguish source bind from structural recursion and the global catch component from the first-component-only alternative. Its five acceptance observations are $\mathsf{just}(2)$, failure for the alternative transaction, final states $1$ and $2$ for the two bind designs, and rejection of a catch with a mismatched fallback tag.

Maintain this invariant: every source and target tree has one result tag; both catch-owned branches have the catch branch tag; the catch continuation accepts that branch tag and returns the enclosing result tag; and each operation tag is dispatched to exactly one elaboration component. Kappa checks the finite tag discipline explicitly. It does not replace the indexed Agda signature.

Representation. Use ValueTag for UnitTag and NatTag, and keep values separate from tags. Represent source computations by HTree: pure, get, put, throw, and catch nodes. A catch stores two source subtrees and one defunctionalized HPost continuation. Target computations use a separate TTree without higher-order branches and a separate TPost. The distinction makes it impossible to confuse a source branch with an ordinary target continuation merely because both are implemented as trees.

Defunctionalized continuations are preferable here to host functions: Kappa can inspect their input and output tags, compose them explicitly, and traverse them structurally. A host-function encoding would be shorter, but its domain, codomain, and equality would be outside the finite checker.

First complete version. Begin with treeTag. Add postInputTag and postOutputTag. Then implement makeCatch. It returns None unless the protected tree, fallback tree, and continuation have precisely the four tags required by the catch constructor. Test one valid unit catch and the invalid unit/natural fallback before writing an evaluator.

Next implement source bind. Its catch case is the decisive one:

case HCatch branchTag _ protected fallback after ->
  HCatch branchTag (postOutputTag post)
    protected fallback (HCompose after post)

The protected and fallback fields are copied unchanged. Only the ordinary continuation is composed with post. At this point the counted-catch program can already expose the source tree produced by one bind.

Remaining cases. Implement target bind and target continuation application before elaboration. The elaborator recursively translates both owned branches in its catch case and converts the ordinary continuation. The GlobalCatch dispatcher handles throw in the protected target tree, selects the fallback only on failure, and then applies the converted continuation. The FirstComponentCatch dispatcher omits the fallback and therefore makes the chapter’s alternative semantics observable.

Add target evaluation in the order used by the transaction calculation: pure returns a value and current state, put replaces the state, get supplies the current state to its continuation, and throw returns Raised. The nominal continuations HTick and HRestoreTick implement the counted-bind witness: they read state, increment it, and return the saved value. Keep fuel explicit and choose it above every named finite example; an Exhausted result is a harness failure, never evidence of a semantic result.

A failing version. First replace the catch case of source bind by recursive calls on both owned branches. The program still typechecks, but the counted catch increments state twice rather than once. This is the executable form of the failed structural recursion in (24.3). Restore the source, then make FirstComponentCatch call the global handler. The alternative transaction now succeeds instead of raising. Finally omit the fallback-tag comparison in makeCatch; the malformed catch is accepted. As a fourth mutation, let ThrowComponent also own CatchOp; the unique-dispatch conjunct fails. Each mutation isolates a different invariant.

Acceptance test. Run the four commands in appendix E. The inline oracle requires exactly

PASS global transaction Just(2)
PASS alternative transaction Nothing
PASS correct bind state 1
PASS structural bind state 2
PASS mismatched catch rejected and operation dispatch unique
All 5 Chapter 30 corpus cases passed.

The test command must exit successfully and audit must print []. Replay each recorded mutation separately, check that the test command exits with failure, restore the accepted source, and rerun the four accepted commands.

Mathematical boundary. The program checks the distinction between owned branches and continuations in definition 24.6, the catamorphic traversal of definition 24.10, and the transaction of proposition 24.26. Finite tagged execution proves none of the chapter’s universal equations, intrinsic typing, modularity, or lawfulness results. The published Agda evidence and its function-extensionality boundary are recorded separately in Appendices D and E.