Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Complete Categorical Semantics for Effect Handlers

Satoshi Kura

TL;DR

This work addresses the gap in categorical semantics for algebraic effects and handlers by establishing soundness and completeness results for two variants of an effect-handler calculus. It introduces a flexible, indexed-monad semantic framework that subsumes free-model-monad models and CPS-based continuation models as valid interpretations, and extends to calculi with equational axioms for effect theories. The authors prove completeness via a term-model construction and connect the semantics to Eilenberg–Moore algebras, base types, and sum types, demonstrating practical modeling with examples like free monads and CPS semantics. The study paves the way toward fibrational logical-relations for effect handlers and broadens the understanding of semantic diversity beyond traditional free-monad models.

Abstract

Soundness and completeness with respect to equational theories for programming languages are fundamental properties in the study of categorical semantics. However, completeness results have not been established for programming languages with algebraic effects and handlers, which raises a question of whether the commonly used models in the literature, i.e., free model monads generated from algebraic theories, are the only valid semantic models for effect handlers. In this paper, we show that this is not the case. We identify the precise characterizations of categorical models of effect handlers that allow us to establish soundness and completeness results with respect to a certain equational theory for effect handling constructs. Notably, this allows us to capture not only free monad models but also the CPS semantics for effect handlers as models of the calculus.

On Complete Categorical Semantics for Effect Handlers

TL;DR

This work addresses the gap in categorical semantics for algebraic effects and handlers by establishing soundness and completeness results for two variants of an effect-handler calculus. It introduces a flexible, indexed-monad semantic framework that subsumes free-model-monad models and CPS-based continuation models as valid interpretations, and extends to calculi with equational axioms for effect theories. The authors prove completeness via a term-model construction and connect the semantics to Eilenberg–Moore algebras, base types, and sum types, demonstrating practical modeling with examples like free monads and CPS semantics. The study paves the way toward fibrational logical-relations for effect handlers and broadens the understanding of semantic diversity beyond traditional free-monad models.

Abstract

Soundness and completeness with respect to equational theories for programming languages are fundamental properties in the study of categorical semantics. However, completeness results have not been established for programming languages with algebraic effects and handlers, which raises a question of whether the commonly used models in the literature, i.e., free model monads generated from algebraic theories, are the only valid semantic models for effect handlers. In this paper, we show that this is not the case. We identify the precise characterizations of categorical models of effect handlers that allow us to establish soundness and completeness results with respect to a certain equational theory for effect handling constructs. Notably, this allows us to capture not only free monad models but also the CPS semantics for effect handlers as models of the calculus.
Paper Structure (48 sections, 47 theorems, 74 equations, 5 figures)

This paper contains 48 sections, 47 theorems, 74 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Strong monads and strong Kleisli triples
  4. Kleisli categories and Kleisli exponentials
  5. Models of the fine-grain call-by-value
  6. An Effect Handler Calculus
  7. Types and Terms
  8. Equational Theory
  9. Operational Semantics
  10. Typing Rules
  11. Equational Theory
  12. Basic Properties
  13. Denotational Semantics
  14. Models and Interpretations
  15. Semantics of signatures
  16. ...and 33 more sections

Key Result

proposition 1

If $\vdash M : C$ is a closed computation term, then either $M$ is a normal form, or there exists a computation term $N$ such that $M \leadsto N$ and $\vdash N : C$. Here, normal forms are computation terms of the form (a) $\mathtt{return}\ V$, (b) $\mathcal{C}[\mathtt{op}(V)]$ where $\mathcal{C}$ d

Figures (5)

  • Figure 1: Selected typing rules. See Appendix \ref{['sec:full-typing-rules']} for full typing rules.
  • Figure 2: The $\beta$ and $\eta$ laws for lambda abstraction and product types, and the monad laws for let-expressions.
  • Figure 3: Equations for effect handlers.
  • Figure 4: Commutative diagrams for \ref{['eq:handle-unit']}, \ref{['eq:handle-multiplication']}, and \ref{['eq:handle-operation']}.
  • Figure 5: Typing rules for $\lambda_{\mathrm{eff}}^{+, {=}}$ related to effect handlers. We implicitly assume that variables in $\Gamma$ and $\hat{\Delta}$ are disjoint.

Theorems & Definitions (82)

  • definition 1
  • definition 2: Kleisli exponentials
  • definition 3
  • proposition 1: type soundness
  • Remark 1
  • definition 4
  • lemma 1
  • proposition 2
  • definition 5
  • proposition 3
  • ...and 72 more