Many useful programming constructions can be expressed as monads.
Examples include probabilistic computations,
time-varying expressions, parsers, and information flow tracking,
not to mention effectful features 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 typechecks. Our algorithm is based on Jones'
qualified types and enjoys three useful properties: (1) principal
types, i.e., the rewriting we perform is the most general; (2)
coherence, i.e., thanks to the monad and morphism laws, all
instances of the principal rewriting have the same semantics; (3)
decidability; i.e., the solver for generated constraints will always
terminate. Throughout the paper we present simple examples from the
domains listed above. Our most complete example, which illustrates
the expressive power of our system, proves that ML programs
rewritten by our algorithm to use the information flow monad are
equivalent to programs in FlowCaml, a domain-specific information
flow tracking language.

@techreport{swamy11monadTR, title = {Lightweight Monadic Programming in {ML}}, author = {Nikhil Swamy and Nataliya Guts and Daan Leijen and Michael Hicks}, number = {MSR-TR-2011-039}, institution = {Microsoft Research}, year = 2011, month = may, http = {http://research.microsoft.com/en-us/projects/coco/} }

*This file was generated by
bibtex2html 1.99.*