Polymonadic Programming. Michael Hicks, Gavin Bierman, Nataliya Guts, Daan Leijen, and Nikhil Swamy. In Proceedings of the Fifth Workshop on Mathematically Structured Functional Programming (MSFP), April 2014.

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 lambdaPM) with syntactic support for programming with polymonads. Type inference and elaboration in lambdaPM 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 lambdaPM 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 has been generated by bibtex2html 1.69