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 *lambda*_{PM})
with syntactic support for programming with polymonads. Type
inference and elaboration in *lambda*_{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 *lambda*_{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 }