(Co-)Algebraic Foundations for Effect Handling and Iteration.
Sergey Goncharov, Lutz Schröder, Christoph Rauch · 2014
Abstract. Large portions of current programming theory and practice are based on algebraic notions of effect. One such concept is the re-cently developed paradigm of handling underspecified (‘free’) algebraic operations, as embodied in the Eff programming language. Here we pro-pose axiomatic foundations for computations with handlers and iteration. In order to accommodate iterative computations we involve a class of computational monads called Elgot monads, characterized by having parametrized uniform iteration operators in sense of Simpson and Plotkin. We interpret free operations in cofree extensions of Elgot monads; the interpretation of handling then relies on the iteration operator in the original Elgot monad. Our main result states that these cofree extensions are again Elgot monads, which therefore leads to novel semantic domains for uniform iterativity. We then elaborate the details of a categorical semantics of a simple call-by-value language w.r.t. an Elgot monad and discuss various use cases formalized in the derived framework. 1