Towards a semantic model for Java wildcards

Wildcard types enrich the types expressible in Java, and extend the set of typeable Java programs. Syntactic models and proofs of soundness for type systems related to Java wildcards have been suggested in the past, however, the semantics of wildcards has not yet been studied. In this paper we propose a semantic model for Java wildcards, inspired by work on semantic subtyping, which traditionally interprets types as sets of possible values. To easily reflect the nominal type system of Java, our model is defined in terms of runtime types (closed class types) rather than the structure of the runtime values themselves. To reflect the variance introduced by wildcards, our model interprets types as sets of such closed class types. Having defined our model, we employ a standard semantic notion of subtyping. We show soundness of syntactic subtyping with respect to the semantic version, and demonstrate that completeness fails in the general case. We identify a restricted (but nonetheless rich) type language for which the syntactic notion of subtyping is both sound and complete.