Rolling Your Own MADT - A Connection Between Linear Types and Monads

Abstract

A methodology is described whereby a linear ADT may be rigorously encapsulated within a state monad. A CPS-like translation from the original ADT axioms into monadic ones is also described and proven correct, so that reasoning can be accomplished at the monadic level without exposing the state. The ADT axioms are suitably constrained by a linear type system to make this translation possible. This constraint also allows the state to be "updated in place," a notion made precise via a graph-rewrite operational semantics. 1 Introduction In recent years, numerous proposals for I/O, destructive updates to data structures, mutable variables, nondeterminism, and concurrency have been put forth, all using monads to structure programs in such a way that details of the computation are effectively hidden and encapsulated [18, 20]. One of the most important uses of monads is in dealing with state, resulting in a style of programming referred to appropriately by Peyton Jones and Wadler as imperativ...