Monadic and Substructural Type Systems for Region-Based Memory Management

  • fluet-thesis.double.pdf fluet-thesis.single.pdf (PhD thesis; 20060727-Defense.ppt)

    Region-based memory management is a scheme for managing dynamically allocated data. A defining characteristic of region-based memory management is the bulk deallocation of data, which avoids both the tedium of malloc/free and the overheads of a garbage collector. Type systems for region-based memory management enhance the utility of this scheme by statically determining when a program is guaranteed to not perform any erroneous region operations.

    We describe three type systems for region-based memory management:

    • a type-and-effect system (a la the Tofte-Talpin region calculus);
    • a novel monadic type system;
    • a novel substructural type system.
    We demonstrate how to successively encode the type-and-effect system into the monadic type system and the monadic type system into the substructural type system. These type systems and encodings support the argument that the type-and-effect systems that have traditionally been used to ensure the safety of region-based memory management are neither the simplest nor the most expressive type systems for this purpose.

    The monadic type system generalizes the state monad of Launchbury and Peyton Jones and demonstrates that the well-understood parametric polymorphism of System F provides sufficient encapsulation to ensure the safety of region-based memory management. The essence of the first encoding is to translate effects to an indexed monad, trading the subtleties of a type-and-effect system for the simplicity of a monadic type system.

    However, both the type-and-effect system and the monadic type system require that regions have nested lifetimes, following the lexical scope of the program, restricting when data may be effectively reclaimed. Hence, we introduce a substructural type system that eliminates the nested-lifetimes requirement. The key idea is to introduce first-class capabilities that mediate access to a region and to provide separate primitives for creating and destroying regions. The essence of the second encoding is to ``break open'' the monad to reveal its store-passing implementation.

    Finally, we show that the substructural type system is expressive enough to faithfully encode other advanced memory-management features.

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.