A Theory of Linear Objects

Recently, linearity has been proposed as a mechanism for mem- ory management, alias control, and typestate tracking. While linear type systems have been extensively studied in functional program- ming, their use in object-oriented systems has been limited to useful but ad-hoc annotation systems that track unique pointers. In this paper, we study object-oriented linearity at level of foun- dational object calculi. Our system tracks not only linear objects (to which there may be only one pointer), but linear methods as well (which may be called at most once). Tracking linear objects allows us to ensure type safety for imperative, type-changing update to methods and imperative, type-changing dynamic inheritance. Be- cause some aliasing is important in practical systems, our system supports linear and non-linear objects and methods and a novel region system that permits borrowed aliases to linear objects. To enforce safety, we allow type-changing modifications only on un- borrowed linear objects, but permit such changes again when these borrowed references are no longer accessible. Note: an earlier ver- sion of this paper appeared in the proceedings of FOOL '06. The current paper includes a simpler and cleaner formalism (with only methods, no lambdas) and significantly extends the previous system with borrowing via regions.