Inclusion polymorphism (subclassing) and parametric polymorphism (generics) are often present in modern object oriented languages. However, their integration is usually limited; an important example is that variant subtyping of parametric types is usually forbidden, even though in some circumstances it is safe and desirable. Existential types have been used to bridge the gap between these two forms of polymorphism used in, for example, Java wildcards or Variant Parametric Types.
In this thesis we investigate how existential types can be used to implement variant subtyping. We contribute a soundness proof for Java with wildcards, and a new, minimal language that uses existential types to implement variance for ownership types.
Java wildcards provide subtype variance to Java generics in a powerful and programmer friendly way. Wildcards have been formalised using a variation on existential types; however, there has never been a type soundness proof for Java with wildcards. Our main contribution is a new formal model of Java with wildcards (Tame FJ) and a detailed proof of soundness.
Ownership types are a mechanism for structuring the topology of the heap in object oriented programs. In an ownership types system, types are parameterised by owners. Similarly to generics, owners are traditionally treated invariantly. There have been several, mostly ad hoc, attempts to add some form of subtype variance to owner-parametric types. Our second contribution is a minimal calculus (Jo&exist) where existential quantification of owners is used to uniformly and cleanly support variance. We include type parametricity in our language, and the interaction of this with existentially quantified owners allows us to more precisely specify the ownership properties of collections and similar code structures. We prove soundness and the owners-as-dominators property for this system.