Breaking Dotty (Scala 3) and Java 16 Decidability

May 03, 2021

Breaking Dotty (Scala 3) and Java 16 Decidability

As I was preparing my talk for the upcoming IFIP WG 2.4, I reflected on trying to explain the foundational work done by my recently graduated PhD student Julian Mackay as published in our POPL 2020 paper and APLAS 2020 paper) last year.

For this example, I used the latest release of Dotty (a.k.a. Scala 3) and the latest release of Java 16:

Imagine you want to have an interface or trait allowing you to compare items called Eq with parameter E. Here is both Java and Scala code alongside each other:

Now imagine a Set that insists on containing the elements that are comparable with other Set instances using Eq and themselves contain elements that are comparable with Eq with both Java and Scala code alongside each other as follows:

Finally, lets create a useful class Tree that implements such Set:

If you are to ask either Dotty or Java a simple looking question: "is Tree a subtype of Eq<? super Tree> in Java or a subtype of Eq {type E >: Tree} in Scala?", they will both literally get their knickers in a twist and explode. Try it!

What is going on here? Why? And how can one write tools that work with such poor compilers or rely on a simple subtyping check to actually be helpful to confuse the Beetlejuice out of a poor programmer!

The answer is in a very simple loop caused by the contra-variance in our subtyping between type parameters (in Java) or type members (in Scala).

In fact, after 6 years of beers, Julian found no less than 3 ways to solve it with minimal impact on the programmers with a very easy to understand syntactic restriction proposed for any language with bounded polymorphism that is simple to check and reason about and still supports transitivity, intersection, and union types as some of the non-trivial subtyping requirements. If you want to know more - get in touch for a more in depth discussion!