log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
Polymonads: reasoning and inference
Friday, May 18, 2012, 3:00-4:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

Joint work with Mike Hicks, Daan Leijen, and Nikhil Swamy

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[SGLH11], 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.

[SGLH11] N. Swamy, N. Guts, D. Leijen, M. Hicks. Lightweight Monadic Programming in ML. In ICFP, 2011.
http://www.cs.umd.edu/~mwh/papers/swamy11monad.html

This talk is organized by Jinseong Jeon