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 this
paper, we present 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* *t* as if they were of type *t*, and our algorithm
inserts the necessary binds, units, and monad-to-monad morphisms so
that the program type checks. Our algorithm, based on Jones'
qualified types, produces principal types. But principal
types are sometimes
problematic: the program's semantics could depend on the choice of
instantiation when more than one instantiation is valid. In such
situations we are able to simplify the types to remove
any ambiguity but without adversely affecting typability; thus we can
accept strictly more programs. Moreover, we have proved that this
simplification is *efficient* (linear in the number of constraints)
and *coherent*: while our algorithm induces a particular rewriting,
all related rewritings will have the same semantics.
We have implemented our approach for a core functional
language and applied it successfully to simple examples from the
domains listed above, which are used as illustrations throughout the
paper.

@INPROCEEDINGS{swamy11monad, TITLE = {Lightweight Monadic Programming in {ML}}, AUTHOR = {Nikhil Swamy and Nataliya Guts and Daan Leijen and Michael Hicks}, BOOKTITLE = {Proceedings of the {ACM} International Conference on Functional Programming (ICFP)}, YEAR = 2011, MONTH = SEP, PAGES = {15--27}, HTTP = {http://research.microsoft.com/en-us/projects/coco/} }