Unifying graded and parameterised monads

Dominic Orchard
(University of Kent)
Philip Wadler
(University of Edinburgh)
Harley Eades III
(Augusta University)

Monads are a useful tool for structuring effectful features of computation such as state, non-determinism, and continuations. In the last decade, several generalisations of monads have been suggested which provide a more fine-grained model of effects by replacing the single type constructor of a monad with an indexed family of constructors. Most notably, graded monads (indexed by a monoid) model effect systems and parameterised monads (indexed by pairs of pre- and post-conditions) model program logics. This paper studies the relationship between these two generalisations of monads via a third generalisation. This third generalisation, which we call category-graded monads, arises by generalising a view of monads as a particular special case of lax functors. A category-graded monad provides a family of functors T f indexed by morphisms f of some other category. This allows certain compositions of effects to be ruled out (in the style of a program logic) as well as an abstract description of effects (in the style of an effect system). Using this as a basis, we show how graded and parameterised monads can be unified, studying their similarities and differences along the way.

In Max S. New and Sam Lindley: Proceedings Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020), Dublin, Ireland, 25th April 2020, Electronic Proceedings in Theoretical Computer Science 317, pp. 18–38.
Published: 1st May 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.317.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org