Rolling Your Own Mutable ADT
A Connection between Linear Types and Monads
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.