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 alla,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.