A Type Theory for Memory Allocation and Data Layout

Preview

This week I’ll present “A Type Theory for Memory Allocation and Data Layout”, by Petersen, Harper, Crary, and Pfenning (POPL 2003). They use ordered type theory (a more strict form of linear types) to show how you can represent adjacency and thereby memory in programs.

Summary

The authors present a “type theoretic account of data layout” so that the layout of memory can be exposed to and controlled by typed, high-level languages. They begin with a discussion of memory creation (reservation, initialization, and allocation), and then discuss ordered linear logic/type theory (which lacks the exchange property present in affine or normal linear logic). A key point is that because ordered variables in this type theory cannot change position, they can represent locations in a region of memory; however, a downside of normal ordered type theory is that it is not size-preserving, because of arbitrary introduction of unrestricted terms. They present their “orderly” lambda calculus, which extends ordered type theory by ensuring that terms also maintain adjacency, by ensuring memory operations preserve size via the “fuse type.”

The rest of the paper discusses their syntax, static and dynamic semantics, and a translation of the standard lambda calculus to orderly lambda calculus. A few things are noteworthy: 1. Terms are “values that do not reserve or allocate in the course of their evaluation.” 2. Memory operations are done in expressions. 3. You can use coercions to manipulate the ordered variables in the frontier, combining or splitting them if adjacent to treat them as different types. 4. You can determine the size of data solely by its type.

Discussion

We first discussed the main points of the paper, went over the different types of substructural type systems as a review, and finally went over static semantics found at the end of the paper. I’ve been working on an implementation of this paper when I have time, and will include a link to the code when up on Github.