ch:scoped-operations: ch:scoped-operations

Problem, result, and invariant. The task is to make the one load-bearing distinction of definition 23.9 executable: ordinary operation branches are substituted recursively, whereas a scoped node preserves its ordinary parameters and owned computation and composes the post-computation only with its stored continuation. The Kappa model is finite and monomorphic so that these fields can be compared structurally.

The invariant maintained by bindProg is:

1. every Or branch is recursively bound;

2. the name and initial fields of Local are copied unchanged;

3. the ScopedComp field of Once and Local is copied unchanged; and

4. the new continuation is appended on the right of the stored continuation.

The observable result is the seven-line report fixed by exercise 23.15. Exact stdout is the decidable acceptance oracle.

Representation. The mathematical syntax is polymorphic in its result set and allows function fields. For an executable finite corpus, defunctionalize the continuation as $$\mathtt{\text{Kont}}::=\mathtt{\text{KDone}}\mid \mathtt{\text{KStep Step Kont}},$$ where Step contains AddOne, Double, and a branching ChooseSelfNext. A separate datatype ScopedComp contains the computation which lies inside a scope: SRet, SFail, and SOr. Finally use The two Nat fields of Local are the ordinary name and initial-state parameters. The next field is the owned computation, and the last field is the outside continuation.

One plausible alternative is to encode the whole tree in one recursive Prog datatype and represent a scope merely by Once Prog. That erases the distinction the project is supposed to test: a generic recursive traversal can then descend into the scope body without the type or representation making the error visible. A second alternative is to use Kappa functions directly for continuations. That is closer to the mathematics but gives the test oracle no structural equality on continuations. Defunctionalization makes composition order decidable.

First complete version. Start with Ret, Fail, and Or. Implement structural equality first. Then add the continuation functions appendKont and runKont. The ordinary bind clauses are

case Ret value -> runKont post value
case Fail -> Fail
case Or left right ->
  Or (bindProg left post)
     (bindProg right post)

The smallest end-to-end test binds AddOne through Or (Ret 1) (Or Fail (Ret 5)) and checks the exact tree Or (Ret 2) (Or Fail (Ret 6)). This establishes the ordinary algebraic baseline before scopes are introduced.

Remaining cases. Add Once next. Its correct clause is

case Once body kont -> Once body (appendKont kont post)

There is no recursive call on body. The body-preservation test binds a branching continuation onto an existing once node and checks both that the stored ScopedComp is unchanged and that the new continuation is present outside it.

Then add Local. Its clause is

case Local name initial body kont ->
  Local name initial body (appendKont kont post)

A dedicated case checks all three preserved fields simultaneously. This is the finite analogue of (23.21).

Finally, test the three monad equations on representative terms. Left unit is checked by binding a continuation to Ret 4; right unit uses KDone; associativity compares two successive binds with one bind by the appended continuation. These are finite instances only, but they force the implementation to use the same continuation order as the printed proof.

A failing version. The artifact constructs both nearby bad trees. False algebraicity pushes the new continuation into the body and resets the outside continuation:

case Once body kont ->
  Once (mapScoped body post) KDone

It therefore loses post from the outside position. This is the finite counterpart of (23.3).

The mutation harness targets the distinct all-fields traversal by replacing the once clause with

case Once body kont ->
  Once (mapScoped body post) (appendKont kont post)

implements the all-fields traversal from (23.16). It still type-checks in this deliberately homogeneous finite model, which is precisely why the semantic oracle is needed. The body-preservation case fails, as does the explicit comparison with the correct tree.

Two independent mutations target the other fields. Changing initial to initial + 1 demonstrates that ordinary parameters are not substitution targets. Replacing appendKont kont post by appendKont post kont demonstrates that continuation composition is ordered. Each mutant passes kappa check but fails the frozen stdout test.

Acceptance test. The accepted corpus must print, in order,

PASS ordinary substitution descends through ordinary branches
PASS scoped substitution preserves ordinary parameters
PASS scoped substitution leaves the scoped computation untouched
PASS scoped substitution composes only the continuation
PASS tested substitution equations and monad laws hold
PASS false algebraicity and all-fields traversal are distinguished
All 6 scoped-operations corpus cases passed.

Run all four required Kappa commands from the repository root. Then run artifacts/ch29-scoped-operations/run-mutations.sh. Each temporary semantic mutant must pass kappa check, produce an empty audit, and make both kappa test and kappa run exit nonzero. After the mutations the harness reruns all four commands on the untouched source. The compiler pins and raw command outcomes are recorded in appendix E.

Mathematical boundary. The program illustrates the constructor cases of definition 23.9 and finite instances of theorem 23.11. Executing six cases does not prove that substitution is well defined under arbitrary reindexing, that the laws hold for every well-founded scoped term, or that the nested and elementwise presentations agree. It proves nothing about handlers because the chapter has no operational handler language. Those distinctions remain mathematical obligations of the printed development. Acceptance is interpreter-only; no native-backend parity is claimed.