ch:effect-rows: ch:effect-rows

Problem and result. Implement the duplicate-preserving row fragment, its guarded unifier, and the one-layer handler machine. The accepted program returns the eight named results in the exercise: exchange without contraction, one-occurrence cancellation, open-row exposure, the guarded shared-tail rejection, the three transaction equations, forwarding, rethrow, and the reader output tail.

Representation. Represent a row by an ordered prefix and an optional tail variable, retaining duplicate labels. Represent substitutions explicitly and handler execution by one-layer frames. A finite set would make exchange cheap, but it would erase the distinction between cancelling one occurrence and contracting two.

First complete version. Begin with row comparison modulo adjacent exchange and cancellation of the first matching label. Return the residual row rather than a Boolean: that residual is the input to every later recursive call and exposes the invariant that each successful cancellation consumes exactly one constructor.

Remaining cases. Add guarded exposure of a tail variable and replay substitutions after every extension. Then add the transaction’s three W equations and the one-layer handler transition. Keep forwarding explicit so the outer fallback sees the remaining raise and the reader resumption is built at the handler output row.

A failing version. In prefix comparison, recurse on the original right row after a match instead of its cancellation residual. The duplicate-label case then reuses an occurrence. The mutant still typechecks and has an empty audit, but the frozen row oracle rejects it.

Acceptance test. Run check, test, run, and audit as recorded in appendix E. Require the exact eight-case output, a successful inline test, mutation rejection, and an empty audit.

Mathematical boundary. The run checks finite instances of cancellation, exposure, inference, and handler dispatch. It proves neither row-equivalence completeness nor the soundness, principality, preservation, or progress theorems.