Variant Parametric Types: A Flexible Subtyping Scheme for Generics

By Atsushi Igarashi and Mirko Viroli. ACM Transactions on Programming Languages and Systems, 28(5):795-847, September 2006.

An earlier version "On Variance-Based Subtyping for Parametric Types" appeared in Proceedings of the Sixteenth European Conference on Object-Oriented Programming (ECOOP2002), Springer LNCS 2374, pages 441-469, Málaga, Spain, June 2002.


We develop the mechanism of variant parametric types, as a means to enhance synergy between parametric and inclusion polymorphism in object-oriented programming languages. Variant parametric types are used to control both subtyping between different instantiations of one generic class and the accessibility of their fields and methods. On one hand, one parametric class can be used to derive covariant types, contravariant types, and bivariant types (generally called variant parametric types), by attaching a variance annotation to a type argument. On the other hand, the type system prohibits certain method/field accesses according to variance annotations, when those accesses may otherwise make the program unsafe. By exploiting variant parametric types, a programmer can write generic code abstractions working on a wide range of parametric types in a safe way. For instance, a method that only reads the elements of a container of numbers can be easily modified so as to accept containers of integers, floating point numbers, or any subtype of the number type.

Technical subtleties in typing for the proposed mechanism are addressed in terms of an intuitive correspondence between variant parametric types and bounded existential types. Then, for a rigorous argument of correctness of the proposed typing rules, we extend Featherweight GJ---an existing formal core calculus for Java with generics---with variant parametric types and prove type soundness.