Skip to content
This repository has been archived by the owner on Dec 22, 2021. It is now read-only.

Support for Multiversal Equality #100

Closed
LPTK opened this issue Jun 6, 2017 · 17 comments
Closed

Support for Multiversal Equality #100

LPTK opened this issue Jun 6, 2017 · 17 comments

Comments

@LPTK
Copy link
Contributor

LPTK commented Jun 6, 2017

With multiversal equality in Dotty (scala/scala3#1247), it would seem inconsistent not to use it for operations based on == such as contains and indexOf, which are currently pretty unsafe:

scala> List(1,2) contains 'ko
val res3: Boolean = false

It has been agreed on before that these methods could benefit from M-E. Indeed, one can write things like:

scala> def contains[A,B](ls: List[A], b: B)(implicit eq: Eq[A,B]) = ls.exists(_ == b)
scala> contains(List(1,2), 'ko)
-- Error: <console>:5:2 --------------------------------------------
5 |  contains(List(1,2), 'ko)
  |                         ^
  |         Values of types Int^ and Symbol^ cannot be compared with == or !=

In order to make that work with current Scala, we could have a single Eq implicit available there so that contains would always work (as before).

One thing I noticed that may or may not be a problem is that adding a subtyping constraint to one of the type parameters makes the code type check again...

scala> def contains[A,B >: A](ls: List[A], b: B)(implicit eq: Eq[A,B]) = ls.exists(_ == b)
scala> contains(List(1,2), 'ko)
res0: Boolean = false
@Blaisorblade
Copy link

Blaisorblade commented Jun 7, 2017

One thing I noticed that may or may not be a problem is that adding a subtyping constraint to one of the type parameters makes the code type check again...

That appears to be intended, because an instance of B could be an A (see top post in scala/scala3#1247), but though it is unfortunate.

@Blaisorblade
Copy link

Blaisorblade commented Jun 7, 2017

I've done a few experiments about how to type methods like ++. Discussion on https://www.reddit.com/r/programming/comments/6elim6/announcing_dotty_012rc1_a_major_step
_towards/diigfus/ points out that such methods might require extra parameters. Indeed, if such methods don't rely on eqAny they must all take extra instances, and if they rely on eqAny I think they lose assurances.

The results might be affected by scala/scala3#2707.

EDIT: what's below are a few alternative experiments. I'm not sure how to summarize them because I'm not sure what's the best course of action 😢

//import dotty.DottyPredef.{eqAny => _, _} // makes a difference
//import scala.{Eq => _, _} //makes no difference.
object Main {
  def equal[S, T](s: S, t: T) = s == t // it seems this should fail without eqAny.

  def contravWitness[A, B >: A](e : Eq[A, B]): Eq[A, A] = e
  //def contravWitness[A, B >: A](e : Eq[A, B]): Eq[B, B] = e
  def contains[A,B >: A](ls: List[A], b: B)(implicit eq: Eq[A,B]) = ls.exists(_ == b)
}

class Cell1[+T : [T] => Eq[T, T]](val value: T) {
  def contains[U >: T : [U] => Eq[U, T]](that: U) = value == that
}

class Cell2[+T](val value: T)(implicit _e: Eq[T, T]) {
  def contains[U](that: U)(implicit eq: Eq[T, U]): Boolean =
    value == that
}

class Cell3[+T](val value: T)(implicit _e: Eq[T, T]) {
  def contains[U >: T](that: U) = value == that
  def append1[U >: T](u: U): Cell3[U] =
    new Cell3(u) //uses eqAny
  def append2[U >: T](u: U)(implicit eq: Eq[T, U]): Cell3[U] =
    new Cell3(u) //uses eqAny
}


class ListCell[+T](val values: List[T])(implicit _e: Eq[T, T]) {
  def contains0[U >: T](that: U): Boolean =
    values.map(new Cell3[T](_)).exists(_.contains(that))
  def contains[U](that: U)(implicit eq: Eq[T, U]): Boolean =
    values.map(new Cell2[T](_)).exists(_.contains(that))
  def append1[U >: T](u: U): ListCell[U] =
    new ListCell(values :+ u) //uses eqAny
  def append2[U >: T](u: U)(implicit eq: Eq[T, U]): ListCell[U] =
    new ListCell(values :+ u) //uses eqAny
  def append3[U >: T](u: U)(implicit eq: Eq[U, U]): ListCell[U] =
    new ListCell(values :+ u)
}

@LPTK
Copy link
Contributor Author

LPTK commented Jun 7, 2017

I don't understand why you want to put an implicit on the CellN class itself instead of on the method. Any particular reasons?

As for classes such as Set and Map which implementations are based on equality internally, I don't think they need an implicit at all. It is understood that when you make a Set[A], the equals and hashCode of A are going to be used, and I cannot think of a case where having the implicit would prevent a common mistake (do you have some in mind?). From my own experience it feels like that's much less a source of errors than passing incompatible arguments in bare calls to == and contains, which is what Eq was designed to fix AFAICT.

@Blaisorblade
Copy link

I don't understand why you want to put an implicit on the CellN class itself instead of on the method. Any particular reasons?

@LPTK thanks for the comments.

CellN classes are just a minimal model of what you need for collections using equality like Set and Map. ListCellN is only a bit more realistic, but I agree you should use Map or Set.

I agree that having implicit arguments for contains-like method is a clear use case. For Map, that includes get and apply. There might be more such methods. But you might need more annotations to catch them all.

When writing these classes, do you hide eqAny or not?

  • if you disable it, it seems you need to show that the key/element type can be compared with itself, so you need extra implicit arguments to the class, and as a consequence also to methods like append (but also map). The only implementation of append above that doesn't use eqAny is ListCell.append3, and it does need an extra Eq instance.
  • if you keep eqAny enabled, you need to ensure manually that all methods like contains take an Eq argument. You might be able to check for that if you maintain enough negative tests. Past experience suggests the chance for bitrot cannot be neglected.

@LPTK
Copy link
Contributor Author

LPTK commented Jun 8, 2017

We can look at it this way:

  • It never makes sense to write 1 == "ok" or (_:Set[Int]) contains "ok", because that always returns false.
  • On the other hand, it sometimes makes sense to write Set(1, "ok") — the validity of a set does not, in general, depend on whether it makes sense to compare each individual element for equality. Therefore, the Eq constraint should not be used to parameterize Set.

I think Eq was not designed to restrict the semantics of equality and change its usage in Scala, but just to rule out code that could be determined to be nonsensical at compile time.

EDIT: Just pressed the "comment and close" button by mistake; subsequently reopened the issue...

@LPTK LPTK closed this as completed Jun 8, 2017
@LPTK LPTK reopened this Jun 8, 2017
@Blaisorblade
Copy link

Blaisorblade commented Jun 8, 2017

Ok, that makes some sense, though supporting it stays hard. But can you now use contains on your Set of 1 and "ok", if it asks for an Eq instance? Thinking a bit about it, it seems that's only possible using eqAny, and I think this use would be valid. But this probably needs more investigation.

@smarter
Copy link
Member

smarter commented Jun 8, 2017

I think there's a much simpler solution to the issue with contains that does not involve Eq. The core problem is that the signature of contains is not what we want:

class ListCell[+T](val values: List[T]) {
  def contains[U >: T](that: U) = values.contains(that)
}

object Test {
  new ListCell(List(1,2,3)).contains("foo") // compiles because we can set U=Any
}

Everything would be fine if we wrote contains(that: T) but that's not possible because of variance checks. However, here it's perfectly fine to ignore variance, it's just that the compiler is not smart enough to see that, but we can force its hand:

import scala.annotation.unchecked.uncheckedVariance

class ListCell[+T](val values: List[T]) {
  // This use of uncheckedVariance is safe because we won't store `that` anywhere
  def contains(that: T @uncheckedVariance) = values.contains(that)
}

object Test {
  new ListCell(List(1,2,3)).contains("foo") // does not compile, as expected
  new ListCell(List(1,2,3)).contains(42) // but this works
}

If using @uncheckedVariance shocks you, consider that the collection strawman already uses it in several places: https://github.com/scala/collection-strawman/search?utf8=%E2%9C%93&q=uncheckedvariance&type= :)

@Blaisorblade
Copy link

Blaisorblade commented Jun 8, 2017 via email

@smarter
Copy link
Member

smarter commented Jun 8, 2017

What about searching Numbers among other Numbers? You know, numbers of different type? Or proxies? Repeat for any Eq instance across types.

Just use .exists(_ == foo) instead of .contains(foo)

If you go this way, do you show or hide uncheckedVariance in the docs?

You need to be honest and show them, or fix the compiler so that they're not needed ;)

@LPTK
Copy link
Contributor Author

LPTK commented Jun 16, 2017

But can you know use contains on your Set of 1 and "ok", if it asks for an Eq instance? Thinking a bit about it, it seems that's only possible using eqAny

What's the problem with eqAny?

You need to be honest and show them, or fix the compiler so that they're not needed ;)

I think the compiler works exactly as intended here. By having ListCell be covariant, you're saying ListCell[A] can be for any type argument B :> A.

So it should not be possible to allow breaches such as the one you suggest because the implementation of contains should not be able to use the fact that its argument is exactly of type A, which would be unsound when the ListCell[A] object is used at type ListCell[B].

Here is your example slightly expanded:

import scala.annotation.unchecked.uncheckedVariance

// Your proposal:
class ListCell[+T](val values: List[T]) {
  def contains(that: T @uncheckedVariance) = values.contains(that)
}

// Now consider this:
def anyListCell: ListCell[Any] = new ListCell[Int](Nil) {
  override def contains(that: Int) = that + 1 > 0
}

anyListCell.contains("oops")

Exception in thread "main" java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer

@smarter
Copy link
Member

smarter commented Jun 16, 2017

Good point, you'd also need to make contains final in ListCell I guess, which should not be too annoying.

@Blaisorblade
Copy link

But can you know use contains on your Set of 1 and "ok", if it asks for an Eq instance? Thinking a bit about it, it seems that's only possible using eqAny
What's the problem with eqAny?

With eqAny in scope you can still write questionable comparisons—between Reddit and arising issues that seemed clear. Luckily, you can use it explicitly if it is not in scope. And it's not clear a Set(1, "ok") is ever a good idea: at best, one can wonder about how to make that fail more gracefully. (A warning somewhere for inferred Foo[Any] might not be a stupid idea).

If you go this way, do you show or hide uncheckedVariance in the docs?

You need to be honest and show them, or fix the compiler so that they're not needed ;)

It's not clear if the compiler can be soundly fixed (nobody proved that a final contains is sound). And part of the point of this rewrite was to have simple signatures (see the whole business with use cases and CanBuildFrom).

I claim that a signature with @uncheckedVariance is not clearly "simple enough" to show. We might have to accept it, but it isn't great. I don't

What about searching Numbers among other Numbers? You know, numbers of different type? Or proxies? Repeat for any Eq instance across types.

What I meant: we should be consistent in these situations.

When you write:

I think there's a much simpler solution to the issue with contains that does not involve Eq.

the overall result is "let's use one complicated solution for == and a different solution for contains, which isn't completely trivial". @smarter, can we agree more consistency is desirable if possible?

Just use .exists(_ == foo) instead of .contains(foo)

Well, on HashSet that means "just use a O(N) algorithm rather than a O(1) algorithm". Convert your foo to the right type seems a better idea, but not always possible.
Also, lots of the complexity of multiversal equality arises exactly to support comparisons across different types. If this isn't fully supported in a consistent way everywhere, one might want to reconsider that extra complexity.

@szeiger
Copy link
Member

szeiger commented Jun 20, 2017

My impression from the discussion here (and around multiversal equality in Dotty) so far is that it's too soon to incorporate this into the collection design. I suggest to explore this further in Dotty in a fork or once we're done with the integration into Scala 2.13. Adding Eq parameters to the collections and a fake Eq typeclass to Scala 2.13 would be premature at this point.

@Blaisorblade
Copy link

I agree more research seems indeed needed.

Should we move these questions to the Dotty repo? And what's the process for these language changes?

I also wonder how such language changes are going to be decided upon. Will multiversal equality be subject to the SIP before it's in the stable language?

@Blaisorblade
Copy link

While we're here: I just realized that @smarter proposal arguably exploits a typechecker misbehavior in Scala and Dotty, violating in some sense the Liskov Substitution Principle: everything possible on values of T must be possible on values of subtypes of T.
I'm not implying that's necessarily a bug.

Here's an example, that gives the same behavior in Scala and Dotty's REPLs (including workarounds for scala/scala3#2789):

import scala.annotation.unchecked.uncheckedVariance

class ListCell[+T](val values: List[T]) {
  final def contains(that: T @uncheckedVariance) = values.contains(that)
}
(new ListCell(List("")).contains(_: Any)) //fails
((new ListCell(List("")): ListCell[Any]).contains(_: Any))

That means that operations are possible in (new ListCell(List("")): ListCell[Any]) that aren't possible on new ListCell(List("")), and this seems a (syntactic) violation of the Liskov Substitution Principle. At least it's inconsistent: in OCaml's you always have to upcast manually, but in Scala you essentially never need to.

@LPTK
Copy link
Contributor Author

LPTK commented Jun 21, 2017

Note that this is not the only occurrence of the violation. I can write Nil.size but not ???.size although Nothing <: Nil.type.

@julienrf
Copy link
Contributor

julienrf commented Jan 3, 2018

I agree with @szeiger comment. Therefore I’m closing this issue.

@julienrf julienrf closed this as completed Jan 3, 2018
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants