Lambda the Ultimate

Implicit Ownership Types for Memory Management. Tian Zhao, Jason Baker, James Hunt, James Noble, and Jan Vitek. Draft.

The Real-time Specification for Java (RTSJ) introduced a range of language features for explicit memory management. While the RTSJ gives programmers fine control over memory use and allows linear allocation and constant time deallocation, the RTSJ relies upon dynamic runtime checks for safety making it unsuitable for safety critical applications. We introduce ScopeJ, a statically typed, multi-threaded, object calculus in which scopes are first class constructs. Scopes reify allocation contexts and provide a safe alternative to automatic memory management. Safety is the result of our use of an ownership type system that enforces a topology on run-time patterns of references. ScopeJ's type system is novel in that ownership annotations are implicit. This substantially reduces the burden for developers, thus increasing the likelihood of adoption. The notion of implicit ownership is particularly appealing when combined with pluggable type systems, as one can apply different type constraints to components depending on the requirements. In related work we have demonstrated the usefulness of our approach in different applications

An example of a pluggable type system which, unlike previous discussions on LtU, eg. Gilad Is Right and Flexible Addition of Static Typing to Dynamically Typed Programs, adds more type rules to an already statically typed language. It doesn't, however, appear to be an optional type system as it seems to make use of a library and some syntactic rules to encode the region types.

The type system itself seems quite complicated which may be due to building on Java's existing type system as much as the support for first-class and multi-threaded regions, an aspect which seems to be unique in region calculi. Compare the complete type system for F^RGN in Monadic Regions. Not that I can claim to understand all the maths in that paper either but Oleg Kiselyov's implemetation on top of Haskell's ST monad is short and sweet.