SCS Undergraduate Thesis Topics
|Matthew Kehrt||Jonathan Aldrich||Linearity for Objects|
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.