On regions and linear types

We explore how two different mechanisms for reasoning about state, linear t yping 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 first-class memory regions, which are explicitly passed as arguments to functions, returned as results and stored in user-defined data structures. In order to ensure app ropriate memory safety properties, we draw upon the literature on linear ty pe 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 v alues are explicitly reference-counted, and show that both interpretations give rise to interesting invariants for manipulating regions. We also explo re new programming paradigms that arise by mixing first-class regions and c onventional linear data structures.