In Scala, this had led to the creation of the DOT calculus, in a project known as Dotty. A little over a year ago, DOT was proven to be sound.
woah, thanks for those, that’s super interesting.
why is this anything more than a bug report against Java? is there some irreparable design flaw in the language spec that is behind this that we should be aware of?
I’ve not read this thoroughly, but often these sorts of unsoundness concerns are not solvable by a patch in the language but instead are a result of how whole language features combine in unsavory ways. Either the features need to be massaged (which is unlikely to retain backward compatibility) or their use together outlawed (same).
That said, sometimes it is just a bug.
I haven’t fully grokked the paper yet, but from what I understand, a key part of the problem is that the value null is a member of every type. I’m not sure if that prevents the type system from being sound fundamentally, but it is called out as a design choice which causes problems at the type level. I hadn’t previously considered or heard about that as a drawback for implicit null values, so that’s been the most interesting take-away from the paper for me so far.
ah! on mobile I didn’t see a link to the paper, just the code. will definitely have to peruse it.
The paper goes into detail. Looks like one thing it points out is that the PL community (which the authors are a part of) should try to improve methods to find these sorts of problems, because although there is a formalism for a subset of Java that has been extended and whose type system has been proved sound, the fact that this subset didn’t include null pointers allowed people to miss this problem.
It’s more than a bug report because bugs can be fixed, whereas mathematical unsoundness suggests that fixing one issue will create another. With typical bugs, finding the cause is hard but fixing the problem is easy. When there’s a design flaw or, worse, a deep logical error, you often can’t fix it without re-writing a number of components from scratch– which, when you’re talking about a language with thousands or millions of users, is virtually impossible.
That said, we’ve known for a long time that Scala’s type system was “broken” in ways that angered theoreticians but didn’t seem to slow adoption. It isn’t news that Java or Scala have severe design flaws, but those don’t prevent people from gainfully putting these languages into production.
Scala is a useful language for the present time, because it’s a hell of a lot easier to use (as a writer of new code, at least) than Java, but I have doubts about its future (and, in the longer term, Java’s). It’s extremely complex and it has a lot of features that don’t play well together.
Don Syme wrote his thesis on finding an “unsoundness” in the Java type system back in the 90’s. I can’t seem to find his thesis right now, but this paper, “Proving Java Type Soundness” is based on that work https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/java.pdf
It was timely research. Microsoft was looking to create a Java alternative, and Don went on to work on .NET generics and become the creator of F#.