Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators
Kazuki Ikemori, Youyou Cong, Hidehiko Masuhara · 2023
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.