Variant Parametric Types: A Flexible Subtyping Scheme for Generics (On Variance-Based Subtyping for Parametric Types)

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.

Abstract

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.

PDF

Earlier version (pdf, 279kbytes). Copyright © 2002 by Springer-Verlag. See LNCS home page. Note: In the third rule on page 23, the fifth premise Δ ... should have been Δ, Δ' ... (Sorry for this small but technically significant typo!)
Full version. (pdf, 462kbytes); Preprint version. Copyright © 2006 by ACM. This document is posted by permission of ACM and may not be redistributed. See copyright notice. Note: Some occurrences of setFst0 in the published version should be setFst(). On page 20, "subtype" in "For example, a Z-free subtype of" should be "supertype".