Associative, commutative, Java-friendly intersection erasure #11808
Conversation
smarter
force-pushed
the
new-intersection-erasure
branch
2 times, most recently
from
423e2f9 to
0552add
Compare
|
does this affect forward compat from Scala 2.13? |
|
Yes, though this isn't new since Scala 3 intersection erasure rules have never exactly matched Scala 2 erasure rules, hence the need for #11603. More precisely you'll probably need to add a Scala3ErasureMap with an override of mergeParents that reimplements erasedGlb: https://github.com/scala/scala/blob/8a2cf63ee5bad8c8c054f76464de0e10226516a0/src/reflect/scala/reflect/internal/transform/Erasure.scala#L297-L314 |
|
Also you'll want to reuse the testcases from sbt-dotty/sbt-test/scala2-compat/erasure |
brilliant, thank you |
smarter
force-pushed
the
new-intersection-erasure
branch
2 times, most recently
from
60ccab5 to
f990f56
Compare
smarter
force-pushed
the
new-intersection-erasure
branch
from
f990f56 to
5717548
Compare
| * - Java compatibility: intersections that would be valid in Java code are | ||
| * erased like javac would erase them (a Java intersection is composed of | ||
| * exactly one class and one or more interfaces and always erases to the | ||
| * class). |
There was a problem hiding this comment.
In our last discussion, hadn't we come to the conclusion that we should never return an Interface as the erasure of an intersection type (unless an interface dominates everything else, of course)? IIRC the issue was that Object & T1 & T2 would otherwise have a different erasure than T1 & T2, even though Object & T1 & T2 can simplify to T1 & T2 and though Java would erase to Object.
There was a problem hiding this comment.
In our last discussion, hadn't we come to the conclusion that we should never return an Interface as the erasure of an intersection type
Yes, I went with this version originally but decided it wasn't worth it in the end:
- Many more types end up being erased to Object which can lead to overloading clashes (it happened in the community build for example), I fear this could be a big problem in the wild making cross-compilation difficult.
- Admittedly, the fact that
Object & T1 & T2has a different erasure thanT1 & T2isn't great, but then so is the fact
Object & T1has a different erasure thanT1. - It turns out that intersection of traits in Java signatures actually work.
- Having erasedGlb(A, B) always return either A or B allows us to implement it as the minimum of a total order, which gives us commutativity and associativity for free and in general makes it easier to reason about what this method does.
There was a problem hiding this comment.
I see. IIUC, this is the critical aspect that allows this approach to work at all:
It turns out that intersection of traits in Java signatures actually work.
There was a problem hiding this comment.
It's helpful, but if those Java signatures weren't allowed, we could also emit a signature containing just the first trait as an approximation, we already have to use approximated signatures in various situations where our type system is more expressive than Java's.
| // is composed of multiple traits. But in practice Scala 2 has always | ||
| // ignored this restriction as intersections of traits seem to be handled | ||
| // correctly by javac, we do the same here since type soundness seems | ||
| // more important than adhering to the spec. |
There was a problem hiding this comment.
This wouldn't be a problem at all if our intersection erasure was only a trait when that trait dominates the intersection.
There was a problem hiding this comment.
This is true, but I don't think that's a good enough reason to use that scheme as outlined in my other comment.
| * - real classes over traits | ||
| * | ||
| * This operation has the following the properties: | ||
| * - Associativity and commutativity, because this method act as the minimum |
There was a problem hiding this comment.
| * - Associativity and commutativity, because this method act as the minimum | |
| * - Associativity and commutativity, because this method acts as the minimum |
| * - subtypes <= supertypes | ||
| * | ||
| * Additionally, lexicographic ordering of the class symbol full name is used | ||
| * as a tie-breaker so `A <= B && B <= A` iff `A =:= B`. |
There was a problem hiding this comment.
I don't understand what the formula after "so" has to do with the comment.
There was a problem hiding this comment.
If we did not have this tie-breaker, A <= B && B <= A would also be true when A and B are two unrelated traits, so we couldn't conclude that A =:= B, I can make this more explicit in the comment.
Thanks to scala#11603, we can now freely decide how we erase our intersection types without compromising compatibility with Scala 2. We take advantage of this by designing a new erasedGlb algorithm which respects associativity and commutativity and can also erase Java intersections without any special case. Incidentally, this lets us reverse a recent change in scala-stm which was previously required due to two equivalent types ending up with different signatures. This commit also improves the way we handle intersections in Java generic signature to produce more precise types when possible and to ensure that we never emit a type that would lead to javac emitting invalid bytecode (which can happen with Scala 2: scala/bug#12300). Fixes scala#5139.
smarter
force-pushed
the
new-intersection-erasure
branch
from
5717548 to
9af4bad
Compare
When I implemented our erasure algorithm in scala#11808, I misread https://docs.oracle.com/javase/specs/jls/se8/html/jls-4.html#jls-4.4 and incorrectly thought that a Java intersection had to contain at least one class, and since we always erase a Scala 3 intersection containing a class to that class, I thought we could use the Scala 3 intersection algorithm to erase Java intersections. But my assumption was incorrect: a Java intersection can in fact contain only interfaces, so we need to special-case them in erasure like before. Fixes scala#12586.
Thanks to #11603, we can now freely decide how we erase our intersection
types without compromising compatibility with Scala 2. We take advantage
of this by designing a new erasedGlb algorithm which respects
associativity and commutativity and can also erase Java intersections
without any special case.
This commit also improves the way we handle intersections in Java
generic signature to produce more precise types when possible and to
ensure that we never emit a type that would lead to javac emitting
invalid bytecode (which can happen with Scala 2:
scala/bug#12300).
Fixes #5139.