Subtyping and Polymorphism

Submitted by mrd on Sun, 03/02/2008 - 9:54pm.

I am addressing an article written by Mark Dominus named Subtypes and polymorphism:

There are two parts to this article, the first discusses the fact that subtyping and polymorphism can lead to some unintuitive results. I won't repeat his point here, but just note that the term for the behavior of "List" here is called "invariant" and the incorrect behavior which he had assumed is called "covariant."

Java's broken arrays

While Java generic Lists are "invariant," Java arrays are "covariant." This is not due to some wonderful property of arrays, but in fact is a gigantic flaw in the Java language which breaks static type safety. As a result, arrays must carry run-time type information in order to dynamically check the type of objects being inserted. Consider this code:

String stringA[] = new String[1]; stringA[0] = "Hello"; Object objectA[] = stringA;

So far this seems okay -- String is a subtype of Object -- therefore it seems safe to say that String arrays are a subtype of Object arrays. This is called "covariant" behavior.

So if objectA is an array of Objects, and everything is a subtype of Object, then it should be okay to put an Integer there instead, right?

objectA[0] = 1;

but wait, now stringA[0] has an Integer in it! A String array cannot have an Integer in it. Before it seemed that arrays might be "covariant," but mutation makes it seem that arrays must be "contravariant." We can't be both at the same time, so it seems mutable arrays are "invariant" after all.

If you try running the code given above, you get:

Exception in thread "main" java.lang.ArrayStoreException: java.lang.Integer

clearly, a run-time type-check is being performed.

About Covariance, Contravariance, and Invariance

I've been using these terms, but haven't really defined them.

A type-constructor C is covariant iff: for all types S,T, if S is a subtype of T then C<S> is a subtype of C<T>.

Similarly, for contravariance, if S is a subtype of T then C<T> is a subtype of C<S>. Note that S and T have swapped.

Invariance (the name is confusing, I know) is the lack of covariance or contravariance.

It may be of interest to know that functions are contravariant in the input, but covariant in the output. Perhaps that is why the Java folks are not so eager to have function types!

Broken arrays and generics

The brokenness of Java arrays has impacted on the design of Java generics as well. Consider the following code that might be written if you were designing your own generic container of some sort:

public class Container<T> { private T[] a;

So far so good, right? An array of some parameterized type seems reasonable.

public Container() { a = (T[])new T[10]; } }

Uh oh!

Container.java:5: generic array creation a = (T[])new T[10]; ^ Note: Container.java uses unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. 1 error

No can do. Java is jumping down my throat over this seemingly reasonable code. Why? Generic arrays are not permitted like this, because -- as described above -- Java arrays must carry run-time type information. But Generics promise total type erasure -- meaning NO run-time type information is kept. Sounds like they designed themselves into a corner when creating Java, and later, Generics.

Polymorphism is not Subtyping

Returning to the second part of the article, I want to dispel a few common misperceptions about polymorphism.

Mark Dominus: Then we define a logical negation function, not, which has type bool → bool, that is, it takes a boolean argument and returns a boolean result. Since this is a subtype of α → α, we can store this function in the cell referenced by a.

I want to make it absolutely clear that bool → bool is not a subtype of α → α. There is no notion of subtyping in basic Hindley-Milner, and it is still not the case even in a "loose" sense.

The easiest way to verify this for yourself is to find your nearest Standard ML (or similar) prompt and type this:

not : 'a -> 'a

and get a type error. not : bool → bool and it is not of type α → α.

Now, his example does not typecheck in Standard ML because of the "value restriction." The value restriction does not exist to preserve type safety at all, but only to prevent programmer confusion.

This post has gone on too long about Java, so I am afraid it will wash out the more important points about polymorphism and the value restriction. I will leave it then, to the next post.