[moon_priestess]

> Java's type system is _sound_ as it guarantees that you will never use a variable of one type as another incompatible type.

Is it though? I always thought it was unsound due to, at a minimum, mutable covariant arrays. It's definitely possible to have a type error at runtime without using a cast.

[johncolanduoni]

I think they are referring to the fact that you will get a type error at runtime, instead of silently corrupting data or other undefined behavior.

[UncleMeat]

But the static type system is what is being evaluated here. This is like saying that python has a sound type system because the interpreter throws type errors when you fuck up.

[eveningcoffee]

Java allows this

  Integer a = 0;
  Object c = a;
  String b = (String) c;

This code compiles but produces a runtime exception. The problem is here that you are allowed to upcast and this is perfectly valid code and it is developers responsibility to verify that upcast is actually valid.

The problem with the code in the paper is that Java 1.5 introduced generic types, that are in principle meant easy such situations and it appears that there are some corner cases where it does not work as expected (to more general populace).

For example consider this code

  static class Upcast {
    static <T extends String> String cast(T t) {
      return t;
    }
  }

  Integer a = 0;
  Object c = a;   
  String b = Upcast.cast(c);

This code does not compile, as we explicitly stated that we want an type that extends the String. Writing the last

  String b = Upcast.cast((String)c);

will make the code compile, but it will produce a compiler warning and runtime exception.

The paper demonstrates a more complex indirection to avoid the compiler warning but still produce a runtime exception.