| 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: (1) a type-and-effect system (a la the Tofte-Talpin region calculus); (2) a novel monadic type system; (3) 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 sub-structural 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. |
