Scoped Effects as Parameterized Algebraic Theories

Sam Lindley; Cristina Matache; Sean Moss; Sam Staton; Nicolas Wu; Zhixuan Yang

doi:10.1007/978-3-031-57262-3_1

Scoped Effects as Parameterized Algebraic Theories

Sam Lindley, Cristina Matache^*, Sean Moss, Sam Staton, Nicolas Wu, Zhixuan Yang

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Downloads (Pure)

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.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I
Editors	Stephanie Weirich
Publisher	Springer
Pages	3-21
Number of pages	19
Edition	1
ISBN (Electronic)	9783031572623
ISBN (Print)	9783031572616
DOIs	https://doi.org/10.1007/978-3-031-57262-3_1
Publication status	Published - 5 Apr 2024
Event	ESOP 2024: 33rd European Symposium on Programming - Luxembourg City, Luxembourg Duration: 8 Apr 2024 → 11 Apr 2024 https://etaps.org/2024/conferences/esop/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	14576
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	ESOP 2024
Abbreviated title	ESOP2024
Country/Territory	Luxembourg
City	Luxembourg City
Period	8/04/24 → 11/04/24
Internet address	https://etaps.org/2024/conferences/esop/

Bibliographical note

Acknowledgments:
We are grateful to many colleagues for helpful discussions and to the anonymous reviewers for their helpful comments and suggestions. This work was supported by the UKRI Future Leaders Fellowship “Effect Handler Oriented Programming” (reference number MR/T043830/1), ERC Project BLAST, and AFOSR Award No. FA9550-21-1-003.

Keywords

algebraic effects
scoped effects
monads
category theory
algebraic theories

Access to Document

10.1007/978-3-031-57262-3_1Licence: Creative Commons: Attribution (CC BY)

LindleyS2024ScopedFinal published version, 526 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

Lindley, S., Matache, C., Moss, S., Staton, S., Wu, N., & Yang, Z. (2024). Scoped Effects as Parameterized Algebraic Theories. In S. Weirich (Ed.), Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I (1 ed., pp. 3-21). (Lecture Notes in Computer Science; Vol. 14576). Springer. https://doi.org/10.1007/978-3-031-57262-3_1

Lindley, Sam ; Matache, Cristina ; Moss, Sean et al. / Scoped Effects as Parameterized Algebraic Theories. Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I. editor / Stephanie Weirich. 1. ed. Springer, 2024. pp. 3-21 (Lecture Notes in Computer Science).

@inproceedings{f5afd0f3aff7475cbdfb26527c8aeca0,

title = "Scoped Effects as Parameterized Algebraic Theories",

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.",

keywords = "algebraic effects, scoped effects, monads, category theory, algebraic theories",

author = "Sam Lindley and Cristina Matache and Sean Moss and Sam Staton and Nicolas Wu and Zhixuan Yang",

note = "Acknowledgments: We are grateful to many colleagues for helpful discussions and to the anonymous reviewers for their helpful comments and suggestions. This work was supported by the UKRI Future Leaders Fellowship “Effect Handler Oriented Programming” (reference number MR/T043830/1), ERC Project BLAST, and AFOSR Award No. FA9550-21-1-003.; ESOP 2024 : 33rd European Symposium on Programming, ESOP2024 ; Conference date: 08-04-2024 Through 11-04-2024",

year = "2024",

month = apr,

day = "5",

doi = "10.1007/978-3-031-57262-3_1",

language = "English",

isbn = "9783031572616",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "3--21",

editor = "Stephanie Weirich",

booktitle = "Programming Languages and Systems",

edition = "1",

url = "https://etaps.org/2024/conferences/esop/",

}

Lindley, S, Matache, C, Moss, S, Staton, S, Wu, N & Yang, Z 2024, Scoped Effects as Parameterized Algebraic Theories. in S Weirich (ed.), Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I. 1 edn, Lecture Notes in Computer Science, vol. 14576, Springer, pp. 3-21, ESOP 2024, Luxembourg City, Luxembourg, 8/04/24. https://doi.org/10.1007/978-3-031-57262-3_1

Scoped Effects as Parameterized Algebraic Theories. / Lindley, Sam; Matache, Cristina; Moss, Sean et al.
Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I. ed. / Stephanie Weirich. 1. ed. Springer, 2024. p. 3-21 (Lecture Notes in Computer Science; Vol. 14576).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Scoped Effects as Parameterized Algebraic Theories

AU - Lindley, Sam

AU - Matache, Cristina

AU - Moss, Sean

AU - Staton, Sam

AU - Wu, Nicolas

AU - Yang, Zhixuan

N1 - Acknowledgments: We are grateful to many colleagues for helpful discussions and to the anonymous reviewers for their helpful comments and suggestions. This work was supported by the UKRI Future Leaders Fellowship “Effect Handler Oriented Programming” (reference number MR/T043830/1), ERC Project BLAST, and AFOSR Award No. FA9550-21-1-003.

PY - 2024/4/5

Y1 - 2024/4/5

N2 - 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.

AB - 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.

KW - algebraic effects

KW - scoped effects

KW - monads

KW - category theory

KW - algebraic theories

U2 - 10.1007/978-3-031-57262-3_1

DO - 10.1007/978-3-031-57262-3_1

M3 - Conference contribution

SN - 9783031572616

T3 - Lecture Notes in Computer Science

SP - 3

EP - 21

BT - Programming Languages and Systems

A2 - Weirich, Stephanie

PB - Springer

T2 - ESOP 2024

Y2 - 8 April 2024 through 11 April 2024

ER -

Lindley S, Matache C, Moss S, Staton S, Wu N, Yang Z. Scoped Effects as Parameterized Algebraic Theories. In Weirich S, editor, Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I. 1 ed. Springer. 2024. p. 3-21. (Lecture Notes in Computer Science). Epub 2024 Apr 4. doi: 10.1007/978-3-031-57262-3_1