dart-lang / language

Design of the Dart language
Other
2.67k stars 205 forks source link

Is equality for int and double specified, implementation defined, or undefined? #1431

Open leafpetersen opened 3 years ago

leafpetersen commented 3 years ago

In a discussion of integer semantics (cc @vsmenon ) I was mildly surprised that 1 == 1.0 is true on our native platforms. I looked for a specification of equality semantics in the specification and didn't find it. The VM implementation does in fact make that equation true. It also makes the following, more surprising equations true:

void main() {
  int x = 4611686018427387904;
  double y = 4611686018427388000.0;
  print(x == y); // Prints true
  print(y == x); // Prints true
}

Is this specified behavior that I just missed? If not, is this missing spec language, or do we consider this to be implementation defined behavior (or even undefined behavior)?

cc @eernstg @lrhn

eernstg commented 3 years ago

Checking all occurrences of == in the language specification, I also cannot see any specification of the behavior of operator == on an instance of int or double when the argument has the type double respectively int.

So we'd rely on the num specification here:

If one operand is a double and the other is an int, they are equal if the double has an integer value (finite with no fractional part) and identical(doubleValue.toInt(), intValue) is true.

This might have been motivated by portability issues, because we can't distinguish those values on the web.

lrhn commented 3 years ago

The specification of that is in the platform libraries. We don't specify very much class-specific behavior in the language specification (only really the identical function, and Type and Symbol object equality). It has "always" been documented to work that way (back to before Dart 1.0), and the VM behavior used to be wrong according to that specification (https://github.com/dart-lang/sdk/issues/4018). Web compilation has always been trivally correct because they have no integers, and we've embraced that now.

The class documentation says that == and < should be based on the numerical values. That makes it a consistent operation on num. (And what Erik quotes is actually wrong now that we have fixed-sized integers. The doubleValue.toInt() loses precision if the value is greater than 2^63, but in that case it's definitely strictly greater than all integer values).

The VM used to convert the integer to double first when comparing an int and a double. They initially argued that it's consistent with other double operations, like +. (It can be argued that the double represents a range, so it only matters if the integer is in that range, but we don't say that for other things, and it means == isn't transitive since 9007199254740994.0 == 9007199254740994 and 9007199254740994.0 == 9007199254740995, but 9007199254740994 != 9007199254740995).

Edit. I thought the VM had never fixed it, but they had. Was probably done when we introduced 64-bit integers. Cheers!

leafpetersen commented 3 years ago

The specification of that is in the platform libraries. We don't specify very much class-specific behavior in the language specification (only really the identical function, and Type and Symbol object equality).

Where is this? I was kind of expecting that, but the only treatment of == I can find is in lib/_internal/vm/lib which just calls into a VM native. In general, my sense has been that things which are implemented in Dart in the publicly visible core libraries can reasonably be said to be "specified" by the Dart code (there is, among other things, a single implementation), but I don't think that == can actually be written in Dart, right? And hence can't really be said to be specified by its (Dart) implementation.

I wonder how breaking "fixing" this would be?

lrhn commented 3 years ago

For number equality, the specification is just the documentation of num.operator==, int.operator== and double.operator== (which all agree with num.operator==) plus the language specification of the == operator (pre-check for null, then call operator==.)

leafpetersen commented 3 years ago

Maybe this is a dartdoc bug then (cc @jcollins-g )? The documentation here doesn't seem to say anything about this.

lrhn commented 3 years ago

The int documentation does seem to miss inheriting the == from num documentation.

munificent commented 3 years ago

It is a little odd that the spec doesn't define == on ints but does specify that ints have primitive == and then uses primitive == for determining compile-time errors. That implies that a Dart core library implementation gets to decide whether this program has a compile-time error or not:

const c = {1, 1};
jcollins-g commented 3 years ago

here

This was a bug in dartdoc, however it was fixed as part of our gradual cleanup of inheritance and interface linkage.

Inheritance is shown correctly for operator== here. https://api.dart.dev/dev/2.13.0-0.0.dev/dart-core/int-class.html

lrhn commented 3 years ago

@munificent Correct. The platform libraries determine the behavior of a lot of compile-time evaluated operations. It's also the libraries which decide that const x = 1 ~/ 0; is a compile-time error, because the evaluation would throw.

The semantics of compile-time evaluation are the same as for run-time evaluation. We just restrict the potentially constant expressions in such a way that we know that we can actually do the evaluation at compile-time without running any Turing complete code. We don't specify the meaning of a constant 1 + 2 in the language specification either.

Pedantically, we don't "use primitive ==" to determine compile-time errors, just ==. The requirement of having "primitive ==" is just to ensure that it's a == we can compute it at compile-time. A const {1, 1} set is a compile-time error because it's an error for the constant set literal to contain elements that are ==, which it does because of the definition of int.operator==.

(We don't even specify in the language specification that Object.operator== is the same as identical, but we rely heavily on it - it's why "not overriding Object.==" means that we have primitive equality. If Object.== had defaulted to checking that the object had the exact same type and doing a == check on the values of each field, then that wouldn't be compile-time computable. The language specification is not separate from the platform library specification, the two are intertwined. We don't have to specify that integers are 64-bit in the language specification, but we need to talk about literals which cannot be represented precisely, so it sneaks in. We do say that Object implements some base functions (toString and noSuchMethod are necessary to the spec. We do say that bool has only two values and Null has only one. Maybe we should specify a number of the base classes in more detail. If we do that, we should think hard about what needs to be there, and what's just gravy, because most of the methods on bool are irrelevant to the spec.)

eernstg commented 3 years ago

I think the precision and the stability of the core class documentation is rather independent of the location: It will have to be precise and stable both in the current placement (as dartdoc comments in core library source code) and if it were moved into the language specification.

However, we'd still need the per-member documentation in a similar form as this. So if we specify some/many Dart core members as part of the language specification, we'd need to duplicate that information as dartdoc comments as well. To me, this implies that it is a useful rule to say "class members are documented in DartDoc, not in the language specification". Let's just keep it that way.

About operator == being primitive: I agree with @lrhn that it is

just to ensure that it's a == we can compute it at compile-time

However, we don't specify anything of that nature. We just use the concept of a primitive == as an uninterpreted label that can put on specific classes of our choice, and we've chosen to put it on a set of classes where the implementation of that operator is controlled by system libraries. This means that we are able to ensure that we can compute the value of e1 == e2 at compile-time in specific situations, and that's what we need.

However, one single thing that came up recently is the fact that JavaScript-compiled >> works on 33 bits, not 32 bits (because the sign bit is the IEEE 754 sign bit, and it is copied into the topmost (31st) bit at each step of the right shift). We should document that. Cf. https://github.com/dart-lang/language/issues/1434.