Algebraic effects and handlers for arrows

Abstract

We present an arrow calculus with operations and handlers and its operational and denotational semantics. The calculus is an extension of Lindley, Wadler and Yallop’s arrow calculus.

The denotational semantics is given using a strong (pro)monad \(\mathcal{A}\) in the bicategory of categories and profunctors. The construction of this strong monad \(\mathcal{A}\) is not trivial because of a size problem. To build denotational semantics, we investigate what \(\mathcal{A}\)-algebras are, and a handler is interpreted as an \(\mathcal{A}\)-homomorphisms between \(\mathcal{A}\)-algebras.

The syntax and operational semantics are derived from the observations on \(\mathcal{A}\)-algebras. We prove the soundness and adequacy theorem of the operational semantics for the denotational semantics.