On Linear Types and Regions
Abstract
We explore how two different mechanisms for reasoning about state,
linear typing and the type, region and effect discipline, complement
one another in the design of a strongly typed functional programming
language. The basis for our language is a simple lambda calculus
containing {\em first-class} regions, which are explicitly passed as
arguments to functions, returned as results and stored in user-defined
data structures. In order to ensure appropriate memory safety
properties, we draw upon the literature on linear type systems to help
control access to and deallocation of regions. In fact, we use
two different interpretations of linear types, one in which
multiple-use values are freely copied and discarded
and one in which multiple-use
values are explicitly reference-counted, and show that both interpretations
give rise to interesting invariants for manipulating regions. We also
explore new programming paradigms that arise by mixing first-class
regions and conventional linear data structures.
(postscript)