Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Adaption and Focus: Practical Linear Types for Imperative Programming

Manuel Fahndrich and Robert DeLine

Abstract

A type system with linearity is useful for checking software protocols andresource management at compile time. Linearity provides powerful reasoning about state changes, but at the price of restrictions on aliasing. The hard division between linear and nonlinear types forces the programmer to make a trade-off between checking a protocol on an object and aliasing the object. Most onerous is the restriction that any type with a linear component must itself be linear. Because of this, checking a protocol on an object imposes aliasing restrictions on any data structure that directly or indirectly points to the object. We propose a new type system that reduces these restrictions with the adoption and focus constructs. Adoption safely allows a programmer to alias objects on which she is checking protocols, and focus allows the reverse. A programmer can alias data structures that point to linear objects and use focus for safe access to those objects. We discuss how we implemented these ideas in the Vault programming language.

Details

Publication typeInproceedings
Published inProceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation
PublisherAssociation for Computing Machinery, Inc.
> Publications > Adaption and Focus: Practical Linear Types for Imperative Programming