Abstract
Linear types provide the framework for a safe embedding of mutable state in functional languages by enforcing the principle that variables of linear type must be used exactly once. A potential disadvantage of this approach is that it places read accesses to such variables under the same restriction as write accesses, and thus prevents reads to proceed in parallel. We present here an extension of linear types which augments the usual distinction between linear and non-linear by a third state, observers of linear variables. Since, unlike linear variables, observers can be duplicated, multiple concurrent reads are made possible. On the other hand, observers must be short-lived enough to never overlap with mutations. The resulting type system is in many aspects similar to the one of ML: It is polymorphic, has principal types, and admits a type reconstruction algorithm.
work was done in part while at IBM T.J. Watson Research Center.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. Abramsky. Computational interpretations of linear logic. Preprint, Imperial College, London, 1990.
H.G. Baker. Unify and conquer (garbage, updating, aliasing, ...) in functional languages. In Proc. ACM Conf. on LISP and Functional Programming, pages 218–226, June 1990.
A. Bloss. Update analysis and the efficient implementation of functional aggregates. In Proc. ACM Conf. on Functional Programming Languages and Computer Architecture, August 1989.
D. Clement, J. Despeyroux, T. Despeyroux, L. Hascoet, and G. Kahn. Natural semantics on the computer. Technical Report RR 416, INRIA, June 1985.
S. Cohen. Multi-version structures in prolog. In Proc. Conf. on Fifth Generation Computer Systems, pages 265–274, 1984.
A. Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In Proc. 17th ACM Symposium on Principles of Programming Languages, Jan. 1990.
M. Draghicescu and S. Puroshothaman. A compositional analysis of evaluation order and its application. In Proc. ACM Conf. on Lisp and Functional Programming, June 1990.
J.C. Guzmán and P. Hudak. Single-threaded polymorphic lambda calculus. In Proc. 5th IEEE Symp. on Logic in Computer Science, June 1990.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
K. Gharachorloo, V. Sarkar, and J.L. Hennessy. A simple and efficient approach for single assignment languages. In Proc. ACM Conf. on Lisp and Functional Programming, 1988.
P. Hudak. A semantic model of reference counting and its abstraction. In S. Abramsky and C. Hankin, editors, Abstract interpretation of declarative languages. Ellis Horwood Ltd., 1987.
P. Jouvelot and D.K. Gifford. Algebraic reconstruction of types and effects. In Proc. 18th ACM Symp. on Principles of Programming Languages, pages 303–310, Jan. 1991.
Mark P. Jones. Towards a theory of qualified types. Technical Report PRG-TR-6-91, Oxford University Computing Laboratory, Oxford, UK, 1991.
Mark P. Jones. Type inference for qualified types. Technical Report PRG-TR-10-91, Oxford University Computing Laboratory, Oxford, UK, 1991.
Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.
J. Lucassen and D.K. Gifford. Polymorphic effect systems. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 47–57, Jan. 1988.
A. Neirynk, P. Panangaden, and A. Demers. Computation of aliases and support sets. In Proc. 14th ACM Symp. on Principles of Programming Languages, pages 274–283, Jan. 1987.
M. Odersky. How to make destructive updates less destructive. In Proc. 18th ACM Symp. on Principles of Programming Languages, pages 25–36, Jan. 1991.
D.A. Schmidt. Detecting global variables in denotational specifications. ACM Transactions on Programming Languages and Systems, 5(2):299–310, 1985.
V. Swarup, U.S. Reddy, and E. Ireland. Assignments for applictive languages. In Proc. ACM Conf. on Functional Programming Languages and Computer Architecture, August 1991.
J.-P. Talpin and P. Jouvelot. Type, effect and region reconstruction in polymorphic functional languages. In Workshop on Static Analysis of Equational, Functional, and Logic Programs, Bordeaux, Oct. 1991.
P. Wadler. Comprehending monads. In Proc. ACM Conf. on LISP and Functional Programming, pages 61–78, June 1990.
Phil Wadler. Linear types can change the world! In Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, pages 547–566, April 1990.
P. Wadler. Is there a use for linear logic? In Proc. ACM Symp. on Partial Evaluation and Semantic-Based Program Manipulation, pages 255–273, June 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Odersky, M. (1992). Observers for linear types. In: Krieg-Brückner, B. (eds) ESOP '92. ESOP 1992. Lecture Notes in Computer Science, vol 582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55253-7_23
Download citation
DOI: https://doi.org/10.1007/3-540-55253-7_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55253-6
Online ISBN: 978-3-540-46803-5
eBook Packages: Springer Book Archive