Abstract:
Algebraic effect handlers and delimited control operators are language facilities for expressing computational effects. Their labeled variations can express multiple kinds of exceptions, multiple states, and so on. We prove that labeled effect handlers and labeled control operators have equal expressive power. To show this, we develop a type-sound calculus for each facility and define macro translations between the typed calculi. The established equivalence can be used to understand and implement one facility in terms of the other.
Reference:
Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators. (Kazuki Ikemori, Youyou Cong and Hidehiko Masuhara), In Proceedings of the 25th International Symposium onPrinciples and Practice of Declarative Programming (PPDP 2023), 2023.
Bibtex Entry:
@inproceedings{ikemori2023ppdp,
author = {Kazuki Ikemori and Youyou Cong and Hidehiko Masuhara},
title = {Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators.},
booktitle = {Proceedings of the 25th International Symposium onPrinciples and Practice of Declarative Programming (PPDP 2023)},
year = 2023,
month = oct,
location = {Cascais, Portugal},
pages = {1--13},
doi = {10.1145/3610612.3610616},
url = {https://ppdp2023.webs.upv.es/},
abstract = {Algebraic effect handlers and delimited control operators are language facilities for expressing computational effects. Their labeled variations can express multiple kinds of exceptions, multiple states, and so on. We prove that labeled effect handlers and labeled control operators have equal expressive power. To show this, we develop a type-sound calculus for each facility and define macro translations between the typed calculi. The established equivalence can be used to understand and implement one facility in terms of the other.},
pdf = {ppdp2023.pdf}
}