Rolling Your Own Mutable ADT

A Connection between Linear Types and Monads

Chih-Ping Chen

In recent years, monads have become the most widely used approach to state manipulation in the pure functional programming society. Nevertheless, little work has been done in formalizing the connection between monads and state. Furthermore, although laws for reasoning about several specific monads exist, there is no general way to derive these laws. In this talk, I am going to outline a methodology that allows one to begin with a conventional axiomatization of state, rigorously encapsulate it within a monad, and reason about it abstractly in a monadic fashion. This is only possible if the axiomatization satisfies a certain linearity condition, established using linear types. This same condition allows us to prove that the state may be updated destructively. Meanwhile, the combination of monads and linear types in our framework reveals a connection between them, which is formalized by a CPS-like transformation. This is a joint work with Professor Paul Hudak.