TY - CONF
T1 - Lightweight monadic programming in ML
T2 - Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
Y1 - 2011
A1 - Swamy,Nikhil
A1 - Guts,Nataliya
A1 - Leijen,Daan
A1 - Hicks, Michael W.
KW - coercion
KW - coherence
KW - monad
KW - rewriting
KW - type
AB - 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 τ as if they were of type τ, 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.
JA - Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
T3 - ICFP '11
PB - ACM
CY - New York, NY, USA
SN - 978-1-4503-0865-6
UR - http://doi.acm.org/10.1145/2034773.2034778
M3 - 10.1145/2034773.2034778
ER -