Modular Monadic Reasoning, a (Co-)Routine [pdf] [bib]
Steven Keuchel and Tom Schrijvers.
Published in Pre-Proceedings of the 24th International Symposium on Implementation and Application of Functional Languages, 2012
Abstract
Higher-order functions that are polymorphic in a monad make highly flexible modular components. Unfortunately, the combination of an unknown function parameter and a polymorphic monad are detrimental to reasoning. This paper shows how to eliminate both the function parameter and the polymorphism. The resulting characterization is amenable to reasoning.
The approach is based on a judicious combination of the coroutine monad transformer and monad morphisms.