ericniebler / stl2

LaTeX and Markdown source for the Ranges TS/STL2 and associated proposals
88 stars 8 forks source link

EqualityComparable should require that things compare equal to themselves. #509

Open ericniebler opened 7 years ago

cjdb commented 7 years ago

Should we stop there, or require an equivalence relation?

CaseyCarter commented 7 years ago

We're close. Close enough that I tricked myself into believing EqualityComparable requires an equivalence relation when I wrote the note in [concepts.lib.compare.equalitycomparable]/3: "[ Note: The requirement that the expression a == b is equality preserving implies that == is reflexive, transitive, and symmetric.—end note ]."

Suppose bool(a == b) holds for values a and b of EqualityComparable type T. By the definition of EqualityComparable, a must be equal to b. Since == is equality preserving, we can substitute a for b and b for a in bool(a == b) to get bool(b == a) which must be equal to bool(a == b). By the same argument, bool(b == a) implies bool(a == b), so == is symmetric.

If bool(b == c) further holds for some value c, we can substitute a for b to get bool(a == c); == is transitive.

If we substitute only a for b in bool(a == b), we get bool(a == a). So for any a, it must be the case that either there is no b such that bool(a == b), or bool(a == a) must hold. If a is equal to anything, it must be equal to itself as well.

This falls just short of requiring an equivalence relation, which I suspect is the best we can do without requiring a == a to be in the domain of == which we notably cannot do if we want EqualityComparable to admit floating point types thanks to the existence of NaNs.

CaseyCarter commented 6 years ago

@ericniebler Are you happy enough with this state of affairs, or do you still believe there's a problem here that needs to be addressed?

ericniebler commented 6 years ago

... which we notably cannot do if we want EqualityComparable to admit floating point types thanks to the existence of NaNs.

Why do we need to care about NaNs for EqualityComparable when we don't for Strict totally ordered?

CaseyCarter commented 6 years ago

Why do we need to care about NaNs for EqualityComparable when we don't for Strict totally ordered?

The argument is the same for both concepts: We can prove that bool(a == a) is true for an EqualityComparable type if it is well-defined for a particular choice of a, and we can likewise prove that bool(a < a) is false for a StrictTotallyOrdered type if it is well-defined for a particular choice of a. What we cannot do is require that those expressions must be well-defined for all values of a type in order for that type to model the concepts.

zygoloid commented 6 years ago

We can prove that bool(a == a) is true for an EqualityComparable type if it is well-defined for a particular choice of a,

Can we? Given:

struct X { int n; };
bool operator==(X, X) { return false; }

which rule do I violate if I claim that X is EqualityComparable and the domain of == covers all values of type X?

I think EqualityComparable<T> is missing the constraint that for all values a of T such that (a, a) is in the domain of ==, bool(a == a) is true.

CaseyCarter commented 6 years ago

which rule do I violate if I claim that X is EqualityComparable and the domain of == covers all values of type X?

You're right: my "we can prove" statement has an implicit premise that a is an equality-preserving expression. (Which I believe is equivalent to your suggested constraint.)

CaseyCarter commented 6 years ago

Proposed Resolution [retracted]

Modify [concept.equalitycomparable] as follows:

 template<class T> 
concept EqualityComparable = 
   weakly-equality-comparable-with <T, T>
+  && requires(const remove_reference_t<T>& t) { t; }
 ;
 2 Let a and b be objects of type T. EqualityComparable<T> is satisfied only if bool(a == b) is
   true when a is equal to b (22.2), and false otherwise.

 3 [ Note: The requirement that the expression a == b is equality-preserving implies that == is
   transitive and symmetric. -end note ]

+? [ Note: The requirement that t is an equality-preserving expression implies that t must be
+   equal to t if t is in the domain of `==`. Consequently bool(t == t) must be true. -end note ]
CaseyCarter commented 6 years ago

I've retracted my PR. The notion that objects are equal to themselves is fundamental to the semantics of equality-preserving expressions; EqualityComparable is not the right place to fix the problem. We need to fix the wording in [concepts.equality].