-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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
Multiversal Equality #1247
Comments
I think this can be refined further, we don't wont to be able to call |
@smarter. Yes, indeed. Maybe we can drop the clause completely because it is already subsumed by the "don't test if it's a global subtype" requirement. |
so, does this proposal introduce '===' or fix '==' ? |
@OlegYch : It fixes |
I'm a bit concerned regarding the
From my perspective it would be better if there was a boilerplate free way to phase-in the new approach, and offer some (maybe annotation-based?) solution to get back the old behavior? Has the "more traditional" way been considered of requiring a typeclass for equality operations instead of providing them by default? What was the lesson here and how did it compare to the proposed approach in this PR? More conceptually, how will this work with the varying levels of "sameness": Identity, equality and floating-point rules? |
@soc I have discussed lots of other ways to make == safe with lots of people, but none of them worked out as well as this one. But that should not stop others from trying! |
I now think it is slightly more consistent to change the requirement on An instance
is valid if |
To be perfectly precise you should exclude |
OK, changed. |
While I applaud the attempt to make I think the better solution is to have the opposite defaults: If you want to allow universal equality on a type, you must add To avoid the problem of backwards incompatibility, one could easily add a language feature import such as WDYT? |
@martin Do you mean
What about case class hierarchies? trait Base //possibly sealed
case class A extends Base
case class B extends Base
... An annotation would be appropriate for Base — it's not clear it can ever be inferred somehow. |
@Sciss Martin's goal, as I understand it, is: Existing code should keep working without changes. Proposals ignoring that will get ignored — I thought that much was clear from the debate on redoing collections. And I'd say, you need a plausible path to incrementally convert code to the new rules, as in gradual typing. So if you want to make that proposal considered, at least flip things: provide |
I'd like to point out that implementing this proposal requires changes to implicit search: 340f883 The main motivation for this proposal is safe refactorings. Unfortunately, the implementation introduces a difference in behavior of top-level type arguments from all the other. This may make refactorings harder as introducing one more(even invariant!) level of type arguments would be a huge change to behavior of the API. At the same time, such a difference in behavior introduces one more freedom of flexibility for library author(as implicits can be chained to infer parameters level-by-level). This can be a source of surprise for someone who tries to understand how implicits work. While I see the rationale, and I like the generated code. I'd feel a lot more confident in making needed change to implicit search if it went through a proper sip process. I'm in favor of this change currently, though I'm not sure how much would it affect existing code and how much surprising would this behavior be to newcomers. |
That's exactly what I'm proposing with What you are saying is flip things back to Martin's proposal. So what's the addition here? So if your old code read
That constituted a bug, and thus "breaking" compilation in the new version should be the desired behaviour. So we assume everything in std lib will have Then in client code if you have the rare case of
You can still compile it if you add legacy flag Win-win IMHO. |
No, only the prototype is for Dotty, otherwise compatibility would indeed make no sense.
That's not the intention: But developers that want to upgrade a huge codebase to a new compiler (say, enterprise shops) will only need to deal with deprecations, without additional busywork.
I propose adding that flag for small or new projects. That doesn't work for converting a code base. See the experience with the transition to Python 3 (still ongoing) or with the alternative to gradual typing (that weren't adopted because with them converting to a code base was implausible). With Martin's proposal, you can add |
Issue: Can one ever introduce An excellent inspiration is given by gradual typing. There you have two type systems, a lax and a strict one (the weak one is usually "no type system", but that seems incidental). There, you need to opt-in to the strict type system both at the definition-site and at the call-site. When you turn some laxly-typed API into strictly-typed API (say, by adding a type signature), existing laxly-typed clients keep compiling, until they're switched to strict typing themselves. For strict compatibility, we'd need to do something similar: some language flag saying "in the scope where this is visible, uses of equals are checked with the new discipline". This might be overkill, but to check if this is actually needed, we'd need to study the overhead on community builds, and confirm it's below some very low threshold. We'll also need numbers about the number of false positives in a bigger study: if all errors are bugs, they might be a bit more acceptable. |
Then I fail to understand how this would magically avoid the annotations. The import surely happens on the use-site not declaration-site. Or do you mean that if I import that flag, all
Then if I have a use-site
How would that import change the compiler's behaviour in your opinion? Presumably that import means universal equality is disabled. So how do you get your
That works precisely for converting a code base. If you have obsolete
Then if you remove the import, you get the compile error. Then if you want to stick to your declaration, you add And what does this have to do with Python 3? There will be a Scala version where procedure syntax and XML literals go from warning to error. So what? I thought we were better than Java in allowing the language to improve over time. The problem with |
What about |
If you were to read my posts, I did describe the opposite:
I also described some issues with that.
If I had a use-site flag (which I proposed later, orthogonally to our discussion), it would enable the discipline being proposed by Martin, under which
I'm talking about codebases big enough that getting to a new correct state takes lots of time — hundreds of thousands of lines.
Deprecation warnings are different: if your code compiles without deprecation warnings, it will work with the next version (modulo small unforeseen issues). And IIRC Martin claimed, at some point, that doing those changes required automated refactoring support.
"Yes", but developers are very concerned about the existing user base, so changes have to happen carefully — especially for something as pervasive as equality. Some summarize the situation as "no", though I disagree. If you want some evidence, take a look at the collection redesign that I already mentioned: #818. Most proposed changes were excluded because they broke compatibility. I only answered your post to inform you that this kind of concern. Overall: I'll take a break from this subthread, because it's dominating the rest; it does not seem very productive; moreover, our perspectives seem too distant. (And I'm not the one to convince anyway). |
Couldn't the type class instance just come with an implementation method, and if you have it then use it? |
I like the proposal, but would prefer the defaults to be switched. I.E. opt-out of the new behavior of == instead of opt-in
|
@Blaisorblade @Sciss It's an interesting idea to switch the defaults. As far as dotty is concerned I am not so much concerned about backwards compatibility - we already have a -language:Scala2 import which could take care of that. But the real problem that I see is what @Blaisorblade noticed: Not all classes are an @equalityClass, so where should the annotation be inserted? One way I can see is:
But that's fragile. Say we have a hierachy
and we want to make Points comparable to Points and Shapes comparable to Shapes (as seems reasonable). Under the current proposal you write
Under the alternative proposal you write:
This seems a bit backwards and fragile to me. It's easy to forget @universalEquality on some trait, and if you do forget it you get overlapping equality classes in subclasses that mix in this trait. I would not be surprised if in the end the number of necessary @unversalEquality annotations would greatly exceed the number of necessary @equalityClass annotations under the current proposal. |
Regarding the universal signature of the |
@Sciss @Blaisorblade The currently proposed scheme also supports a simple heuristic:
I don't see a similar heuristic for |
Could the implementation of |
@odersky Thanks for your comments. I can see the difficulties in unambiguously deciding for which types we have the new equality under the "opposite default" scheme. With the heuristics of synthesising the type class when This kind of connects then to the question of ADT syntax - because you can have |
I strongly agree with @lrytz. If the long term goal is simplification of the language, we cannot always rely on implementing everything with macros and annotation purely as library views. While I generally like Scala's approach of going library first before baking it into the language - e.g. collections, concurrency - I think these fundamental things like equality, abstract data types etc. should look very clean and not tucked on through some |
@lrytz I thought the goal this issue requires fragmenting equality into legacy and non-legacy mode and giving choices to users. So why should annotations not be composable? My proposal is simply that I'm not talking about splitting Then, there's already a split between builtin equality and Haskell-style Finally: if a solution if is flexible enough and clearly right, it doesn't hurt to make it a builtin. Regarding Scala's approach in general, I'd recommend https://www.youtube.com/watch?v=_ahvzDzKdB0 (you can also google "Growing a language Guy Steele" to find a transcript). |
@Blaisorblade I am not too concerned about migration away from |
I moved |
IMO there's still a big issue in this proposal that seems to have gone unnoticed, in that we're still relying on a dev's one-time, trusted declaration of equality. As we all know, over time and after refactorings, past declarations can easily become invalid. Consider: // In file A we have:
@equalityClass case class A (number: Int, name: String)
// Then in another file, much further down the dependency graph, we have
@equalityClass case class B (allOfMyStuff: List[A], number: Int) All looks good in the above and then a year later there's a refactoring to // New and improved A!
// Universal equality no longer holds here.
trait A {
val number: Int
def name(): String
} whilst, unbeknownst to the refactorer, the following code has now become incorrect and escaped their notice. // ↓ No longer true! Oh noes.
@equalityClass case class B (allOfMyStuff: List[A], number: Int) I recently open-sourced a small library with a similar objective to this proposal, called UnivEq. I solved this by having a macro to derive an instance after inspecting the fields of a case class. If all the case class's fields have proven or trusted universal equality, then all is well, else there is a compiler error that informs the user about the bereft fields. In code, it looks like this: case class B (allOfMyStuff: List[A], number: Int)
object B {
implicit def univEq = UnivEq.derive[B]
} which compiles in the first case above, and fails compilation after the refactoring to I think it critical to include some kind of similar ability in this proposal, or else the refactoring fear remains. |
In what sense is this no longer true? |
First, I generally agree with the concern that Second, going to @japgolly's comment, I guess his @japgolly's UnivEq[A] does I think something slightly different — it proves that |
Say you start with this:
And then after a refactoring,
Here you can can see here that If I refactored a class and, for whatever reason, had to remove it's equality, then it's very important for me to know that any other classes whose equality depends on the equality just removed, should also be flagged to me. Else I could find out in production that "hey something's wrong, oh it turns out that @equalityClass needed to be removed on B but we missed it cos the codebase is huge.". @Blaisorblade np, I'll try to update my docs to make it clearer. The point of my library was that I need to know (and continue to know) that if I depend on If you're correct in:
then IMO this proposal does way to little to be useful, because it's just too easy to introduce incorrectness after refactorings, or even when you're first creating classes. Maybe it's a philosophical difference in that I'm not just interested in ensuring that |
Now that we know better there are two different things in discussion, we can compare them — and I like @japgolly's idea. It also resembles the behavior of Haskell's But I haven't worked out & checked all the details — I haven't even re-read the proposal in full to check if this change would fit in and preserve all properties, though I guess it should. |
Well it should also be noted that Scala does have a concept of reference equality as well as structural equality, unlike Haskell which only really deals with structural equality. |
This is in fact desired, and assumed. The proposal here and |
The described implementation has been merged. |
Is it possible to make If it is possible, we can proof equality at compile time, like:
|
@Atry You seem to imply that |
The current |
How?
…On Mon, Jul 10, 2017 at 11:39 AM 杨博 (Yang Bo) ***@***.***> wrote:
The current .type behavior breaks referential transparency
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1247 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAGAUByS9sER-swgOTU_bU2i3NurMp2Nks5sMkWlgaJpZM4IZY7K>
.
|
Given `val x: Some[42] = Some[42](42)`,
`x`, as a case class, it should be able to replace to its definition
without changing behavior. It's true for expressions. However, not true for
types:
`implicitly[Some[42] =:= Some[42]] // compiles`
`implicitly[x.type =:= Some[42]] // does not compile`
2017-07-11 8:23 GMT+08:00 nafg <[email protected]>:
… How?
On Mon, Jul 10, 2017 at 11:39 AM 杨博 (Yang Bo) ***@***.***>
wrote:
> The current .type behavior breaks referential transparency
>
> —
> You are receiving this because you were mentioned.
> Reply to this email directly, view it on GitHub
> <#1247 (comment)>,
> or mute the thread
> <https://github.com/notifications/unsubscribe-auth/AAGAUByS9sER-swgOTU_
bU2i3NurMp2Nks5sMkWlgaJpZM4IZY7K>
> .
>
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1247 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAktus8ljgyxweIEmPAMHtYXmbGcO1fKks5sMsCHgaJpZM4IZY7K>
.
--
杨博 (Yang Bo)
|
The case class behavior is different from binding of literal types:
val y: 4 = 4
implicitly[y.type =:= 4] // compiles
2017-07-11 8:54 GMT+08:00 杨博 <[email protected]>:
… Given `val x: Some[42] = Some[42](42)`,
`x`, as a case class, it should be able to replace to its definition
without changing behavior. It's true for expressions. However, not true for
types:
`implicitly[Some[42] =:= Some[42]] // compiles`
`implicitly[x.type =:= Some[42]] // does not compile`
2017-07-11 8:23 GMT+08:00 nafg ***@***.***>:
> How?
>
> On Mon, Jul 10, 2017 at 11:39 AM 杨博 (Yang Bo) ***@***.***>
> wrote:
>
> > The current .type behavior breaks referential transparency
> >
> > —
> > You are receiving this because you were mentioned.
> > Reply to this email directly, view it on GitHub
> > <#1247 (comment)>,
> > or mute the thread
> > <https://github.com/notifications/unsubscribe-auth/
> AAGAUByS9sER-swgOTU_bU2i3NurMp2Nks5sMkWlgaJpZM4IZY7K>
>
> > .
> >
>
> —
> You are receiving this because you were mentioned.
> Reply to this email directly, view it on GitHub
> <#1247 (comment)>,
> or mute the thread
> <https://github.com/notifications/unsubscribe-auth/AAktus8ljgyxweIEmPAMHtYXmbGcO1fKks5sMsCHgaJpZM4IZY7K>
> .
>
--
杨博 (Yang Bo)
--
杨博 (Yang Bo)
|
That's because XXX.type is defined to be a singleton type (a type that is
inhabited by exactly one value) and the literal type 4 is a singleton type.
So they are the identical type: the singleton type defined to be inhabited
only by 4.
However Some[42] is not a singleton type at all. There can be multiple
values of type Some[42]. Given val x, x.type is inhabited only by the value
x. So they are not the same type. They are different types and their
inhabitants differ.
Honestly I've never heard of type-level referential transparency anyway
(although as I explained it's a moot point here).
Anyway I'm no compiler hacker or type theorist so I could be wrong, but
that's how I see it and why your objection doesn't bother me.
On Mon, Jul 10, 2017 at 8:58 PM 杨博 (Yang Bo) <[email protected]>
wrote:
… The case class behavior is different from binding of literal types:
val y: 4 = 4
implicitly[y.type =:= 4] // compiles
2017-07-11 8:54 GMT+08:00 杨博 ***@***.***>:
> Given `val x: Some[42] = Some[42](42)`,
> `x`, as a case class, it should be able to replace to its definition
> without changing behavior. It's true for expressions. However, not true
for
> types:
>
> `implicitly[Some[42] =:= Some[42]] // compiles`
>
>
> `implicitly[x.type =:= Some[42]] // does not compile`
>
>
>
>
> 2017-07-11 8:23 GMT+08:00 nafg ***@***.***>:
>
>> How?
>>
>> On Mon, Jul 10, 2017 at 11:39 AM 杨博 (Yang Bo) ***@***.***
>
>> wrote:
>>
>> > The current .type behavior breaks referential transparency
>> >
>> > —
>> > You are receiving this because you were mentioned.
>> > Reply to this email directly, view it on GitHub
>> > <#1247 (comment)
>,
>> > or mute the thread
>> > <https://github.com/notifications/unsubscribe-auth/
>> AAGAUByS9sER-swgOTU_bU2i3NurMp2Nks5sMkWlgaJpZM4IZY7K>
>>
>> > .
>> >
>>
>> —
>> You are receiving this because you were mentioned.
>> Reply to this email directly, view it on GitHub
>> <#1247 (comment)>,
>> or mute the thread
>> <
https://github.com/notifications/unsubscribe-auth/AAktus8ljgyxweIEmPAMHtYXmbGcO1fKks5sMsCHgaJpZM4IZY7K
>
>> .
>>
>
>
>
> --
> 杨博 (Yang Bo)
>
--
杨博 (Yang Bo)
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1247 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAGAUHgjVBAefra8zq3q7WFBKh37rhYOks5sMsi0gaJpZM4IZY7K>
.
|
Note: I edited the definition of "lifting" by adding the clause:
Here's a scenario where this is important:
In the
Without the change, this fails as We might need further tweaks in the future to what exactly lifting should be. |
It's the case without |
Note
The status of
eqAny
and other predefined eq comparisons has changed in #2786, together with the resolution algorithm. The up-to-date details are in the reference http://dotty.epfl.ch/docs/reference/multiversal-equality.htmlMotivation
Scala prides itself of its strong static type system. Its type discipline is particularly useful when it comes to refactoring. Indeed, it's possible to write programs in such a way that refactoring problems show up with very high probability as type errors. This is essential for being able to refactor with the confidence that nothing will break. And the ability to do such refactorings is in turn very important for keeping code bases from rotting.
Of course, getting such a robust code base requires the cooperation of the developers. They should avoid type
Any
, casts, stringly typed logic, and more generally any operation over loose types that do not capture the important properties of a value. Unfortunately, there is one area in Scala where such loose types are very hard to avoid: That's equality. Comparisons with==
and!=
are universal. They compare any two values, no matter what their types are. This causes real problems for writing code and more problems for refactoring it.For instance, one might want to introduce a proxy for some data structure so that instead of accessing the data structure directly one goes through the proxy. The proxy and the underlying data would have different types. Normally this should be an easy refactoring. If one passes by accident a proxy for the underlying type or vice versa the type checker will flag the error. However, if one accidentally compares a proxy with the underlying type using
==
or a pattern match, the program is still valid, but will just always sayfalse
. This is a real worry in practice. I recently abandoned a desirable extensive refactoring because I feared that it would be too hard to track down such errors.Current Status
The problems of universal equality in Scala are of course well known. Some libraries have tried to fix it by adding another equality operator with more restricted typing. Most often this safer equality is written
===
. While===
is certainly useful, I am not a fan of adding another equality operator to the language and core libraries. It would be much better if we could fix==
instead. This would be both simpler and would catch all potential equality problems including those related to pattern matching.How can
==
be fixed? It looks much harder to do this than adding an alternate equality operator. First, we have to keep backwards compatibility. The ability to compare everything to everything is by now baked into lots of code and libraries. For instance, we might have aMap
withAny
keys that usesuniversal equality and hashcode to store and retrieve any value. Second, with just one equality operator we need to make this operator work in all cases where it makes sense. An alternative
===
operator can choose to refuse some comparisons which would still be sensical because there's always==
to fall back to. With a unique==
operator we do not have this luxury.The current status in Scala is that the compiler will give warnings for some comparisons that are always false. But the coverage is very weak. For instance this will give a warning:
But this will not:
There are also cases where a warning is given for a valid equality test that actually makes sense because the result could be
true
. In summary, the current checking catches some obvious bugs, which is nice. But it is far too weak and fickle to be an effective refactoring aid.Proposal
I believe to do better, we need to enlist the cooperation of developers. Ultimately it's the developer who provides implementations of equality methods and who is therefore best placed to characterize which equalities make sense. Sometimes this characterization can be involved. For instance, an
Int
can be compared to other primitive numeric values or to instances of typeNumber
but any other comparison will always yieldfalse
. Or, it makes sense to compare twoList
values if and only if it makes sense to compare the list's element values.The best known way to characterize such relationships is with type classes (aka implicit values). A type class
Eq[T, U]
can capture the property that values of typeT
can be compared to values of typeU
. Here's the proposed definition of this type class:Note 1:
Eq
is contravariant. So an instance of, say,Eq[Number, Number]
is also an instance ofEq[BigInt, BigDecimal]
. In other words: If all instances ofNumber
can be compared thenBigInt
s can be compared toBigDecimal
s, because they are both instances ofNumber
.Note 2:
Eq
does not have any members; it's a pure marker trait. The idea is that the Scala compiler will check every time it encounters a potentially problematic comparison between values of typesT
andU
that there is an implicit instance ofEq[T, U]
. A comparison is potentially problematic if it is between incompatible types. As long asT <: U
orU <: T
the equality could make sense because both sides can potentially be the same value.The Scala compiler will also perform this check on every pattern match against a value (i.e. where the pattern is a non-variable identifier or a selection, or a literal). It treats such a pattern match like a comparison between the type of the scrutinee and the type of the pattern value.
Developers can define equality classes by giving implicit
Eq
instances. Here is a simple one:Since
Eq
does not have any members, the sole purpose of these implicit instances is for type checking. The right hand side of the instance does not matter, as long as it is type-correct. The companion objectEq
is always correct since it extendsEq[Any, Any]
.Parameterized types generally need polymorphic
Eq
instances. For example:This expresses that
List
s can be compared if their elements can be compared.What about types for which no
Eq
instance exists? To maintain backwards compatibility, we allow comparisons of such types as well, by means of the standardeqAny
instance in theEq
object that was shown above. The type signature ofeqAny
suggests that it works for any two types, but this would render equality checking ineffective, becauseEq
instances would always be found. But in fact the compiler will check any generatedeqAny
instance in implicit search for validity.Let
lift
be a function on types that maps every covariant occurrence of an abstract type to its upper bound and that drops all refinements in covariant positions. An instanceis valid if
T <: lift(U)
or ifU <: lift(T)
or if bothT
,U
are Eq-free. A typeS
is Eq-free if there is no implicit instance of typeEq[S, S]
other thaneqAny
itself. InvalideqAny
instances will not returned from implicit search.Note 3: The purpose of
lift
above is to make code like this compile:Without it, we would have to resort to a widening cast, i.e.
if (x.asInstanceOf[Any] == null
, which is ugly.Note 4: It is conceivable that the
eqAny
behavior can be implemented as a macro. We will know more once macros are redesigned.A Refinement
The
scala.equalityClass
annotation can be used to avoid the boilerplate of writing implicitEq
instances by hand. If@equalityClass
is given for a classC
, the companion object ofC
would get an automatically generatedEq
instance defined in the way sketched above. For instance:would generate the following
Eq
instance:It should be possible to get this functionality by making
@equalityClass
a macro annotation.Properties
Here are some properties of the proposal
allow comparisons only between their instances with
@equalityClass
, or they have to define implicitEq
instances by hand.@equalityClass
annotations equality works as before.equality is not affected at all.
Eq
instances given, it can be very precise. That is,no comparisons that might yield
true
need to be rejected, and most comparisons thatwill always yield
false
are in fact rejected.The scheme effectively leads to a partition of the former universe of types into sets of types. Values with types in the same partition can be compared among themselves but values with types in different partitions cannot.
An
@equalityClass
annotation on a type creates a new partition. All types that do not have anyEq
instances (excepteqAny
, that is) form together another partition.So instead of a single universe of values that can be compared to each other we get a multiverse of partitions. Hence the name of the proposal: Multiversal Equality.
Implementation Status
The core of the proposal is implemented in #1246. The refinement of having
@equalityClass
annotations generateEq
instances is not yet implemented.Experience
As a first step, I added
Eq
instances to some of the core types ofdotty
:Type
,Symbol
,Denotation
,Name
. Two bugs were found where comparisons made no sense because they compared values of different types and therefore would always yield false (one of them was a pattern match). There were no instances where a sensical comparison was flagged as an error.A Possible Variant
The current proposal needs a change to the handling of contravariant type parameters in implicit search and overloading resolution, which is described and implemented in 340f883. Without that change,
eqAny
would always take precedence over any other implicitEq
instance, which is not what we want.If we do not want to rely on that change, one could alternatively make
Eq
non-variant, but thenEq
instances become more complicated because they have to talk about all possible subtypesof an equality class using additional type parameters.
The text was updated successfully, but these errors were encountered: