Category-Graded Algebraic Theories and Effect Handlers

TL;DR

This paper introduces CatEff, an effect system based on category-graded algebraic theories, enabling fine-grained effect management with handlers that respect the structure of effects, demonstrated through typed data protocols.

Contribution

It develops a novel category-graded algebraic theory framework for effect systems, providing semantics, soundness, and practical examples of effect handling.

Findings

CatEff supports category-graded effects with morphism-based grading.

Soundness and adequacy of the semantics are established.

An example protocol demonstrates the system's expressiveness.

Abstract

We provide an effect system CatEff based on a category-graded extension of algebraic theories that correspond to category-graded monads. CatEff has category-graded operations and handlers. Effects in CatEff are graded by morphisms of the grading category. Grading morphisms represent fine structures of effects such as dependencies or sorts of states. Handlers in CatEff are regarded as an implementation of category-graded effects. We define the notion of category-graded algebraic theory to give semantics of CatEff and prove soundness and adequacy. We also give an example using category-graded effects to express protocols for sending receiving typed data.