From their semantic origins to their use in structuring effectful computations, monads are now also used as a programming pattern to structure code in a number of important scenarios, including functional reactivity, information flow tracking and probabilistic computation. However, whilst these examples are inspired by monads they are not strictly speaking monadic but rather something more general. The first contribution of this paper is the definition of a new structure, the polymonad, which subsumes monads and encompasses the monad-like programming patterns that we have observed. A concern is that given such a general setting, a program would quickly become polluted with polymonadic coercions, making it hard to read and maintain. The second contribution of this paper is to build on previous work to define a polymorphic type inference algorithm that supports programming with polymonads using a direct style, e.g., as if computations of type M τ were expressions of type τ. During type inference the program is rewritten to insert the necessary polymonadic coercions, a process that we prove is coherent---all sound rewritings produce programs with the same semantics. The resulting programming style is powerful and lightweight.

[ .pdf ]

@techreport{hicks12polymonadTR,
  title = {Polymonads},
  author = {Nataliya Guts and Michael Hicks and Nikhil Swamy and Daan Leijen and Gavin Bierman},
  note = {Extended version of POPL'13 submission},
  institution = {University of Maryland Department of Computer Science},
  number = {XXX},
  month = jul,
  year = 2012
}

This file was generated by bibtex2html 1.99.