Scoped Effects as Parameterized Algebraic Theories
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914801355063296 |
|---|---|
| author | Matache, Cristina Lindley, Sam Moss, Sean Staton, Sam Wu, Nicolas Yang, Zhixuan |
| author_facet | Matache, Cristina Lindley, Sam Moss, Sean Staton, Sam Wu, Nicolas Yang, Zhixuan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_03103 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Scoped Effects as Parameterized Algebraic Theories Matache, Cristina Lindley, Sam Moss, Sean Staton, Sam Wu, Nicolas Yang, Zhixuan Programming Languages Logic in Computer Science Category Theory 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. |
| title | Scoped Effects as Parameterized Algebraic Theories |
| topic | Programming Languages Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2402.03103 |