Write a Blog >>
APLAS 2020
Sun 29 November - Thu 3 December 2020

\emph{Monad algebras}, turning computations over return values into values, are used to resolve algebraic effects invoked by programs (effect handling), whereas \emph{comonad coalgebras}, turning initial states into cocomputations over states, are used to specify production of environments with coalgebraic coeffects (coeffect production). \emph{(Monad-comonad) interaction laws} by Katsumata et al. describe interaction protocols between a computation and a cocomputation. We show that any triple of those tools can be combined into a single algebra handling computations over state predicates. This method yields an isomorphism between the category of interaction laws, and the category of so-called \emph{merge functors} which merge algebras and coalgebras to form combined algebras. In a similar vein, we can combine interaction laws with coalgebras only, retrieving Uustalu’s stateful runners. If instead we combine interaction laws with algebras only, we get a novel concept of continuation-based runners that lift a cocomputation of value predicates to a single predicate on computations of values. We use these notions to study different running examples of interactions of computations and cocomputations.