The Because-Calculus: Separating Production, Existence, and Interpretation in Computation
2026-07-20 • Programming Languages
Programming LanguagesLogic in Computer Science
AI summaryⓘ
The authors study two related programming frameworks for handling effects called handler calculus and because-calculus. They show that handler calculus mixes two kinds of effects (ones that can pause and resume, and those that can't) in ways that don't break the system but allow useless code. Because-calculus separates these two clearly, preventing such useless code before running the program. They prove a key theorem showing that combining these distinctions into one can lose important information, and they use category theory to explain these relationships. Finally, they verify important properties ensuring programs behave well in these systems.
handler calculusbecause-calculusresumable effectsnon-resumable effectstype safetyprogresssubject reductioncategory theoryadjoint tripleeffect rows
Authors
Oscar Perez Mora
Abstract
Handler calculus conflates resumable and non-resumable effect operations through a single do construct, distinguished only by result type annotation. This conflation does not compromise type safety -- progress and preservation hold -- but it permits resumption bindings for non-resumable operations, creating vacuous bindings that the because-calculus eliminates at compile-time. The because-calculus structurally separates registration (non-resumable, void-returning) from attestation (resumable, non-void-returning) using dual effect rows and level-indexed typing, rejecting such clauses at compile-time via the Resumption Subconstraint. We prove the Conflation Theorem: collapsing the adjoint triple of existential, substitution, and universal functors into a single effect operation is non-faithful -- the erasure from the because-calculus to handler calculus maps rejected clauses to accepted ones. Four movements correspond to four natural transformations; categorical semantics maps each judgment to a category-theoretic construct. We establish progress, subject reduction, and tower progress for the full calculus.