Capabilities for External Uniqueness

Philipp Haller and Martin Odersky have submitted Capabilities for External Uniqueness to OOPSLA'09.

Unique object references have many important applications in object-oriented programming. For instance, with sufficient encapsulation properties they enable safe and efficient transfer of message objects between concurrent processes. However, it is a long-standing challenge to integrate unique references into practical object-oriented programming languages.

This paper introduces a new approach to external uniqueness. The idea is to use capabilities for enforcing both aliasing constraints that guarantee external uniqueness, and linear consumption of unique references. We formalize our approach as a type system, and prove a type preservation theorem. Type safety rests on an alias invariant that builds on a novel formalization of external uniqueness.

We show how a capability-based type system can be used to integrate external uniqueness into widely available object-oriented programming languages. Practical experience suggests that our system allows adding uniqueness information to common collection classes in a simple and concise way.

A prototype plugin for the Scala compiler can be found on the same page.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

now

that's a bibliography.

Cool work

That is a very cool work.

This line:

  def append(other: LinkedList @unique) {

It reminded me of C++:

  void append(std::auto_ptr<LinkedList> other) {

Now I do realize that "auto_ptr" does not guarantee uniqueness, but it comes close. In fact using a custom allocator, and a few custom pointer types one could create a unique pointer. I find the parallel interesting.

Update

There's an updated version of the system at Capabilities for Uniqueness and Borrowing.