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 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 ]

  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.