Capabilities for External Uniqueness

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.