Deriving Effect Handler Semantics
C. Lemaire (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Casper Bach Bach Poulsen – Mentor (TU Delft - Programming Languages)
J.S. Reinders – Graduation committee member (TU Delft - Programming Languages)
A.E. Zaidman – Mentor (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
For algebraic effects and handlers, we know both small-step and big-step operational semantics and we are familiar with denotational semantics. But, what is missing is a structured showing that one is equivalent to the other. On top of this, most efficient implementations of algebraic effects and handlers closely resemble their denotational semantics by encoding operations in what is called the free monad. In this work, we often refer to these implementations as freer monad-based embeddings of effects and handlers. These embeddings enable programmers to write effectful programs as though they are monadic programs. However, the derivation of such an embedding from an operational semantics remains thusfar unexplored. This work fills in the gap between a denotational interpreter derived by inverse closure conversion and the freer monad-based embedding of effects and handlers. We thus define and show program transformations that extend the steps needed to transform a denotational interpreter to a small-step interpreter and vice versa.