Abstract
Linear typing schemes guarantee single-threadedness and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This has prompted research into static analysis and more sophisticated typing disciplines, to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this line of research by defining a new typing scheme which better approximates the semantic property of soundness of in-place update for a functional semantics. Our typing scheme includes two kinds of products ( ⊗and x), which allows data structures with or without sharing to be defined.We begin from the observation that some data is used only in a “read-only” context after which it may be safely re-used before being destroyed. Formalizing the inplace update interpretation and giving a machine model semantics allows us to refine this observation.We define three usage aspects apparent from the semantics, which are used to annotate function argument types. The aspects are (1) used destructively, (2) used read-only but shared with result, and (3) used read-only and not shared.
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
David Aspinall and Adriana Compagnoni. Heap bounded assembly language. Technical report, Division of Informatics, University of Edinburgh, 2002.
David Aspinall and Martin Hofmann. Heap bounded functional programming in Java. Implementation experiments, 2001.
E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579–612, 1996.
Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proceedings ACM Principles of Programming Languages, pages 262–275, 1999.
M. Draghicescu and S. Purushothaman. A uniform treatment of order of evaluation and aggregate update. Theoretical Computer Science, 118(2):231–262, September 1993.
Martin Hofmann. Linear types and non size-increasing polynomial time computation. In Logic in Computer Science (LICS), pages 464–476. IEEE, Computer Society Press, 1999.
Martin Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7(4):258–289, 2000. An extended abstract has appeared in Programming Languages and Systems, G. Smolka, ed., Springer LNCS, 2000.
Martin Hofmann. The strength of non size-increasing computation. In Proceedings ACM Principles of Programming Languages, 2002.
Samin Ishtiaq and Peter W. O’Hearn. BI as an assertion language for mutable data structures. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 14–26, New York, 2001. ACM.
Naoki Kobayashi. Quasi-linear types. In Proceedings ACM Principles of Programming Languages, pages 29–42, 1999.
Martin Odersky. Observers for linear types. In B. Krieg-Brückner, editor, ESOP’ 92: 4th European Symposium on Programming, Rennes, France, Proceedings, pages 390–407. Springer-Verlag, February 1992. Lecture Notes in Computer Science 582.
Peter W. O’Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–243, 1999.
P. W. O’Hearn, M. Takeyama, A. J. Power, and R. D. Tennent. Syntactic control of interference revisited. In MFPS XI, Conference on Mathematical Foundations of Program Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.
Simon Peyton-Jones and Keith Wansbrough. Simple usage polymorphism. In Proc. 3rd ACM SIGPLAN Workshop on Types in Compilation, Montreal, September 2000.
J. C. Reynolds. Syntactic control of interference. In Proc. Fifth ACM Symp. on Princ. of Prog. Lang. (POPL), 1978.
John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Jim Davies, Bill Roscoe, and Jim Woodcock, editors, Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.
Natarajan Shankar. Efficiently executing PVS. Technical report, Computer Science Laboratory, SRI International, 1999.
Frederick Smith, David Walker, and Greg Morrisett. Alias types. In G. Smolka, editor, Programming Languages and Systems, volume 1782, pages 366–381. Springer LNCS, 2000.
M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.
Philip Wadler. Linear types can change the world. In M. Broy and C. B. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561–581, Sea of Gallilee, Israel, 1990. North-Holland.
Mitchell Wand and William D. Clinger. Set constraints for destructive array update optimization. In Proc. IEEE Conf. on Computer Languages’ 98, pages 184–193, 1998.
Reinhard Wilhelm, Mooly Sagiv, and Thomas Reps. Shape analysis. In Proceedings Compiler Construction, CC 2000, 2000.
H. Yang and U. Reddy. Imperative lambda calculus revisited, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aspinall, D., Hofmann, M. (2002). Another Type System for In-Place Update. In: Le Métayer, D. (eds) Programming Languages and Systems. ESOP 2002. Lecture Notes in Computer Science, vol 2305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45927-8_4
Download citation
DOI: https://doi.org/10.1007/3-540-45927-8_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43363-7
Online ISBN: 978-3-540-45927-9
eBook Packages: Springer Book Archive