Institute for Software Research
School of Computer Science, Carnegie Mellon University


Linearity For Objects

Matthew Kehrt, Andi Bejleri*, Jonathan Aldrich

July 2006


Keywords: Linear types, object calculi, prototyped-based languages, static type checker, type safety

Linear type systems guarantee that no copies are made of certain program values. The EGO language is a foundational calculus which adds linearity to object oriented languages. EGO allows changes to be made to the interface of an object, such as the addition or removal of methods, as long as such an object is linear, i.e., there exists only one reference to it. However, this linearity constraint is often unwieldy and hard to program with. We extend EGO with a linguistic primitive for temporarily relaxing the linearity guarantee. EGO allows objects to be linear and enforces that only one reference exists such an object. We allow multiple references to linear objects in certain expressions by borrowing references to these objects. Borrowing annotates the type of the reference with a region, which is a unique token indicating where the reference was borrowed. We disallow references with types containing regions that are not currently borrowed. We use this to temporarily make multiple references to an object in a given expression but enforce that outside this expression only one reference exists.

53 pages

*Computer Science Department, Universita di Pisa, Lungarno Pacinotti, 43, 56126 Pisa, Italy

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by