Christoph Lüth
Abstract
Monads are a useful abstraction of computation, as they model diverse computational effects such as stateful computations, exceptions and I/O in a uniform manner. Their potential to provide both a modular semantics and a modular programming style was soon recognised. However, in general, monads proved difficult to compose and so research focused on special mechanisms for their composition such as distributive monads and monad transformers.We present a new approach to this problem which is general in that nearly all monads compose, mathematically elegant in using the standard categorical tools underpinning monads and computationally expressive in supporting a canonical recursion operator. In a nutshell, we propose that two monads should be composed by taking their coproduct. Although abstractly this is a simple idea, the actual construction of the coproduct of two monads is non-trivial. We outline this construction, show how to implement the coproduct within Haskell and demonstrate its usage with a few examples. We also discuss its relationship with other ways of combining monads, in particular distributive laws for monads and monad transformers.
- J. Adamek and J. Rosický. Locally Presentable and Accessible Categories. LMS Lecture Notes 183. Cambridge University Press, 1994.Google Scholar
- M. Barr and C. Wells. Toposes, Triples and Theories. Grundlehren der mathematischen Wissenschaften 278. Springer Verlag, 1985.Google Scholar
- R. Bird and O. de Moor. Algebra of Programming. Prentice-Hall, 1997. Google ScholarDigital Library
- M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. LICS'99, pages 193--202. IEEE Computer Society Press, 1999. Google ScholarDigital Library
- Martin Hyland, Gordon Plotkin, and John Power. Combining computational effects: Commutativity and sum. In TCS 2002, 2nd IFIP International Conference on Computer Science, Montreal, 2002. Google ScholarDigital Library
- M. Jones and L. Duponcheel. Composing monads. Technical Report YALEU/DCS/RR-1004, Yale University, Dept. Comp. Sci, Dec 1993.Google Scholar
- G. M. Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves and so on. Bulletins of the Australian Mathematical Society, 22:1--83, 1980.Google ScholarCross Ref
- G. M. Kelly. Basic Concepts of Enriched Category Theory, LMS Lecture Notes~64. Cambridge University Press, 1982.Google Scholar
- G. M. Kelly and A. J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary monads. Journal for Pure and Applied Algebra, 89:163--179, 1993.Google ScholarCross Ref
- David King and Philip Wadler. Combining monads. In J. Launchbury and P.M. Samson, editors, Glasgow Workshop on Functional Programming, Workshops in Computing Series, Ayr, July 1992. Springer Verlag. Google ScholarDigital Library
- S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages. ACM Press, Jan 1995. Google ScholarDigital Library
- C. Lüth. Categorical Term Rewriting: Monads and Modularity. PhD thesis, University of Edinburgh, 1998.Google Scholar
- Monads and modular term rewriting. In Category Theory in Computer Science CTCS'97, LNCS 1290, pages 69--86. Springer Verlag, September 1997. Google ScholarDigital Library
- C. Lüth and N. Ghani. Monads and modularity. In Frontiers of Combining Systems FroCoS'02, LNAI 2309, pages 18--32. Springer Verlag, 2002. Google ScholarDigital Library
- S. Mac Lane. Categories for the Working Mathematician, Graduate Texts in Mathematics 5. Springer Verlag, 1971.Google Scholar
- Ernest G. Manes. Algebraic Theories, Graduate Texts in Mathematics 26. Springer Verlag, 1976.Google Scholar
- E. Moggi. Computational lambda-calculus and monads. In Fourth Annual Symposium on Logic in Computer Science. IEEE, Computer Society Press, June 1989. Google ScholarDigital Library
- E. Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, LFCS, 1990.Google Scholar
- Gordon Plotkin and John Power. Notions of computation determine monads. In M. Nielsen and U. Engeberg, editors, Proc. FOSSACS 2002, LNCS 2303, pages 342--356, 2002. Google ScholarDigital Library
- John Power. Enriched Lawvere theories. Theories and Applications of Categories 6:83--93, 2000.Google Scholar
- E. Robinson. Variations on algebra: monadicity and generalisations of equational theories. Technical Report 6/94, Sussex Computer Science, 1994.Google Scholar
- D. E. Rydeheard and J. G. Stell. Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms. In Category Theory and Computer Science, LNCS 283, pages 114--139. Springer Verlag, 1987. Google ScholarDigital Library
- M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):763--783, 1982.Google ScholarCross Ref
Index Terms
- Composing monads using coproducts
Recommendations
Composing monads using coproducts
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programmingMonads are a useful abstraction of computation, as they model diverse computational effects such as stateful computations, exceptions and I/O in a uniform manner. Their potential to provide both a modular semantics and a modular programming style was ...
Coproducts of Monads on Set
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer ScienceCoproducts of monads on $\Set$ have arisen in both the study of computational effects and universal algebra. We describe coproducts of consistent monads on $\Set$ by an initial algebra formula, and prove also the converse: if the coproduct exists, so do ...
Composing Partially Ordered Monads
RelMiCS '09/AKA '09: Proceedings of the 11th International Conference on Relational Methods in Computer Science and 6th International Conference on Applications of Kleene Algebra: Relations and Kleene Algebra in Computer ScienceComposition of the many-valued powerset partially ordered monad with the term monad provides extensions to non-classical relations and also new examples for Kleene algebras.
Comments