Monads are a popular tool for the working functional programmer to
structure effectful computations. This paper presents
*polymonads*, a generalization of monads. Polymonads give the
familiar monadic bind the more general type
for all*a*,*b*. *L* *a* ->(*a* ->*M* *b*) ->*N* *b*, to
compose computations with three different kinds of effects, rather
than just one. Polymonads subsume monads and parameterized monads,
and can express other constructions, including precise
type-and-effect systems and information flow tracking; more
generally, polymonads correspond to Tate's *productoid*
semantic model. We show how to equip a core language (called λ_{PM})
with syntactic support for programming with polymonads. Type
inference and elaboration in λ_{PM} allows programmers to write
polymonadic code directly in an ML-like syntax---our algorithms
compute principal types and produce elaborated programs wherein
the binds appear explicitly. Furthermore, we prove that the
elaboration is *coherent*: no matter which (type-correct) binds
are chosen, the elaborated program's semantics will be the
same. Pleasingly, the inferred types are easy to read: the polymonad
laws justify (sometimes dramatic) simplifications, but with no
effect on a type's generality.

A prototype implementation of λ_{PM} is available.

[ .pdf ]

@inproceedings{hicks14polymonad, title = {Polymonadic Programming}, author = {Michael Hicks and Gavin Bierman and Nataliya Guts and Daan Leijen and Nikhil Swamy}, booktitle = {Proceedings of the Fifth Workshop on Mathematically Structured Functional Programming (MSFP)}, month = apr, year = 2014 }

*This file was generated by
bibtex2html 1.99.*