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