|
CMU-ISRI-06-115
Institute for Software Research
School of Computer Science, Carnegie Mellon University
CMU-ISRI-06-115
Linearity For Objects
Matthew Kehrt, Andi Bejleri*, Jonathan Aldrich
July 2006
CMU-ISRI-06-115.pdf
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
|