Effect rows, inference, and handlers

The calculus of chapter 25 is fine-grain call by value with separate values and computations, base types, effect-annotated arrows, atomic operation requests, pure let-generalization, and deep handlers. Effects are finite label multisets whose duplicate occurrences are retained; there is at most one open row-variable tail. The fixed finite operation signature assigns every label closed, well-kinded parameter and result types. The fixed constant signature assigns each constant a closed, well-kinded value scheme. Adjacent exchange is the only row equation: contraction, unique-label lacks constraints, subeffect inequalities, type classes, answer-type indices, recursion, and dependent types are absent.

The complete rules are V-Var, V-Const, V-Lam, C-Return, C-App, C-To, C-Op, C-Let, C-RowConv, and C-Handle. A handler removes exactly one occurrence of every handled label and gives each deep resumption the handler output row. Primitive H-Op and H-Forward use the handler-free request context $R$; forwarding crosses one syntactic handler layer. Nearest-handler decomposition is lemma 25.6; request-context replacement, preservation, progress up to a terminal request, and the empty-effect no-unhandled-operation consequence are lemma 25.7, theorem 25.9, theorem 25.10.

Cancellation is lemma 25.2. Exposure has both its equational and principal-factorization clauses in lemma 25.12. The unifier includes reflexive, variable, symmetric, equal-base, empty, arrow, and extension successes. Its complete same-kind failures are distinct bases, base–arrow in both orientations, and empty–extension in both orientations; type–row equations are rejected as ill kinded before unification. It also has occurs-check and shared-tail guard failures. Its visible-row and outer work-list termination measures are in lemma 25.13; soundness, completeness, and most-general factorization are theorem 25.14. These results are for finite duplicate-label rows, not for unique rows with implicit lacks constraints.

${\mathsf{W}}_v$ and ${\mathsf{W}}_c$ infer values and type-and-effect pairs. Return reports a fresh open row; sequencing unifies the two premise rows; pure let unifies the bound effect with the empty row before value generalization. The handler accumulator processes body, return clause, operation clauses in source order, and the final input-row equation, applying every accumulated substitution to the remaining environment. Computation generalization is lemma 25.16; inference soundness and principal factorization are theorem 25.17, theorem 25.18. The transaction trace displays all three row equations and their composite substitution.

Kind-preserving type-and-row substitution preserves typing and row equivalence; scheme enlargement preserves every old variable instance. Ordinary value substitution is simultaneous for values and computations and covers lambda, operation, let, handler-parameter, and deep-resumption binders. Its generalized form allows each use of a pure-let variable to choose a different fresh type-and-row instance. The C-RowConv case reapplies the substituted equivalence. Preservation uses ordinary substitution for beta, sequencing, handled return, parameter, and resumption binders, and generalized substitution for the pure-let root.

The running transaction has principal computation scheme $\mathrm{\forall }\mu .(\mathsf{Int}!⟨\mathsf{get},\mathsf{put},\mathsf{raise}\mid \mu ⟩)$ in the let-polymorphic callback context, and the displayed monomorphic wrapper has one common latent row. Fallback, rethrow, logging rethrow, reader, twice resumption, and state-passing handlers are each typed by the same C-Handle rule. The rethrower requires two $\mathsf{raise}$ occurrences, consumes one, and leaves one for the outer fallback.

Theorem 25.19 is a typing theorem only. Its source fragment is monomorphic and C-Let-free, and every row in the derivation is closed. It maps a row to its finite support and terms to the annotated CBPV calculus of chapter 22; in particular, $\lfloor \mathsf{handle}e\mathsf{with}H\rfloor =\mathsf{handle}\lfloor e\rfloor \mathsf{with}\lfloor H\rfloor$, with return and operation clauses translated under the target’s thunked resumption assumption. The proof derives the complete target handler judgment and its set-difference premise. No operational simulation is claimed: the target uses explicit operation continuations, force/thunk administration, and sequencing equations for which this chapter defines no simulation closure. Duplicate rethrow remains typable after support erasure, but its consumed occurrence is no longer represented.

Leijen’s Extensible Records with Scoped Labels supplies the scoped-label row design in Section 3 (archived PDF pp. 2–3) and the exposure unifier and shared-tail guard in Section 7.1, Figures 2–3 (archived PDF pp. 6–7) [Lei05]. Koka: Programming with Row-polymorphic Effect Types gives duplicate effects in Sections 2.3–2.4 (printed pp. 103–105; archived PDF pp. 4–6) and inference in Appendix A (printed pp. 124–126; archived PDF pp. 25–27), especially Figures 8–9 (printed pp. 125–126; archived PDF pp. 26–27) [Lei14]. Those papers do not prove the local deep-handler safety theorem or the restricted target typing translation into chapter 22.

The pinned Kappa companion in subsubappendix E.3.6 represents finite rows, substitutions, exposure/unification, W row equations, and one-layer handler frames as object-language data. Its eight passing cases and three failing semantic mutations corroborate the examples only. They do not mechanize or prove any row, inference, safety, translation, or source theorem.

The source, intermediates, and target are separately fixed: $$F_{\epsilon }\to F_p\to F_{pw}\to F_{pb}\to F.$$ Evidence has type $q=(m,h,w)$, and the vector laws make $w.\ell$ select the newest evidence for $\ell$. An internal-safe $F_{pw}$ term is reachable from a closed, well-typed source-form term containing no prompt, yield, or marker. The imported endpoints are preservation (Theorem 2), progress (Theorem 3), and marker uniqueness (Theorem 4), all in §3.1.4, pp. 18–19, and Theorem 7 (§4.4, p. 24; PDF p. 25) of [XL21]. The end-to-end statement requires $$\cdot ⊢e:\mathsf{Int}\mid ⟨⟩⇝e^{\prime }$$ and concludes preservation of integer termination and divergence after applying $e^{\prime }$ to $⟨⟩⟩$. It is not a theorem about open programs, row inference, arbitrary prompt terms, or generated C.

The selected ${\lambda }_{\complement }$ card fixes a finite closed effect universe, Boolean effect formulas modulo ${\equiv }_{\mathsf{B}}$, no subeffecting, and the explicit term $e\mathsf{without}F$. The imported endpoint is Theorem 3.14 (§3.4, p. 16) of [LMSB23]: $${⊢}_m⟨\mathsf{do}F(v)\mid k⟩\mathsf{ok}⟹F\notin \mathsf{forb}(k).$$ Progress and preservation are Theorems 3.10–3.11. These results belong to Boolean unification and principal types modulo Boolean equivalence. They do not strengthen the duplicate-row MGU or inference theorem.