Monads for Behaviour

The monads used to model effectful computations traditionally concentrate on the ‘destination’—the final results of the program. However, sometimes we are also interested in the ‘journey’—the intermediate course of a computation—especially when reasoning about non-terminating interactive systems. In this article we claim that a necessary property of a monad for it to be able to describe the behaviour of a program is complete iterativity. We show how an ordinary monad can be modified to disclose more about its internal computational behaviour, by applying an associated transformer to a completely iterative monad. To illustrate this, we introduce two new constructions: a coinductive cousin of Cenciarelli and Moggiʼs generalised resumption transformer, and States—a State-like monad that accumulates the intermediate states.