Scoped effects as parameterized algebraic theories
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....
| Main Authors: | , , , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2024
|
| Summary: | 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. |
|---|