Abstract
We present a uniqueness type system that is simpler than both Clean’s uniqueness system and a system we proposed previously. The new type system is straightforward to implement and add to existing compilers, and can easily be extended with advanced features such as higher rank types and impredicativity. We describe our implementation in Morrow, an experimental functional language with both these features. Finally, we prove soundness of the core type system with respect to the call-by-need lambda calculus.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barendsen, E., Smetsers, S.: Conventional and uniqueness typing in graph rewrite systems. Technical Report CSI-R9328, University of Nijmegen (December 1993)
Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Math. Struct. in Computer Science 6, 579–612 (1996)
De Vries, E., Plasmeijer, R., Abrahamson, D.: Uniqueness typing redefined. In: Horváth, Z., Zsók, V., Butterfield, A. (eds.) IFL 2006. LNCS, vol. 4449. Springer, Heidelberg (2007)
Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. JFP 8(3), 275–317 (1998)
Jones, M.P.: A system of constructor classes: overloading and implicit higher-order polymorphism. In: FPCA 1993, pp. 52–61 (1993)
Sheard, T.: Putting Curry-Howard to work. In: Haskell Workshop 2005, pp. 74–85. ACM, New York (2005)
Sulzmann, M., Chakravarty, M.M.T., Jones, S.P., Donnelly, K.: System F with type equality coercions. In: TLDI 2007, pp. 53–66. ACM Press, New York (2007)
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL 1982, pp. 207–212 (1982)
Baader, F., Niphow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Brown, F.M.: Boolean Reasoning. Dover Publications, Inc. (2003)
Peyton Jones, S., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitrary-rank types. JFP 17(1), 1–82 (2007)
Leijen, D.: HMF: Simple type inference for first-class polymorphism. Technical Report MSR-TR-2007-118, Microsoft Research, Redmond
Vytiniotis, D., Weirich, S., Peyton Jones, S.: Boxy types: inference for higher-rank types and impredicativity. In: ICFP 2006, pp. 251–262 (2006)
Botlan, D.L., Rémy, D.: MLF: raising ML to the power of System F. In: ICFP 2003, pp. 27–38 (2003)
Walker, D.: Substructural type systems. In: Pierce, B. (ed.) Advanced Topics in Types and Programming Languages. The MIT Press, Cambridge (2005)
Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19–75 (2002)
Launchbury, J.: A natural semantics for lazy evaluation. In: POPL 1993, pp. 144–154 (1993)
de Vries, E.: Uniqueness typing simplified—technical appendix. Technical Report TCD-CS-2008-19, Trinity College Dublin
Harrington, D.: Uniqueness logic. Theor. Comput. Sci. 354(1), 24–41 (2006)
Hage, J., Holdermans, S., Middelkoop, A.: A generic usage analysis with subeffect qualifiers. In: ICFP 2007, pp. 235–246. ACM, New York (2007)
Hage, J., Holdermans, S.: Heap recycling for lazy languages. In: PEPM 2008, pp. 189–197. ACM, New York (2008)
Wadler, P.: Is there a use for linear logic? In: PEPM 1991, pp. 255–273 (1991)
Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: FPCA 1995, pp. 1–11 (1995)
Guzman, J., Hudak, P.: Single-threaded polymorphic lambda calculus. In: Logic in Computer Science 1990, June 1990, pp. 333–343 (1990)
Plasmeijer, R., van Eekelen, M.: Clean language report (version 2.1)
Odersky, M.: Observers for linear types. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 390–407. Springer, Heidelberg (1992)
Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. SIGPLAN Not. 43(1), 3–15 (2008)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Vries, E., Plasmeijer, R., Abrahamson, D.M. (2008). Uniqueness Typing Simplified. In: Chitil, O., Horváth, Z., Zsók, V. (eds) Implementation and Application of Functional Languages. IFL 2007. Lecture Notes in Computer Science, vol 5083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85373-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-85373-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85372-5
Online ISBN: 978-3-540-85373-2
eBook Packages: Computer ScienceComputer Science (R0)