Monads for behaviour

Abstract

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.