Skip to content

Intersection types are not commutative for overriding and overloading #5139

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
panacekcz opened this issue Sep 21, 2018 · 15 comments · Fixed by #11808
Closed

Intersection types are not commutative for overriding and overloading #5139

panacekcz opened this issue Sep 21, 2018 · 15 comments · Fixed by #11808
Assignees
Milestone

Comments

@panacekcz
Copy link
Contributor

Although A & B and B & A are claimed to be the same type, the are not the same for overriding and overloading.
It seems to be "caused" by erasue, which erases A & B to A and B & A to B.

Overriding

trait A
trait B

class Base{
  def m(ab: A&B) = ab
}
class Derived extends Base{
  override def m(ab: B&A) = ab // unexpected error
}

Output:

8 |  override def m(ab: B&A) = ab // unexpected error
  |               ^
  |       error overriding method m in class Base of type (ab: A & B): A & B;
  |         method m of type (ab: B & A): A & B has incompatible type

On the other hand, if the override is omitted, an error is correctly issued.

class Derived2 extends Base{
  def m(ab: B&A)=ab // OK - "needs override" error when expected
}

Also, when the first type in the intersection is the same (therefore erased type is the same), overriding works as expected:

trait C
class Base3{
  def m(abc: A&B&C) = abc
}
class Derived3 extends Base3{
  override def m(abc: A&C&B) = abc // OK - no error
}

Overloading

Similarly, overloading is allowed when the first type differs.

class Overload{
  def m(ab: A&B) = ab
  def m(ab: B&A) = ab // No error when expected
}

On the other hand, such methods cannot be called, as expected:

object Caller{
  Overload.m(new A with B) // OK - "ambiguous overload" error when expected
}

That seems to be the same behavior as with scalac.

@sjrd
Copy link
Member

sjrd commented Sep 21, 2018

I think I suggested at some point that erasure should choose deterministically, for example by:

  • prefer class over trait (for performance reasons)
  • tie break: lexicographically first class/trait name

@panacekcz
Copy link
Contributor Author

Using lexicographical order of names would mean that code could break when you rename a trait even if its name is not mentioned anywhere, like

trait B
trait A { // Rename A to C
 def m(a:B&this.type) = 1
 def m(a:B) = 2 // Ok in A, conflict in C
}

That seems brittle. You would also give up any programmer control over the erasure for a quite arbitrary rule.

Would it be reasonable to just put the current behavior into the specification? You'd have to weaken the claim that A & B is the same type as B & A, and say something like & is commutative except for erasure and its consequences.

@sjrd
Copy link
Member

sjrd commented Sep 25, 2018

and say something like & is commutative except for erasure and its consequences.

That is even more brittle, because the compiler can and might change the order of an & internally for arbitrary reasons.

At least my proposal is specifiable.

@smarter
Copy link
Member

smarter commented Sep 25, 2018

FWIW, the rules for erasure of & are at https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeErasure.scala#L299 and the rules for | are at https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeErasure.scala#L244

The lexicographic tie break makes sense to me, but it doesn't match what scalac is doing (we already don't always match what scalac is doing, but I was hoping we could fix that: #4619 for example), which can lead to issues when using scalac-compiled libraries.
It could also break code that abuses how erasure works to implement tagged type by assuming that Int & AMarkerTrait erases to Integer and not AMarkerTrait (I think scalaz used to do this but may have gone with something saner since then).

@smarter
Copy link
Member

smarter commented Sep 25, 2018

We could potentially have different erasure rules for symbols that are Scala2-defined or override something that is Scala2-defined, but that seems rather involved.

@odersky
Copy link
Contributor

odersky commented Oct 1, 2018

Why would the current behavior not be specifiable? It seems we need to take erasure into account only for types that are written down. Those won't be re-arranged by the compiler. Going lexicographic has the mentioned disadvantages wrt renaming and Scala-2 interop.

@odersky
Copy link
Contributor

odersky commented Oct 2, 2018

The error messages given in the issue are confusing. They stem from the fact that methods are classified according to their signature, which is essentially a string representation of their erased type. Since the erasure of A & B and B & A is not the same, the methods are classified as different, so can't override each other. The compiler could double-check in this case and issue a more specific error message saying that the erased types of the methods differ.

@odersky
Copy link
Contributor

odersky commented Oct 2, 2018

Another TODO: Be more precise about what we mean in

Unlike with types, & is commutative: A & B is the same type as B & A.

Something like:

& is commutative: A & B and B & A are equivalent types, in the sense that each is a subtype of the other.

The issue with with types is not that they were not commutative (they were treated as such) it was that the commutative law for with types did not respect the Liskov substitution principle. But that's a bit much to explain in a tutorial page.

@sjrd
Copy link
Member

sjrd commented Oct 2, 2018

It seems we need to take erasure into account only for types that are written down.

No, you need to take erasure of the result type of a method into account, and that can be an inferred/lub'ed type. For example, what's the erasure of the following method?

def foo(x: Int) =
  if (x > 0) (??? : (A & B))
  else (??? : (B & A))

The spec won't say anything regarding whether A & B or B & A will be chosen as the result of the if/else, and yet that will be the result type of foo.

@odersky
Copy link
Contributor

odersky commented Oct 7, 2018

@sjrd Why does erasure matter for result types? ... and what does scalac do in this case?

@sjrd
Copy link
Member

sjrd commented Oct 7, 2018

Result types are part of a JVM method signature. foo(String)String is a different method than foo(String)List. So they're important for erasure. If foo above erases to foo(int)A in one case but foo(int)B in another case, they won't be compatible. That's also why we need bridges for covariant result types (and javac does too).

scalac appears to select the one coming from the then branch, but I would bet it's pure accident.

@abgruszecki
Copy link
Contributor

@smarter Is this related to #4619?

@smarter
Copy link
Member

smarter commented Jan 5, 2021

It's a separate issue, dotty does not erase intersections like scala 2, and neither of them is commutative. The plan is to handle intersections coming from scala 2 specially, but we didn't reach a decision for this issue on whether we want to change the dotty-defined intersection type erasure to be commutative (which would be nice indeed).

@smarter smarter added this to the 3.0.0-RC1 milestone Jan 5, 2021
@anatoliykmetyuk anatoliykmetyuk modified the milestones: 3.0.0-RC1, 3.0.0-RC2 Feb 11, 2021
@smarter smarter self-assigned this Mar 15, 2021
smarter added a commit to dotty-staging/dotty that referenced this issue Mar 18, 2021
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.

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 added a commit to dotty-staging/dotty that referenced this issue Mar 18, 2021
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.

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 added a commit to dotty-staging/dotty that referenced this issue Mar 20, 2021
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.
@nafg
Copy link

nafg commented Mar 21, 2021

What about using the LUB? Worst case the JVM sees it as returning Object. I assume Scala will still see it as the correct type either way.

smarter added a commit to dotty-staging/dotty that referenced this issue Mar 21, 2021
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
Copy link
Member

smarter commented Mar 21, 2021

Some problems with using the lub:

In any case, I've already opened #11808 to fix this issue which I believe is optimal.

smarter added a commit to dotty-staging/dotty that referenced this issue Mar 21, 2021
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 added a commit to dotty-staging/dotty that referenced this issue Mar 22, 2021
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.
michelou pushed a commit to michelou/scala3 that referenced this issue Mar 22, 2021
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.
michelou pushed a commit to michelou/scala3 that referenced this issue Mar 22, 2021
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.
@Kordyjan Kordyjan modified the milestones: 3.0.0-RC2, 3.0.0 Aug 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

8 participants