Formal definition of compatible types in Java (soundness)

Question

I was trying to find the algorithmic definition of convertible (and thus inconvertible) types in Java.

In my opinion a CORRECT compiler should block at compile-time explicit and implicit castings between expressions having inconvertible static types, whatever the definition of inconvertible would be.

On the other hand, since it would be nice if each reference had a dynamic type which is a subtype of its static type, in order to prevent ClassCastExceptions at run-time, the compiler should always block castings between types that have no common subtypes.

A candidate definition that makes sense to me is be the following:

1. Two classes A and B are convertible iff either A is a subtype of B or B is a subtype of A
2. An interface I and a class C are convertible iff either C implements I or I and C have a common subtype (a class that implements I and extends C, possibly in an indirect way)
3. Two interfaces I1 and I2 are convertible iff they have a common subtype (a class or another interface)

However the following snippets do NOT give compilation errors (only warnings for example in IntelliJIDEA):

interface A {}
class B {}

class Test {

  public static void main(String[] args) {
    B b  = new B();
    A a = (A)b;    // this casting will produce a run-time error
  }
}

interface M {}
interface N {}
class A implements M {}
class B extends A {}
class C extends A implements N {}

class Test {

  public static void main(String[] args) {
    N x = new C();
    M y = (B)x;   // this casting will produce a run-time error
  }
}

interface M {}
class A implements N{}
interface N {}

class Test {

  public static void main(String[] args) {
    N x = new A();
    M y = (M)x;   // this casting will produce a run-time error
  }
}

In conclusion I want to understand if there is an official definition of (in)convertible types in the Java specs, and whether it has been correctly implemented in the existing compilers.

Answer 1

The question you're asking is about the soundness of the java type system (here's a nice intro on the topic).

There's no formal definition in the case of java, but a number of reconstructions do exist, arriving at statements like "We were surprised by the subtlety and the non-uniformity of the language semantics, especially since its description is rather colossal, ambiguous, and erroneous." with a tendency to consider it by and large sound, apart from obvious glitches.

Obvious glitches stem from backwards compatibility issues, e.g. with typed collections that were put on top of untyped collections, and always can be undermined by operations taking the untyped way. The issue of casting the OP dwells upon may be yet another flavor of the issue, since what should one think of char c = (char)1024;?

On the other hand fundamental inconsistencies have been unearthed as well, more on the level of "parametrically polymorphic functions that can turn any type into any type without (down)casting". Find a discussion about what's fundamental and what's a glitch here, also hinting at discrepancies between the language spec and the compiler.

It may be interesting to note, that the argument is also valid for the Scala language up to version 2.x, and perhaps any other industry scale OO-language, only the upcoming Scala 3 gets provably rid of them. An effort that took the contributors almost a decade and is supposed to be a novelty in the realm of object oriented languages.