On regions and linear types (extended 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 functionalprogramming language. The basis for our language is a simple lambdacalculus containing first-class memory regions, which areexplicitly passed as arguments to functions, returned as resultsand stored in user-defined data structures. In order to ensureappropriate memory safety properties, we draw upon the literatureon linear type systems to help control access to and deallocationof regions. In fact, we use two different interpretations of lineartypes, one in which multiple-use values are freely copied anddiscarded and one in which multiple-use values are explicitlyreference-counted, and show that both interpretations give rise tointeresting invariants for manipulating regions. We also explorenew programming paradigms that arise by mixing first-class regionsand conventional linear data structures.