Comment by jhdevos | Hacker News Reader

Comment by jhdevos | Hacker News Reader

Parent Full thread

I don't see the headline as misleading at all. There are two type systems in Java: the JVM's run-time type system, and Java's compile time type system. It's the latter that has been shown to be unsound. As the paper notes, it's fortunate that generics have been implemented with type erasure, because that is what saves the JVM from being unsound, too.

As for the problem itself: it really has nothing to do with inner classes (they are static in the example!). The problem is with this line:

    Constrain<U,? super T> constrain = null;

which leads the type system to assume that there is a type that is a superclass of T, which also is a subclass of B (from the 'Constrain' class) - even though no such type could possibly exist! The evil trick is in the 'null' - even though a type with the stated constraints is impossible, and so no actual 'real' value of this generic type could exist, 'null' is part of all types, so the compiler can't see the problem.

It really is a problem in the type system as defined in the standard, not just a compiler bug.

Yes, it's all about nulls. I was curious to break it down from Curry-Howard correspondence (Types as Propositions) point of view. The line

  static class Constrain<A, B extends A> {}

reads as

  for all propositions A and B, such that B implies A, proposition Constrain<A, B> holds.

While, the line:

  Constrain<U,? super T> constrain = null;

kind of says:

  Admit that there exists type X, such that T implies X, for which Constrain<U, X> holds.

Even though no proof (read constructed instance) that X implies U is provided.

If we look at concrete execution instance with String and Integer:

String implies Object, Serializable, Comparable<String>, CharSequence. None of those imply/extend Integer, which is required for truthful Constrain<U, ? super T> proposition.

Basically, ex falso quodlibet :)

EDIT: spacing, formatting, wording.

Good point with the null, they have an example without the null keyword which is an even dirtier trick (because it is still null).

https://github.com/namin/unsound/blob/master/Nullless.java

Do you have a spec reference for that (not trying to be a dick - i just want to understand what the type system believes it should be doing here as the value being assigned to a reference should not influence the type system behaviour)

This is explained in the article in a bit more detail. The point is not that the type system does something with the actual value - the point is that it would be impossible to create any code that results in such a value (other than null), since then you would have to provide an actual type that is somewhere between Integer and String - and that would obviously not pass the type checking. Using null avoids that.

Section 4.5 in the language spec deals with parameterized types; 4.5.1 deals with wildcards. Of course, there is no example in the specs that clearly points out what happens in this example - otherwise this wouldn't have remained undiscovered for so many years :)

If you can show, using the rules in the spec, that the sample program shouldn't pass type checking, then you'll have proved the article wrong :-)

Reply on news.ycombinator.com