Manuel Fahndrich
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.
- J. Boyland. Alias burying: Unique variables without destructive reads Software---Practice and Experience, 31(6):533--553, May 2001]] Google Scholar
Digital Library
- K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities]] Google ScholarDigital Library
- R. DeLine and M. Fahndrich. Enforcing high-level protocols in low-level software. Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2001]] Google ScholarDigital Library
- D. Gay and A. Aiken. Memory management with explicit regions. Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation, number 33:5 in SIGPLAN notices, pages 313--323, June 1998]] Google ScholarDigital Library
- F. Henglein, H. Makholm, and H. Niss. A direct approach to control-flow sensitive region-based memory management. ACM Conference on Principles and Practice of Declarative Programming, Sept. 2001]] Google ScholarDigital Library
- S. S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. Conference Record of the 28th Annual ACM Symposium on Principles of Programming Languages, pages 14--26. ACM Press, Jan. 2001]] Google ScholarDigital Library
- V. Kuncak, P. Lam, and M. C. Rinard. Role analysis. Conference Record of the 29th Annual ACM Symposium on Principles of Programming Languages, Jan. 2002]] Google ScholarDigital Library
- K. R. M. Leino and G. Nelson. Data abstraction and information hiding.Technical Report 160, Compaq SRC, nov 2000]]Google Scholar
- M. Odersky. Observers for linear types. B. Krieg-Bruckner, editor, ESOP '92: 4th European Symposium on Programming, Rennes, France, Proceedings, pages 390--407, New York, 1992. Springer-Verlag]] Google ScholarDigital Library
- Conference Record of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, Jan. 1999]]Google Scholar
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic.In POPL'99 \citepopl99, pages 105--118]] Google ScholarDigital Library
- S. Smetsers, E. Barendsen, M. v. Eekelen, and R. Plasmeijer. Guaranteeing safe destructive updates through a type system with uniqueness information for graphs. Lecture Notes in Computer Science, 776:358--379, 1994]] Google ScholarDigital Library
- F. Smith, D. Walker, and J. G. Morrisett. Alias types. European Symposium on Programming, pages 366--381, 2000]] Google ScholarDigital Library
- R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. SE-12(1):157--171, Jan. 1986]] Google ScholarDigital Library
- M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, P. Sestoft, and P. Bertelsen. Programming with regions in the ml kit (for version 3). Technical Report 98/25, Department of Computer Science, University of Copenhagen, 1998]]Google Scholar
- M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value-calculus using a stack of regions. Conference Record of the 21st Annual ACM SSymposium on Principles of Programming Languages, pages 188--201, Jan. 1994]] Google ScholarDigital Library
- P. Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods. Apr. 1990. IFIP TC 2 Working Conference]]Google Scholar
- D. Walker and G. Morrisett. Alias types for recursive data structures. Proceedings of the 4th Workshop on Types in Compilation, Sept. 2000]] Google ScholarDigital Library
- D. Walker and K. Watkins. On linear types and regions. Proceedings of the International Conference on Functional Programming (ICFP '01), Sept. 2001]]Google Scholar
Index Terms
- Adoption and focus: practical linear types for imperative programming
Recommendations
Linear Haskell: practical linearity in a higher-order polymorphic language
Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-...
Adoption and focus: practical linear types for imperative programming
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 ...
Disjointness domains for fine-grained aliasing
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and ApplicationsAliasing is crucial for supporting useful implementation patterns, but it makes reasoning about programs difficult. To deal with this problem, numerous type-based aliasing control mechanisms have been proposed, expressing properties such as uniqueness. ...
Comments