15.5 Subtyping and Other Features

< Free Open Study >

As we extend our simple calculus with subtyping toward a full-blown programming language, each new feature must be examined carefully to see how it interacts with subtyping. In this section we consider some of the features we have seen at this point.^[3] Later chapters will take up the (significantly more complex) interactions between subtyping and features such as parametric polymorphism (Chapters 26 and 28), recursive types (Chapters 20 and 21), and type operators (Chapter 31).

Ascription and Casting

The ascription operator t as T was introduced in §11.4 as a form of checked documentation, allowing the programmer to record in the text of the program the assertion that some subterm of a complex expression has some particular type. In the examples in this book, ascription is also used to control the way in which types are printed, forcing the typechecker to use a more readable abbreviated form instead of the type that it has actually calculated for a term.

In languages with subtyping such as Java and C++, ascription becomes quite a bit more interesting. It is often called casting in these languages, and is written (T)t. There are actually two quite different forms of casting-so-called up-casts and down-casts. The former are straightforward; the latter, which involve dynamic type-testing, require a significant extension.

Up-casts, in which a term is ascribed a supertype of the type that the typechecker would naturally assign it, are instances of the standard ascription operator. We give a term t and a type T at which we intend to "view" t. The typechecker verifies that T is indeed one of the types of t by attempting to build a derivation

using the "natural" typing of t, the subsumption rule T-SUB, and the ascription rule from §11.4:

Up-casts can be viewed as a form of abstraction-a way of hiding the existence of some parts of a value so that they cannot be used in some surrounding context. For example, if t is a record (or, more generally, an object), then we can use an up-cast to hide some of its fields (methods).

A down-cast, on the other hand, allows us to assign types to terms that the typechecker cannot derive statically. To allow down-casts, we make a somewhat surprising change to the typing rule for as:

That is, we check that t₁ is well typed (i.e., that it has some type S) and then assign it type T, without making any demand about the relation between S and T. For example, using down-casting we can write a function f that takes any argument whatsoever, casts it down to a record with an a field containing a number, and returns this number:

   f = λ(x:Top) (x as {a:Nat}).a;

In effect, the programmer is saying to the typechecker, "I know (for reasons that are too complex to explain in terms of the typing rules) that f will always be applied to record arguments with numeric a fields; I want you to trust me on this one."

Of course, blindly trusting such assertions will have a disastrous effect on the safety of our language: if the programmer somehow makes a mistake and applies f to a record that does not contain an a field, the results might (depending on the details of the compiler) be completely arbitrary! Instead, our motto should be "trust, but verify." At compile time, the typechecker simply accepts the type given in the down-cast. However, it inserts a check that, at run time, will verify that the actual value does indeed have the type claimed. In other words, the evaluation rule for ascriptions should not just discard the annotation, as our original evaluation rule for ascriptions did,

but should first compare the actual (run-time) type of the value with the declared type:

For example, if we apply the function f above to the argument {a=5,b=true}, then this rule will check (successfully) that ⊢ {a=5,b=true} : {a:Nat}. On the other hand, if we apply f to {b=true}, then the E-DOWNCAST rule will not apply and evaluation will get stuck at this point. This run-time check recovers the type preservation property.

15.5.1 Exercise [⋆⋆ ↛]

Prove this.

Of course, we lose progress, since a well-typed program can certainly get stuck by attempting to evaluate a bad down-cast. Languages that provide down-casts normally address this in one of two ways: either by making a failed down-cast raise a dynamic exception that can be caught and handled by the program (cf. Chapter 14) or else by replacing the down-cast operator by a form of dynamic type test:

Uses of down-casts are actually quite common in languages like Java. In particular, down-casts support a kind of "poor-man's polymorphism." For example, "collection classes" such as Set and List are monomorphic in Java: instead of providing a type List T (lists containing elements of type T) for every type T, Java provides just List, the type of lists whose elements belong to the maximal type Object. Since Object is a supertype of every other type of objects in Java, this means that lists may actually contain anything at all: when we want to add an element to a list, we simply use subsumption to promote its type to Object. However, when we take an element out of a list, all the typechecker knows about it is that it has type Object. This type does not warrant calling most of the methods of the object, since the type Object mentions only a few very generic methods for printing and such, which are shared by all Java objects. In order to do anything useful with it, we must first downcast it to some expected type T.

It has been argued-for example, by the designers of Pizza (Odersky and Wadler, 1997), GJ (Bracha, Odersky, Stoutamire, and Wadler, 1998), PolyJ (Myers, Bank, and Liskov, 1997), and NextGen (Cartwright and Steele, 1998)-that it is better to extend the Java type system with real polymorphism (cf. Chapter 23), which is both safer and more efficient than the down-cast idiom, requiring no run-time tests. On the other hand, such extensions add significant complexity to an already-large language, interacting with many other features of the language and type system (see Igarashi, Pierce, and Wadler, 1999, Igarashi, Pierce, and Wadler, 2001, for example); this fact supports a view that the down-cast idiom offers a reasonable pragmatic compromise between safety and complexity.

Down-casts also play a critical role in Java's facilities for reflection. Using reflection, the programmer can tell the Java run-time system to dynamically load a bytecode file and create an instance of some class that it contains. Clearly, there is no way that the typechecker can statically predict the shape of the class that will be loaded at this point (the bytecode file can be obtained on demand from across the net, for example), so the best it can do is to assign the maximal type Object to the newly created instance. Again, in order to do anything useful, we must downcast the new object to some expected type T, handle the run-time exception that may result if the class provided by the bytecode file does not actually match this type, and then go ahead and use it with type T.

To close the discussion of down-casts, a note about implementation is in order. It seems, from the rules we have given, that including down-casts to a language involves adding all the machinery for typechecking to the run-time system. Worse, since values are typically represented differently at run time than inside the compiler (in particular, functions are compiled into byte-codes or native machine instructions), it appears that we will need to write a different typechecker for calculating the types needed in dynamic checks. To avoid this, real languages combine down-casts with type tags-single-word tags (similar in some ways to ML's datatype constructors and the variant tags in §11.10) that capture a run-time "residue" of compile-time types and that are sufficient to perform dynamic subtype tests. Chapter 19 develops one instance of this mechanism in detail.

Variants

The subtyping rules for variants (cf. §11.10) are nearly identical to the ones for records; the only difference is that the width rule S-VARIANTWIDTH allows new variants to be added, not dropped, when moving from a subtype to a supertype. The intuition is that a tagged expression <l=t> belongs to a variant type <l_i:T_i^iÎ1..n> if its label l is one of the possible labels {T_i} listed in the type; adding more labels to this set decreases the information it gives us about its elements. A singleton variant type <l₁ :T₁> tells us precisely what label its elements are tagged with; a two-variant type <l₁ : T₁ , l₂ :T₂> tells us that its elements have either label l₁ or label l₂, etc. Conversely, when we use variant values, it is always in the context of a case statement, which must have one branch for each variant listed by the type-listing more variants just means forcing case statements to include some unnecessary extra branches.

Figure 15-5: Variants and Subtyping

Another consequence of combining subtyping and variants is that we can drop the annotation from the tagging construct, writing just <l=t> instead of <l=t> as <l_i :T_i^iÎ1..n>, as we did in §11.10, and changing the typing rule for tagging so that it assigns <l₁=t₁> the precise type <l₁ :T₁>. We can then use subsumption plus S-VARIANTWIDTH to obtain any larger variant type.

Lists

We have seen a number of examples of covariant type constructors (records and variants, as well as function types, on their right-hand sides) and one contravariant constructor (arrow, on the left-hand side). The List constructor is also covariant: if we have a list whose elements have type S₁, and S₁ <: T₁, then we can safely regard our list as having elements of type T₁.

References

Not all type constructors are covariant or contravariant. The Ref constructor, for example, must be taken to be invariant in order to preserve type safety.

For Ref S₁ to be a subtype of Ref T₁, we demand that S₁ and T₁ be equivalent under the subtype relation-each a subtype of the other. This gives us the flexibility to reorder the fields of records under a Ref constructor-for example, Ref {a:Bool,b:Nat} <: Ref {b:Nat,a:Bool}-but nothing more.

The reason for this very restrictive subtyping rule is that a value of type Ref T₁ can be used in a given context in two different ways: for both reading (!) and writing (:=). When it is used for reading, the context expects to obtain a value of type T₁, so if the reference actually yields a value of type S₁ then we need S₁ <: T₁ to avoid violating the context's expectations. On the other hand, if the same reference cell is used for writing, then the new value provided by the context will have type T₁. If the actual type of the reference is Ref S₁, then someone else may later read this value and use it as an S₁; this will be safe only if T₁ <: S₁.

15.5.2 Exercise [⋆ ↛]

(1) Write a short program that will fail with a run-time type error (i.e., its evaluation will get stuck) if the first premise of S-REF is dropped. (2) Write another program that will fail if the second premise is dropped.

Arrays

Clearly, the motivations behind the invariant subtyping rule for references also apply to arrays, since the operations on arrays include forms of both dereferencing and assignment.

Interestingly, Java actually permits covariant subtyping of arrays:

(in Java syntax, S₁[] <: T₁ []). This feature was originally introduced to compensate for the lack of parametric polymorphism in the typing of some basic operations such as copying parts of arrays, but is now generally considered a flaw in the language design, since it seriously affects the performance of programs involving arrays. The reason is that the unsound subtyping rule must be compensated with a run-time check on every assignment to any array, to make sure the value being written belongs to (a subtype of) the actual type of the elements of the array.

15.5.3 Exercise [⋆⋆⋆ ↛]

Write a short Java program involving arrays that type-checks but fails (by raising an ArrayStoreException) at run time.

References Again

A more refined analysis of references, first explored by Reynolds in the language Forsythe (1988), can be obtained by introducing two new type constructors, Source and Sink. Intuitively, Source T is thought of as a capability to read values of type T from a cell (but which does not permit assignment), while Sink T is a capability to write to a cell. Ref T is a combination of these two capabilities, giving permission both to read and to write.

The typing rules for dereferencing and assignment (Figure 13-1) are modified so that they demand only the appropriate capability.

Now, if we have only the capability to read values from a cell and if these values are guaranteed to have type S₁, then it is safe to "downgrade" this to a capability to read values of type T₁, as long as S₁ is a subtype of T₁. That is, the Source constructor is covariant.

Conversely, a capability to write values of type S₁ to a given cell can be downgraded to a capability to write values of some smaller type T₁: the Sink constructor is contravariant.

Finally, we express the intuition that Ref T₁ is a combination of read and write capabilities by two subtyping rules that permit a Ref to be downgraded to either a Source or a Sink.

Channels

The same intuitions (and identical subtyping rules) form the basis for the treatment of channel types in recent concurrent programming languages such as Pict (Pierce and Turner, 2000; Pierce and Sangiorgi, 1993). The key observation is that, from the point of view of typing, a communication channel behaves exactly like a reference cell: it can be used for both reading and writing, and, since it is difficult to determine statically which reads correspond to which writes, the only simple way to ensure type safety is to require that all the values passed along the channel must belong to the same type. Now, if we pass someone only the capability to write to a given channel, then it is safe for them to pass this capability to someone else who promises to write values of a smaller type-the "output channel" type constructor is contravariant. Similarly, if we pass just the capability to read from a channel, then this capability can safely be downgraded to a capability for reading values of any larger type-the "input channel" constructor is covariant.

Base Types

In a full-blown language with a rich set of base types, it is often convenient to introduce primitive subtype relations among these types. For example, in many languages the boolean values true and false are actually represented by the numbers 1 and 0. We can, if we like, expose this fact to the programmer by introducing a subtyping axiom Bool <: Nat. Now we can write compact expressions like 5*b instead of if b then 5 else 0.

^[3]Most of the extensions discussed in this section are not implemented in the fullsub checker.

< Free Open Study >