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
|
| _version_ | 1797113113473974272 |
|---|---|
| author | Lindley, S Matache, C Moss, S Staton, S Wu, N Yang, Z |
| author_facet | Lindley, S Matache, C Moss, S Staton, S Wu, N Yang, Z |
| author_sort | Lindley, S |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T08:21:18Z |
| format | Conference item |
| id | oxford-uuid:32b1d594-e062-4f20-9ca9-1a2102e7480d |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-04-09T03:58:53Z |
| publishDate | 2024 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:32b1d594-e062-4f20-9ca9-1a2102e7480d2024-04-08T10:42:58ZScoped effects as parameterized algebraic theoriesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:32b1d594-e062-4f20-9ca9-1a2102e7480dEnglishSymplectic ElementsSpringer2024Lindley, SMatache, CMoss, SStaton, SWu, NYang, ZNotions 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. |
| spellingShingle | Lindley, S Matache, C Moss, S Staton, S Wu, N Yang, Z Scoped effects as parameterized algebraic theories |
| title | Scoped effects as parameterized algebraic theories |
| title_full | Scoped effects as parameterized algebraic theories |
| title_fullStr | Scoped effects as parameterized algebraic theories |
| title_full_unstemmed | Scoped effects as parameterized algebraic theories |
| title_short | Scoped effects as parameterized algebraic theories |
| title_sort | scoped effects as parameterized algebraic theories |
| work_keys_str_mv | AT lindleys scopedeffectsasparameterizedalgebraictheories AT matachec scopedeffectsasparameterizedalgebraictheories AT mosss scopedeffectsasparameterizedalgebraictheories AT statons scopedeffectsasparameterizedalgebraictheories AT wun scopedeffectsasparameterizedalgebraictheories AT yangz scopedeffectsasparameterizedalgebraictheories |