| Towards an Existential Types Model for Java (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. 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, ∃J, is type sound, and illustrate how it models wildcards in the Java Programming Language. ∃J is not a full model for Java wildcards, because it does not support lower bounds for wildcards. We discuss why ∃J can not be easily extended with lower bounds, and how full Java wildcards could be modelled in a type sound way. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||