Add Me!Close Menu Navigation

Subtype Ambiguity in Java

Let’s take a look at an example of a situation where ambiguity occurs during the derivation of subtyping proofs in Java. In general, it’s conjectured that subtyping in Java is undecidable.

true ? 1 : "Hello"

Take a look at the Java expression on the left hand side. Off of the top of your head, can you tell me if it will type check? If so what will be its type?

If you had asked me this question out of the blue, I would have probably said no; I would reason it as follows: this is a Java expression, so it must be assigned a type, meaning that we’re giving a system of equations saying that the type of 1 and the type of "Hello" must be equal; this is clearly not the case as one is an Integer and the other a String, so this can’t possibly type check!

Of course, I’m actually just suffering from a common case of overlooking the obvious. It turns out that I’m forgetting about the whole subtyping thing built into Java and that I can actually assign Object o = true ? 1 : "Hello";, because the type Object sits at the \top of the type ordering.

1. Subtyping as Inequalities

Since we’re speaking of subtyping as a type relation anyways, let’s give it a symbolic name to make it easier for us: we’ll let T and S range over types in Java, and we’ll say

    \[S \le T\]

to mean that S is a subtype of T. Under one interpretation, we can think of this as saying that if we’re expecting a T somewhere, we should theoretically be allowed to plug in a S in its place and not expect weird or undefined behaviors as a result. Another perhaps more practical view is to claim that there exists some function called the coercion function (which we will denote, for the sake of historical consistency, \Theta) that, given some subtype relation S \le T, will be able to translate an object of type S into an object of type T that behaves “similarly”.

Anyways, It’s obvious that both \g{Integer} \le \g{Object} and \g{String} \le \g{Object} (since everything’s a subtype of Object), so we can draw a subtyping hierarchy as a tree:

Rendered by QuickLaTeX.com

and we can type check true?1:"Hello" : Object. This seems to suggest that we can typecheck all instances of (b?x:y) to some type R if we can typecheck x to S, y to T, and S,T \le R. In otherwords, R is an upper bound of the types of x and y.

Of course, upon closer inspection, it turns out that both Integer and String share another common supertype: Serializable.

Rendered by QuickLaTeX.com

So just as well, we could claim that the ternary expression above extends Serializable. But if we want to “assign” a type to an expression, we don’t just want its supertypes.

2. Most Precise Supertype

Looking at the type hierarchy above, it’s clear that the lower a type is on that hierarchy, the more “precise” it is. When we say that an expression has a type, we don’t mean that it is bounded above by some set of super types; we actually mean that its most “precise” type is so and so. For example, we could just as well draw the type hierarchy for Integers as

Rendered by QuickLaTeX.com

and claim that a 1 is a Serializable; but when I typically talk about the type of the expression 1, I’m usually talking about Integer, not Serializable.

From this, it’s clear that we also want a way to find the most precise (smallest) type of true ? 1 : "Hello" such that it is also an upper bound of both 1 and “Hello”; this is called the least upper bound, and we will for historical reasons call this the “join” of two types.

Symbolically, if we want to find the most precise upperbound (join) type of two types S and T, we will denote it as R such that

    \[R = S \sqcup T\]

the reason that the least upper bound is usually denoted as a square union symbol is actually somewhat natural: the union of two sets is the least upper bound of those two sets in the partial order \subseteq (set inclusion), convince yourself that this is actually the case.

Note that whenever we join two types, the resulting type is “less precise”. We are after all finding an upper bound!

Going back to the problem at hand, the entire point of this exercise is then very simple: we want to find the least upper bound of Integer and String:

    \[\g{Integer} \sqcup \g{String}\]

We’ve already seen earlier that both Object and Serializable are upper bounds of both Integer and String, but we also know that \g{Serializable} \le \g{Object}, so Serializable is a more precise (less) upper bound than Object is, but is Serializable the most precise?

In order to answer this question and find the least upper bound, we’re going to need the complete subtyping hierarchy. Consulting the Java documentation, we find that Integer is a subtype of Numbers, which are Serializable, and are themselves Comparable with other Integers. Furthermore, Strings are also Serializable and Comparable with other Strings! This gives the slightly more convoluted typing hierarchy:

Rendered by QuickLaTeX.com

3. Problems

At first first glance, it doesn’t seem possible that there’s a least upper bound: it seems like both Comparable and Serializable are the most precise upper bounds. Furthermore, this isn’t even necessarily true as Comparable itself might be too imprecise.

Wildcards and Bounded Quantifiers

Consider the constraint

    \[\g{String} \sqcup \g{Integer} \le \g{Comparable}\ba{?}\]

now, we know that

    \[\g{String} \le \g{Comparable}\ba{\g{String}}, \g{Integer} \le \g{Comparable}\ba{\g{Integer}}\]

so we can rewrite this as

    \[\g{String} \le \g{Comparable}\ba{?~\g{extends}~\g{Comparable}\ba{?}}\]

by plugging in \g{String} \le \g{Comparable}\ba{?} into the \g{String} in \g{Comparable}\ba{\g{String}}. (Wildcards, amiright?) Similarly, we can say the same about integers, so we get

    \[\g{String} \sqcup \g{Integer} \le \g{Comparable}\ba{?~\g{extends}~\g{Comparable}\ba{?}}\]

but we \g{Comparable}\ba{?~\g{extends}~\g{Comparable}\ba{?}} \le \g{Comparable}\ba{?}, so a more precise upper bound of \g{String}\sqcup \g{Integer} is \g{Comparable}\ba{?~\g{extends}~\g{Comparable}\ba{?}}. But now, we can construct a sequence

    \[\g{Comparable}\ba{?},\]

    \[\g{Comparable}\ba{?~\g{extends}~\g{Comparable}\ba{?}},\]

    \[\g{Comparable}\ba{?~\g{extends}~\g{Comparable}\ba{?~\g{extends}~\g{Comparable}\ba{?}}},\]

    \[\vdots\]

each of which a more precise approximation than the previous, which undoubtedly converges to the most precise type: and here’s the kicker, that type cannot be expressed finitely!

So how does Java handle these types? Let’s try it out. I wanted Java to output the internal type representation, so I need to get a type-mismatch error during compile time.

Comparable Type

It seems as if Java is reporting the type of the two as an unbounded quantification: just Comparable<?>. This is intentional, Java treats the ? extends ... as a constraint (or a system of inequalities) and discards them during type checking and coercion in order to use them later solely for typechecking, so we seemed to have for now solved the problem (So even though A\ba{?~\g{extends}~\g{A}\ba{?}} \le A\ba{?}, we’re going to treat them as if they weren’t).

No least upper bound?

But we still have another problem, there’s is no least upper bound in the above hierarchy! Again, let’s see what Java does:

Intersection Type

It turns out that the least upper bound is just the “intersection” over the three types, which should then be the LEAST upper-bound of all three.

Posted By Lee

Woosh