An Effect System for Algebraic Effects and Handlers

Andrej Bauer; Matija Pretnar

doi:10.2168/LMCS-10(4:9)2014

Andrej Bauer ; Matija Pretnar - An Effect System for Algebraic Effects and Handlers

lmcs:1153 - Logical Methods in Computer Science, December 10, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:9)2014

An Effect System for Algebraic Effects and HandlersArticle

Authors: Andrej Bauer ; Matija Pretnar

We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff, using Pitts's theory of minimal invariant relations, and prove it adequate. We use this fact to develop tools for finding useful contextual equivalences, including an induction principle. To demonstrate their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We have formalized the effect system, the operational semantics, and the safety theorem in Twelf.

https://doi.org/10.2168/LMCS-10(4:9)2014

Source: arXiv.org:1306.6316

Volume: Volume 10, Issue 4

Published on: December 10, 2014

Imported on: February 18, 2014

Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

27 Documents citing this article

Donnacha Oisín Kidney;Zhixuan Yang;Nicolas Wu, 2024, Algebraic Effects Meet Hoare Logic in Cubical Agda, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 1663-1695, 10.1145/3632898, https://doi.org/10.1145/3632898.

Wenhao Tang;Daniel Hillerström;Sam Lindley;J. Garrett Morris, 2024, Soundly Handling Linearity, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 1600-1628, 10.1145/3632896, https://doi.org/10.1145/3632896.

Paulo Emílio de Vilhena;François Pottier, Lecture notes in computer science, A Type System for Effect Handlers and Dynamic Labels, pp. 225-252, 2023, 10.1007/978-3-031-30044-8_9, https://doi.org/10.1007/978-3-031-30044-8_9.

Cas van der Rest;Casper Bach Poulsen, Lecture notes in computer science, Towards a Language for Defining Reusable Programming Language Components, pp. 18-38, 2022, 10.1007/978-3-031-21314-4_2.

Zhixuan Yang;Marco Paviotti;Nicolas Wu;Birthe van den Berg;Tom Schrijvers, Lecture notes in computer science, Structured Handling of Scoped Effects, pp. 462-491, 2022, 10.1007/978-3-030-99336-8_17, https://doi.org/10.1007/978-3-030-99336-8_17.

Danel Ahman;Matija Pretnar, 2021, Asynchronous effects, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-28, 10.1145/3434305, https://doi.org/10.1145/3434305.

Georgios Karachalias;Filip Koprivec;Matija Pretnar;Tom Schrijvers, 2021, Efficient compilation of algebraic effect handlers, Proceedings of the ACM on Programming Languages, 5, OOPSLA, pp. 1-28, 10.1145/3485479, https://doi.org/10.1145/3485479.

Nikita Zyuzin;Aleksandar Nanevski, 2021, Contextual modal types for algebraic effects and handlers, Proceedings of the ACM on Programming Languages, 5, ICFP, pp. 1-29, 10.1145/3473580, https://doi.org/10.1145/3473580.

Zhixuan Yang;Nicolas Wu, 2021, Reasoning about effect interaction by fusion, Proceedings of the ACM on Programming Languages, 5, ICFP, pp. 1-29, 10.1145/3473578, https://doi.org/10.1145/3473578.

Danel Ahman;Andrej Bauer, Lecture notes in computer science, Runners in Action, pp. 29-55, 2020, 10.1007/978-3-030-44914-8_2, https://doi.org/10.1007/978-3-030-44914-8_2.

LUKAS CONVENT;SAM LINDLEY;CONOR MCBRIDE;CRAIG MCLAUGHLIN, 2020, Doo bee doo bee doo, Journal of Functional Programming, 30, 10.1017/s0956796820000039, https://doi.org/10.1017/s0956796820000039.

Ningning Xie;Jonathan Immanuel Brachthäuser;Daniel Hillerström;Philipp Schuster;Daan Leijen, 2020, Effect handlers, evidently, Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-29, 10.1145/3408981, https://doi.org/10.1145/3408981.

ŽIGA LUKŠIČ;MATIJA PRETNAR, 2020, Local algebraic effect theories, arXiv (Cornell University), 30, 10.1017/s0956796819000212, https://arxiv.org/abs/2005.13654.

Dariusz Biernacki;Maciej Piróg;Piotr Polesiuk;Filip Sieczkowski, 2019, Binders by day, labels by night: effect instances via lexically scoped handlers, Proceedings of the ACM on Programming Languages, 4, POPL, pp. 1-29, 10.1145/3371116, https://doi.org/10.1145/3371116.

Dariusz Biernacki;Maciej Piróg;Piotr Polesiuk;Filip Sieczkowski, 2019, Abstracting algebraic effects, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-28, 10.1145/3290319, https://doi.org/10.1145/3290319.

Koen Pauwels;Tom Schrijvers;Shin-Cheng Mu, Lirias (KU Leuven), Handling Local State with Global State, pp. 18-44, 2019, 10.1007/978-3-030-33636-3_2, https://lirias.kuleuven.be/handle/123456789/646136.

YANNICK FORSTER;OHAD KAMMAR;SAM LINDLEY;MATIJA PRETNAR, 2019, On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control, Edinburgh Research Explorer (University of Edinburgh), 29, 10.1017/s0956796819000121, https://dl.acm.org/citation.cfm?doid=3136534.3110257.

Yizhou Zhang;Andrew C. Myers, 2019, Abstraction-safe effect handlers via tunneling, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-29, 10.1145/3290318, https://doi.org/10.1145/3290318.

Daan Leijen, 2017, Type directed compilation of row-typed algebraic effects, ACM SIGPLAN Notices, 52, 1, pp. 486-499, 10.1145/3093333.3009872.

Dariusz Biernacki;Maciej Piróg;Piotr Polesiuk;Filip Sieczkowski, 2017, Handle with care: relational interpretation of algebraic effects and handlers, Proceedings of the ACM on Programming Languages, 2, POPL, pp. 1-30, 10.1145/3158096, https://doi.org/10.1145/3158096.

OHAD KAMMAR;MATIJA PRETNAR, 2017, No value restriction is needed for algebraic effects and handlers, arXiv (Cornell University), 27, 10.1017/s0956796816000320, https://arxiv.org/abs/1605.06938.

Sam Lindley;Conor McBride;Craig McLaughlin, 2017, Do be do be do, ACM SIGPLAN Notices, 52, 1, pp. 500-514, 10.1145/3093333.3009897.

Yannick Forster;Ohad Kammar;Sam Lindley;Matija Pretnar, 2017, On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control, Proceedings of the ACM on Programming Languages, 1, ICFP, pp. 1-29, 10.1145/3110257, https://doi.org/10.1145/3110257.

Daan Leijen, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Type directed compilation of row-typed algebraic effects, 2016, Paris France, 10.1145/3009837.3009872.

Daniel Hillerström;Sam Lindley, Edinburgh Research Explorer (University of Edinburgh), Liberating effects with rows and handlers, 2016, Nara Japan, 10.1145/2976022.2976033, https://www.research.ed.ac.uk/en/publications/a55cafe9-5000-4b27-a887-baf7bf8ba5b1.

Sam Lindley;Conor McBride;Craig McLaughlin, Edinburgh Research Explorer (University of Edinburgh), Do be do be do, 2016, Paris France, 10.1145/3009837.3009897, http://hdl.handle.net/20.500.11820/bd2598b0-20ce-4272-821f-985974bdd4f6.

Matija Pretnar, 2015, An Introduction to Algebraic Effects and Handlers. Invited tutorial paper, Electronic Notes in Theoretical Computer Science, 319, pp. 19-35, 10.1016/j.entcs.2015.12.003, https://doi.org/10.1016/j.entcs.2015.12.003.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3198 times.

This article's PDF has been downloaded 872 times.