Hostname: page-component-8448b6f56d-c47g7 Total loading time: 0 Render date: 2024-04-24T00:01:13.461Z Has data issue: false hasContentIssue false
  • English
  • Français

A type system with usage aspects

Part of: JFP Research Articles

Published online by Cambridge University Press:  01 March 2008

DAVID ASPINALL ,
MARTIN HOFMANN  and
MICHAL KONEČNÝ
DAVID ASPINALL
Affiliation:
LFCS Edinburgh, Mayfield Rd, Edinburgh EH9 3JZ, UK (e-mail: David.Aspinall@ed.ac.uk) http://homepages.inf.ed.ac.uk/da/
MARTIN HOFMANN
Affiliation:
Institut für Informatik, Oettingenstraβe 67, 80538 München, Germany (e-mail: mhofmann@informatik.uni-muenchen.de) http://www.tcs.informatik.uni-muenchen.de~mhofmann/
MICHAL KONEČNÝ
Affiliation:
Aston University, Aston Triangle, Birmingham, B4 7ET, UK (e-mail: m.konecny@aston.ac.uk) http://www.aston.ac.uk~konecnym/
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Linear typing schemes can be used to guarantee non-interference 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 limitation 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 direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a “read-only” context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that 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 with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konečn'y (In TYPES 2002 workshop, Nijmegen, Proceedings, Springer-Verlag, 2003).

Type
Articles
Information
Journal of Functional Programming , Volume 18 , Issue 2 , March 2008 , pp. 141 - 178
Copyright
Copyright © Cambridge University Press 2007

References

Wikipedia article on the administrative normal form. (2007). http:\\en.wikipedia.org wiki/Administrative_Normal_Form. Accessed March 27, 2007.Google Scholar
Aiken, A., Foster, J. S., Kodumal, J. & Terauchi, T. (2003). Checking and inferring local non-aliasing. In PLDI '03: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation. New York: ACM Press, pp. 129–140.CrossRefGoogle Scholar
Aspinall, D. & Compagnoni, A. (2003). Heap-bounded assembly language. J. Automated Reason. 31 (3/4), 261–302.CrossRefGoogle Scholar
Aspinall, D. & Hofmann, M. (2002). Another type system for in-place update. In Programming Languages and Systems, Proceedings of 11th European Symposium on Programming, D. L. Métayer (ed), Springer-Verlag. Lecture Notes in Computer Science 2305.CrossRefGoogle Scholar
Aspinall, D. & Konevcný, M. (2003, February). Type Systems for Resource Bounded Programming and Compilation Project Homepage. http://homepages.inf.ed.ac.uk/da/resbnd. Accessed 1 June 2007.Google Scholar
Barendsen, E. & Smetsers, S. (1996). Uniqueness typing for functional languages with graph rewriting semantics. Math. Struct. Comput. Sci. 6, 579–612.CrossRefGoogle Scholar
Boyland, J. (2003). Checking interference with fractional permissions. In Static Analysis: 10th International Symposium, Cousot, R. (ed), Lecture Notes in Computer Science, vol. 2694. Berlin, Heidelberg, New York: Springer, pp. 55–72.CrossRefGoogle Scholar
Crary, K., Walker, D. & Morrisett, G. (1999). Typed memory management in a calculus of capabilities. In Proceedings ACM Principles of Programming Languages, Kobayashi: Hofmann & Jost, Istiaq & O'Hearn, pp. 262–275.CrossRefGoogle Scholar
Dor, N., Rodeh, M. & Sagiv, M. (2000). Checking cleanness in linked lists. In Proceedings of the Seventh International Static Analysis Symposium. Springer, Berlin/Heidelberg, pp. 115–134. Lecture Notes in Computer Science 1824.CrossRefGoogle Scholar
Draghicescu, M. & Purushothaman, S. (1993). A uniform treatment of order of evaluation and aggregate update. Theor. Comput. Sci. 118 (2), 231–262.CrossRefGoogle Scholar
Evans, D. (1996). Static detection of dynamic memory errors. In PLDI '96: Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation. New York: ACM Press, pp. 44–53.CrossRefGoogle Scholar
Fahndrich, M. & DeLine, R. (2002). Adoption and focus: Practical linear types for imperative programming. In Pldi '02: Proceedings of the ACM Sigplan 2002 Conference on Programming Language Design and Implementation. New York: ACM Press, pp. 13–24.CrossRefGoogle Scholar
Gifford, D. K., & Lucassen, J. M. (1986). Integrating functional and imperative programming. LFP '86: Proceedings of the 1986 ACM Conference on LISP and Functional Programming. New York: ACM Press, pp. 28–38.CrossRefGoogle Scholar
Hofmann, M. (2000). A type system for bounded space and functional in-place update. Nordic J. Comput., 7 (4), 258–289. An extended abstract has appeared in Programming Languages and Systems, G. Smolka, ed., Springer LNCS, 2000.Google Scholar
Hofmann, M. & Jost, S. (2003). Static prediction of heap space usage for first-order functional programs. In 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL '03), New York: ACM Press, pp. 185–197.CrossRefGoogle Scholar
Ishtiaq, S. & O'Hearn, P. W. (2001). BI as an assertion language for mutable data structures. The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '01), New York: ACM Press, pp. 14–26.CrossRefGoogle Scholar
Kobayashi, N. (1998). Quasi-linear Types. Tech. rept. 98–02. Department of Information Science, University of Tokyo.Google Scholar
Kobayashi, N. (1999). Quasi-linear types. 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '99), New York: ACM Press, pp. 29–42.CrossRefGoogle Scholar
Konečný, M. (2003a). Functional in-place update with layered datatype sharing. TLCA 2003, Valencia, Spain, Proceedings. Springer-Verlag, pp. 195–210. Lecture Notes in Computer Science 2701.CrossRefGoogle Scholar
Konečný, M. (2003b). Typing with conditions and guarantees for functional in-place update. In TYPES 2002 Workshop, Nijmegen, Proceedings. Springer-Verlag, pp. 182–199. Lecture Notes in Computer Science 2646.CrossRefGoogle Scholar
MacKenzie, K. & Wolverson, N. (2004). Camelot and grail: resource-aware functional programming on the JVM. Trends in Functional Programing, Vol. 4. Bristol: Intellect, pp. 29–46.Google Scholar
Odersky, M. (1992). Observers for linear types. 4th European Symposium on Programming (ESOP '92), B. Krieg-Brückner (ed), Rennes, France: Springer-Verlag, pp. 390–407. Lecture Notes in Computer Science 582.CrossRefGoogle Scholar
O'Hearn, P. W., Takeyama, M., Power, A. J., & Tennent, R. D. (1995). Syntactic control of interference revisited. In MFPS XI, Conference on Mathematical Foundations of Program Semantics. Electronic Notes in Theoretical Computer Science, vol. 1. Elsevier.Google Scholar
Peyton, J. S. & Wansbrough, K. (2000, September). Simple usage polymorphism. In Proc. 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC 2000). Technical Report CMU–CS–00–161.Google Scholar
Reynolds, J. C. (1978). Syntactic control of interference. Proceedings of the Fifth ACM Symposium on Principles of Programming Languages (POPL). Tucson, AZ: ACM Press, pp. 39–46.CrossRefGoogle Scholar
Reynolds, J. C. (2002). Separation logic: A logic for shared mutable data structures. Proceedings of 17th annual IEEE Symposium on Logic in Computer Science (LICS'02), pp. 55–74.CrossRefGoogle Scholar
Sabry, A. & Felleisen, M. (1993). Reasoning about programs in continuation-passing style. LISP and Symbolic Comput., 6 (3/4), 289–360.CrossRefGoogle Scholar
Shankar, N. (1999, November). Efficiently Executing PVS. Project report, Computer Science Laboratory, SRI International, Menlo Park, CA.Google Scholar
Smith, F., Walker, D. & Morrisett, G. (2000). Alias types. In: 9th European Symposium on Programming (ESOP'00), Smolka, G. (ed), Springer-Verlag, pp. 366–381. Lecture Notes in Computer Science 1782.Google Scholar
Talpin, J.-P. & Jouvelot, P. (1994). The type and effect discipline. Inf. Comput., 111 (2), 245–296.CrossRefGoogle Scholar
Tofte, M., & Talpin, J.-P. (1997). Region-based memory management. Inf. Comput., 132 (2), 109–176.CrossRefGoogle Scholar
Wadler, P. (1990). Linear types can change the world. IFIP TC 2 Working Conference on Programming Concepts and Methods, M. Broy & C. B., Jones (eds), Sea of Gallilee, Israel: North-Holland, pp. 561–581.Google Scholar
Walker, D. & Morrisett, J. G. (2001). Alias types for recursive data structures. In TIC '00: Selected Papers from the Third International Workshop on Types in Compilation. London, UK: Springer-Verlag, pp. 177–206.Google Scholar
Wand, M. & Clinger, W. D. (1998). Set constraints for destructive array update optimization. In Proc. IEEE International Conference on Computer Languages (ICCL'98), IEEE, pp. 184–193.CrossRefGoogle Scholar
Wilhelm, R., Sagiv, M., & Reps, T. (2000). Shape analysis. In Proc. 9th International Conference on Compiler Construction (CC 2000). Springer-Verlag, pp. 1–70. Lecture Notes in Computer Science 1781.CrossRefGoogle Scholar
Yang, H., & Reddy, U. (1997). Imperative lambda calculus revisited. Electronic manuscript.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.