Algebraic and coalgebraic perspectives on interaction laws

Abstract

Monad algebras, turning computations over return values into values, are used to handle algebraic effects invoked by programs, whereas comonad coalgebras, turning initial states into environments (“cocomputations”) over states, describe production of coalgebraic coeffects that can respond to effects. (Monad-comonad) interaction laws by Katsumata et al. describe interaction protocols between a computation and an environment. We show that any triple of those devices 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 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 an environment 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 environments.