Abstract
Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004)
Barendregt, H.: The Lambda Calculus. Revised edn. North-Holland, Amsterdam (1984)
Bracha, G.: Generics in the Java programming language (2004), http://java.sun.com/j2se/1.5/pdf/generics-tutorial.pdf
Cameron, N., Drossopoulou, S., Noble, J., Smith, M.: Multiple Ownership. In: OOPSLA 2007 (October 2007)
Cameron, N., Ernst, E., Drossopoulou, S.: Towards an existential types model for java wildcards. In: 9th Workshop on Formal Techniques for Java-like Programs (2007)
Cardelli, L., Leroy, X.: Abstract types and the dot notation. Research report 56, DEC Systems Research Center (1990)
Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Computing Surveys 17(4), 471–522 (1985)
Chin, W.-N., Craciun, F., Khoo, S.-C., Popeea, C.: A flow-based approach for variant parametric types. In: Proceedings of the 2006 ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA 2006). ACM Press, New York (2006)
Clarke, D., Drossopoulou, S., Noble, J., Wrigstad, T.: Tribe: a simple virtual class calculus. In: AOSD 2007: Proceedings of the 6th international conference on Aspect-oriented software development, Vancouver, British Columbia, Canada, pp. 121–134. ACM, New York (2007), http://doi.acm.org/10.1145/1218563.1218578
Ghelli, G., Pierce, B.: Bounded existentials and minimal typing. Theoretical Computer Science 193(1-2), 75–96 (1998)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification Third Edition. Addison-Wesley, Boston (2005)
Grossman, D.: Existential types for imperative languages. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, pp. 21–35. Springer, Heidelberg (2002)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001); An earlier version of this work appeared at OOPSLA 1999.
Igarashi, A., Viroli, M.: Variant parametric types: A flexible subtyping scheme for generics. ACM Trans. Program. Lang. Syst. 28(5), 795–847 (2006); An earlier version appeared as On variance-based subtyping for parametric types at (ECOOP 2002)
Kennedy, A.J., Pierce, B.C.: On decidability of nominal subtyping with variance. In: International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD 2007), Nice, France (January 2007)
Lu, Y., Potter, J.: On ownership and accessibility. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 99–123. Springer, Heidelberg (2006)
Torgersen, M., Ernst, E., Hansen, C.P.: Wild FJ. In: 12th International Workshop on Foundations of Object-Oriented Languages (FOOL 12), Long Beach, California, ACM Press, New York (2005)
Madsen, O.L., Moller-Pedersen, B.: Virtual classes: a powerful mechanism in object-oriented programming. In: OOPSLA 1989: Conference proceedings on Object-oriented programming systems, languages and applications, pp. 397–406. ACM Press, New York (1989)
Mazurak, K., Zdancewic, S.: Note on Type Inference for Java 5: Wildcards, F-Bounds, and Undecidability (2006), http://www.cis.upenn.edu/~stevez/note.html
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential types. In: POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 37–51. ACM Press, New York (1985)
Pierce, B.C.: Bounded quantification is undecidable. In: POPL 1992: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 305–315. ACM Press, New York (1992)
Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)
Krab Thorup, K., Torgersen, M.: Unifying genericity - combining the benefits of virtual types and parameterized classes. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, pp. 186–204. Springer, Heidelberg (1999)
Torgersen, M., Hansen, C.P., Ernst, E., von der Ahé, P., Bracha, G., Gafter, N.: Adding wildcards to the Java programming language. Journal of Object Technology 3(11), 97–116 (2004); Special issue: OOPS track at SAC 2004, Nicosia/Cyprus.
Urban, C., Berghofer, S., Norrish, M.: Barendregt’s variable convention in rule inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 35–50. Springer, Heidelberg (2007)
Viroli, M., Rimassa, G.: On access restriction with Java wildcards. Journal of Object Technology 4(10), 117–139 (2005); Special issue: OOPS track at SAC 2005, Santa Fe/New Mexico. The earlier version in the proceedings of SAC 2005 appeared as Understanding access restriction of variant parametric types and Java wildcards.
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Wrigstad, T., Clarke, D.: Existential owners for ownership types. JOT 6(4), 141–159 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cameron, N., Drossopoulou, S., Ernst, E. (2008). A Model for Java with Wildcards. In: Vitek, J. (eds) ECOOP 2008 – Object-Oriented Programming. ECOOP 2008. Lecture Notes in Computer Science, vol 5142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70592-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-70592-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70591-8
Online ISBN: 978-3-540-70592-5
eBook Packages: Computer ScienceComputer Science (R0)