Rolling Your Own Mutable ADT -- A Connection between Linear Types and Monads

Authors:

Chih-Ping Chen and Paul Hudak

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.

Bibtex:

 @inproceedings{linearMADT
    ,author={Chih-Ping Chen and Paul Hudak}
    ,title={Rolling Your Own Mutable ADT---A Connection between Linear
            Types and Monads}
    ,booktitle ={Proceedings of 24th ACM Symposium on Principles of
                 Programming Languages}
    ,year =        "1997"
    ,publisher =   "ACM Press"
    ,address =     "New York"
    ,month =       "January"
    ,pages={54--66}
    } 

Links:

madt-popl.pdf