They are both the same, mathematical equality. It's just a matter of which mathematical object you're comparing. Objects in programming are not mathematical objects, they represent mathematical objects, and how they represent them is a matter of definition / semantics / documentation / interpretation.
11111111 in memory can represent a sequence of 8 bits, or it can represent the number 255, or it can represent the number -1.
Hence you have different notions of "equality" and "order" depending on whether you're comparing bit representations, or whether you're comparing the numbers these representations correspond to according to our interpretation.
Eq is supposed to return true when the semantic interpretation (that the programmer defines) of two objects are the same. Their representations in memory may be different. There is a specific (weaker) requirement that this must satisfy transitive properties between representations, etc.
a == b;
// is equivalent to
::std::cmp::PartialEq::eq(&a, &b);
The operator == is defined in terms of PartialEq::eq, which is not equality (in the mathematical sense).
Yet we might claim that if a type also implements Eq, then it (magically) becomes equality. But I think that's not the (main) point of Eq. The point is that Eq adds reflexivity.
Anyway, maybe this is just a semantical discussion. But still, it might help to add some fixes to the docs to help ease confusion.
(And it's needed in regard to PartialOrd in any case, I would say.)
Note that this relationship between more concrete representations of more abstract objects, where equivalent representations represent equal objects, is precisely the thing that equivalence relations allow you do to.
The more abstract objects that are being represented are gained by creating a quotient structure, i.e. by considering equivalence classes. But they can also be a set of canonical representatives, or any other set of objects as long as you have a (many-to-one) mapping from representatives to those objects.
I would agree that it is valid to claim Eq means "equality". But it raises some (legitimate) concerns in regard to PartialEq. What is PartialEq then? And does the documentation really point out the difference properly?
I could live either with Eq being said to be "equality" (but this requires some clarification in the overview perhaps), or with Eq being said to be an "equivalence relation".
But I'm not happy with PartialOrd being described as "partial order", because it is not.Edit: I have to think about this again. Maybe you could demand that it's only implemented for partial orders.Edit #2: But then you could also always implement Eq.
Exactly what I've been saying. == means equality of the semantic interpretation of what the objects mean. It is an equivalence relationship on representations. But it's still equality.
For comparison, note that e.g. Haskell does go further in their specification of an Eq trait since they also require a form of “extensionality”
if x == y = True and f is a function whose return type is an instance of Eq , then f x == f y = True
Since in Rust, types like Vecdo have (public) API that includes functions like Vec::capacity(&self) -> usize which violates extentionality (i.e. x == y does not imply x.capacity() == y.capacity()), it seems legitimate to keep describing Eq as a trait for a (canonical) equivalence relation on a type, not necessarily really some form of “equality”.
Formally, PartialOrd cannot describe a (plain) partial order because a partial order is a binary relation. PartialOrd also requires you to also implement PartialEq, which is a "partial equivalence relation".
I think.
And if you derive an equivalence relation from a partial order, then it will be reflexive. Thus you could also implement Eq.
I think.
But you don't want to implement Eq for partial orders. Now I'm totally confused.
P.S.: Ignore this post if it doesn't make sense. Maybe I thought about this topic too much.
f32::NAN == f32::NAN is also false, so the two copies of NAN are not the same thing according to the floating point interpretation. Every copy of NAN is a different thing. It works fine with the definition of partial ordering, it's just that NAN.clone() creates a different object that is not equal. I guess even every time you look at the same copy of NAN it's a different thing, hmm. Weird, but I guess still workable.
Maybe you could argue that f32 doesn't really have a partial order (I would say it's close enough), but even if so, doesn't mean the trait is not a partial order trait, it's just that impl PartialOrder for f32 doesn't do the right thing.
Maybe the point is: If we demand that PartialOrd was a partial order, then it must not be implemented by f64. So in fact PartialOrd describes something else.
Fun fact: if you “phrase” the partial order axioms in a particular way, i.e.
if 𝑎 = 𝑏 then 𝑎 ≤ 𝑏
if 𝑎 ≤ 𝑏 and 𝑏 ≤ 𝑎 then 𝑎 = 𝑏
if 𝑎 ≤ 𝑏 and 𝑏 ≤ 𝑐 then 𝑎 ≤ 𝑐
(i.e. mostly reflexivity got written down in a more sophisticated, but equivalent manner)
then they suddenly become a legitimate way of describing PartialOrd, if you just – syntactically – replace ≤ with <= and = with ==, i.e.
if a == b then a <= b
if a <= b and b <= a then a == b
if a <= b and b <= c then a <= c
Of course, this ignores the fact that the definition of “partial order” does assume “=” to be true mathematical equality and thus in particular an equivalence relation that’s concruent w.r.t. “≤”. (I.e. you can replace equal things with equal things on either side of the “≤”.)
I would like to rephrase what I tried to say earlier:
PartialOrdcould be used to describe a partial order. But then we also must implement PartialEq in such a way that a == a is always true. And then we could also mark our type as impl Eq.
Hence, PartialOrd is
not really defined in a good way to describe a partial order because it demands PartialEq but not Eq,
implemented in cases when there isn't a partial order (such as for f32 and f64).
IIRC I ended up at the rule of a == b ⇒ a.clone() == b.clone(), which works for f32 and anything else I can think of, though that's not sufficient in general and I think it can be at most a SHOULD since there might be types that don't meet it today.
Irreflexivity and transitivity together imply asymmetry. Also, asymmetry implies irreflexivity. In other words, a transitive relation is asymmetric if and only if it is irreflexive. So the definition is the same if it omits either irreflexivity or asymmetry (but not both).
So we need transitivity and either irreflexivity or asymmetry.
Let's try to show that PartialOrd is a partial order:
Checking the docs on PartialOrd, I don't see either irreflexivity or asymmetry. But there is a demand that a < b if and only if b > a:
The comparison must satisfy, for all a, b and c :
transitivity: a < b and b < c implies a < c. The same must hold for both == and >.
duality: a < b if and only if b > a.
Now if we set b to a (which we can, because the "duality" must hold for all a and b), we get:
a < a if and only if a > a. Since PartialOrd::partial_cmp cannot return both Some(Less) and Some(Greater), we can deduce that a < a is always false. Hence irreflexivity is fulfilled (and then also asymmetry), and we have a partial order. q.e.d.
Eh.. alright, technically < is a strict partial order here. But in the context of strict partial orders, the corresponding non-strict partial order is gained by taking true equality into consideration, i.e. you define a ≤ b by a < b || a = b. In other words, the notion of “equality/equivalence” in the context of strict partial orders is mathematical equality, which is – in particular – an equivalence relation. (And also fulfills concruence axioms like: a = b and b < c and c = d implies a < d).
In Rust, there is not implicit, always present, already-defined true equality with these properties that we can use, so discussing the question of whether we have a strict partial order stops making all that much sense once we also want to have a corresponding ≤ relation. (Which we do want in the case of PartialOrd; it’s the method le after all.)
In other words: You cannot define ≤ from < alone, when you have a strict partial order <. Instead, you’d need to talk about the strict partial order <and also the way it relates to the partial equivalence relation ==. (You can define all the remaining operations in terms of these two.)
In order to get all the requirements of PartialOrd, you need to add the following axioms in order to specify how < and == interact:
at most one of a < b, a == b or b < a is true (this axiom is present - implicitly - in the PartialOrd docs, also this axiom immediately implies irreflexivity as you’ve noticed)
a == b and b < c and c == d implies a < d (i.e. the congruence axiom that is missing from the PartialOrd docs)
Now, if you want to, you can verify that having a partial equivalence relation == and a strict partial order < with these two additional axioms is cryptomorphic to having a single, arbitrary, reflexive relation ≤,
using the definitions
(≤ in terms of < and ==):
a ≤ b iff a < b || a == b
and
(== and < in terms of ≤):
a == b iff a ≤ b || b ≤ a
a < b iff a ≤ b && !(a == b)
I.e. verify that using the axioms for < and == described above1, and the definition for ≤, you can derive that ≤ is reflexive, and the definitions of < and == in terms of ≤ are true; and vice-versa, using a reflexive relation ≤ and the definitions of < and == in terms of ≤, verify that < and == fulfill the axioms described above1, and verify that the definition of ≤ in terms of < and == is correct.
1Those axioms were: < is a strict partial order, == a partial equivalence relation, and the two additional axioms
a == b;
// is equivalent to
::std::cmp::PartialEq::eq(&a, &b);
I'm only skimming this thread, and you probably meant semantically, but that documentation is wrong, as discussed previously (for the standard lib docs).
Which is funny, of course, given that AFAIK the whole reason PartialOrd exists is the IEEE 754 floating-point semantics. Is there even precedence for objects that behave like IEEE floats in mathematics? Are they weird enough to not match any more-or-less commonly used terminology?
NULL in SQL has similar semantics but seems more sane in that it embraces true three-valued logic: its "PartialEq" actually returns "Option<bool>" in Rust terms. So NULL == NULL is neither true nor false, it is itself NULL, as in unknown, just like NULL < NULL.
Yes, I did find "partial preorder" which matches, as mentioned somewhere above in this thread.. ah here it is:
Admitted, one cannot really necessarily call this notion
if it isn't even (really, AFAICT) possible to find the definition in the English Wikipedia.
But alas, "reflexive relation" isn't too out-of-the-world either, and that's apparently (according to my interpretation of the docs) what PartialOrd is all about. Of course the alternative interpretation of "if you leave out this NaN element, it's a total order, but NaN is incomparable with everything and not even equal to itself" is a totally mathematical apt description.
Might be more sane; but note that (as far as my mathematical experience goes) three-valued logic is not generally the most common thing used in "mathematics". Your average mathematician would probably be happier with the "transitive relation" or even the "partial preorder".
I accidentally incorrectly simplified the second axiom. It has to be two separate ones
a == b and b < c implies a < c
a < b and b == c implies a < c
(I had applied a way of simplifying congruence that only legitimately works with actual equivalence relations, not with a partial equivalence relation. Sorry for that oversight.)
Also, I only just noticed that the first of those two (well, now three) axioms follows from the second one (or rather from the other two), using the axioms of "strict partial order".
or even the "partial preorder".