Scoped Effects as Parameterized Algebraic Theories
Cristina Matache, Sam Lindley, Sean Moss, Sam Staton, Nicolas Wu, Zhixuan Yang
TL;DR
This work addresses how to model and reason about scoped computational effects by reframing them as parameterized algebraic theories with non-commutative linear parameters. The authors translate scoped operations into a parameterized theory framework, yielding a sound and complete equational system and canonical Set^{\\mathbb{N}}-based models, and they demonstrate with concrete free-models for nondeterminism with once, exceptions, local state, and cut. Key contributions include a unified equational theory for scoped effects, a detailed account of models as free parameterized theories, and a mechanism to derive parameterized theories from arbitrary scoped operations, with implications for effect handlers and modular semantics. The approach strengthens the algebraic understanding of effects with resources, enabling principled reasoning about scope management and resource lifetimes in languages that support advanced effectful features.
Abstract
Notions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes or dynamically allocated resources. Such mechanisms can be supported via extensions to algebraic effects including scoped effects and parameterized algebraic theories. We present a fresh perspective on scoped effects by translation into a variation of parameterized algebraic theories. The translation enables a new approach to equational reasoning for scoped effects and gives rise to an alternative characterization of monads in terms of generators and equations involving both scoped and algebraic operations. We demonstrate the power of our fresh perspective by way of equational characterizations of several known models of scoped effects.