Operation trees, CBPV, and deep handlers

Chapter 22 first fixes a finite many-sorted operation signature and its well-founded free trees $T_{\mathrm{\Sigma }}A$. Return, bind, and handler folds are structural definitions on those trees. There is no recursion, divergence, hidden store, or equation between effect operations in this signature. Effect-specific theories enter only through an explicitly declared quotient.

The monad laws and operation algebraicity are lemma 22.4, proposition 22.5. Fold existence and uniqueness and its homomorphism equation are theorem 22.8, corollary 22.9. Descent through an effect quotient is equivalent to equalizing every generator under every tree-valued instantiation. Whole-$\mathrm{\Sigma }$-algebra validity under every carrier-valued assignment is a sufficient, stronger condition; no isolated clause check is sufficient.

The source is the simply typed lambda calculus over declared base constants, with the four named rules S-Var, S-Const, S-Lam, and S-App, and separate call-by-value and call-by-name big-step relations. The target ${\mathsf{CBPV}}_0$ has base values, thunks, returns, sequencing, forcing, and value-to-computation functions. Its reductions are exactly To, Force, Beta, and their Frame closure; weak evaluation does not enter a thunk or lambda.

Weakening and the two substitution lemmas, canonical terminal forms, and safety are lemma 22.12, lemma 22.13, theorem 22.14. Typing and substitution for both translations are lemma 22.15, lemma 22.16. Administrative transport and exact translated-trace phase decomposition are lemma 22.17, lemma 22.18. Preservation and reflection of the two source evaluations are precisely theorem 22.19; call by name is compared only up to the declared force–thunk administrative congruence.

The extension has finite closed effect sets, effect-annotated thunks and computation arrows, explicit operation requests, deep handlers, and effect weakening. Handler typing includes the return clause, every distinct handled operation clause, the exact resumed-continuation type, and the set-difference forwarding premise. Operational reduction selects the nearest matching handler through an operation-open context, reinstalls that handler in every resumption, and explicitly rebuilds an unhandled request.

The exact structural and replacement lemma is lemma 22.23. Operation-open-context decomposition is lemma 22.24. Preservation is theorem 22.25; progress up to a named exposed operation is theorem 22.26; and the empty-effect corollary is corollary 22.27. In the handled-operation case, response substitution is followed by C-Weaken before replacement; the reinstalled continuation then receives the handler’s output effect.

The reification theorem applies only to the displayed first-order fragment and its two administrative resumption forms. Open-context reification and deep-continuation substitution are lemma 22.29, lemma 22.30. Every listed one-step reduction preserves the exact reified tree, and finite handler evaluation agrees with the corresponding fold, by theorem 22.31.

The agreement theorem excludes arbitrary higher-order application frames, general recursion, and extra effect equations. The isolated shift/reset calculation proves only failure of an algebraicity-style context-commutation law; it imports no control typing or answer-type theorem. Closed sets provide safe upper bounds but no effect polymorphism, generalization, row unification, or one-occurrence removal for duplicate labels. Those are obligations of the following chapters.

A pinned Kappa companion executes finite first-order operation-tree, sequencing, state and exception order, and deep-handler cases. Its frozen output and negative mutations are implementation checks only. They prove none of the metatheorems above and do not enlarge the printed signature.