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* *tau* were expressions
of type *tau*. 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 ]

@MISC{hicks12polymonad, TITLE = {Polymonads}, AUTHOR = {Nataliya Guts and Michael Hicks and Nikhil Swamy and Daan Leijen and Gavin Bierman}, MONTH = JUL, YEAR = 2012, SUBMITTED = {yes} }