Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In our previous work, we presented a type-based rewriting algorithm to make programming with arbitrary monads as easy as using ML’s built-in support for state and I/O. Developers write programs using monadic values of type m τ as if they were of type τ, and our algorithm inserts the necessary binds, units, and monad-to-monad morphisms so that the program typechecks.

A number of other programming idioms resemble monads but deviate from the standard monad binding mechanism. Examples include parameterized monads, monads for effects, information flow state tracking. Our present work aims to provide support for formal reasoning and lightweight programming for such constructs. We present a new expressive paradigm, polymonads, including the equivalent of monad and morphism laws. Polymonads subsume conventional monads and all other examples mentioned above. On the practical side, we provide an extension of our type inference rewriting algorithm to support lightweight programming with polymonads.

Joint work with Nataliya Guts, Daan Leijen, and Nikhil Swamy