Wildcards extend Java generics by softening the mismatch between subtype and parametric polymorphism. Although they are a key part of the Java 5.0 programming language, a type system including wildcards has never been proven type sound. Wildcards have previously been formalised as existential types. In this paper we extend FGJ, a featherweight formalisation of Java with generics, with existential types. We prove that this calculus, ExistsJ, is type sound, and illustrate how it models wildcards in the Java Programming Language. ExistsJ is not a full model for Java wildcards, because it does not support lower bounds for wildcards. We discuss why ExistsJ can not be easily extended with lower bounds, and how full Java wildcards could be modelled in a type sound way.
Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs (ftfjp), in Association With Ecoop 2007, 2007, p. 1-13
Main Research Area:
9th Workshop on Formal Techniques for Java-like Programs (FTfJP), in association with ECOOP 2007
Nanjing University / University of Wisconsin-Milwaukee