Subtyping for Object Type Constructors
Dominic Duggan, Adriana B. Compagnoni · 2007
Object type constructors have been introduced as an approach to adding container object types to a language with type inference. Useful subtyping for object type constructors requires a flexible subtype rule for type constructors that is not simply the pointwise extension of subtyping for types. At the same time, subtyping should avoid requiring run-time type checks, as in the Java subtype rule for arrays. An extension of object type constructors is considered to allow this subtyping, extending the kinds of object type constructors with polarities that allow this subtyping without jeopardizing soundness. 1 Introduction Recent years have seen much attention paid to the foundations of typed object oriented programming languages. Less attention has been paid to the types of container objects (for example, vectors, lists and arrays). Such objects provides interfaces that are parameterized by one or more type variables (representing the element type, in the aforesaid examples). A formal ca...