ch:algebraic-effects: ch:algebraic-effects

Problem, result, and invariant. Implement the finite CBPV and algebraic-operation examples behind the chapter’s handler calculations. The result is the eight-case report in appendix E. A deep handler must reinstall itself in every continuation, while a forwarded node must retain both its request and recursively handled continuation.

Representation. Use separate nominal datatypes for values, first-order operation trees, defunctionalized post-computations, handler results, and the small force/thunk machine. Give Boolean-response operations explicit false and true branches. This finite representation avoids using Kappa effects as the oracle.

First complete version. Define bindTree by pushing a continuation through returns and every operation branch. Add force/thunk and sequencing. Test left and right unit, one associativity instance, and algebraicity at an explicit choice node.

Remaining cases. Implement state and exception folds in both orders and reproduce rollback versus commit, then their agreement on successful return. Forward an unhandled state request through exception handling. Implement the deep twice-choice handler by recursively handling both response branches before sequencing them, and compare its choice-node equation with the tree fold.

A failing version. Leave the nested true choice branch unhandled. The program still typechecks, but the deep-handler case exposes the residual choice. Reusing the old state after put and discarding a forwarded get provide independent controls for state and forwarding.

Acceptance test. Run the four gates in appendix E. Require eight exact PASS lines, the frozen summary, and empty audit output. Replay the shallow-choice, old-state-at-put, and discarded-get mutations; every mutant must remain type-correct and fail its named oracle case.

Mathematical boundary. The artifact checks finite monad-law instances, handler order, forwarding, deep reinstallation, and one operational/tree equation. It proves neither the monad laws, algebraicity, handler safety, CBPV simulation, quotient soundness, contextual equivalence, nor the later open effect-collection result.