Unguarded Recursion on Coinductive Resumptions

We study a model of side-effecting processes obtained by starting from amonad modelling base effects and adjoining free operations using a cofreecoalgebra construction; one thus arrives at what one may think of as types ofnon-wellfounded side-effecting trees, generalizing the infinite resumptionmonad. Correspondingly, the arising monad transformer has been termed thecoinductive generalized resumption transformer. Monads of this kind havereceived some attention in the recent literature; in particular, it has beenshown that they admit guarded iteration. Here, we show that they also admitunguarded iteration, i.e. form complete Elgot monads, provided that theunderlying base effect supports unguarded iteration. Moreover, we provide auniversal characterization of the coinductive resumption monad transformer interms of coproducts of complete Elgot monads.Comment: 47 pages, extended version of http://www.sciencedirect.com/science/article/pii/S157106611500079