Why `sort()` need `T` to be `Ord`?

IDK, I guess the worst part is actually that it calls PartialOrd “partial ordering”, which is so far off that it cannot even be rectified: For Eq and Ord at least the description as “equality” and “total order” is “correct” if you interpret “equivalence” as “equality”, e.g. by reasoning about equivalence classes.

As you pointed out (before editing your comment) “partial equality” is a strange term, too, but at least it’s not misleading.

I would agree (but have to admit I'm not really a mathematician, disregarding my interest in math).

Yes. But if you do that, you could also claim that Ord is a total order, right?

I edited it, because I noticed you referred to Eq (sorry to have lost history now).

That’s what I said, isn’t it?

The point is that if you do that, you still cannot call “PartialOrd” a partial ordering. Only “PartialOrd + Eq” would be a partial ordering, if you interpret “equivalent” values to be “equal”. In-fact this process of considering “equivalent” values to be equal does really only work if you have an equivalence relation, so the PartialEq bound from PartialOrd is not enough.

No problem; I tend to edit posts, too.

No, you said total preorder.

I mean here:

My point was that if we interpret Eq as equality rather than "some equivalence relation", then we could interpret Ord as total order (opposed to just be a total preorder).

I agree.

Didn't we say "preorder" here? Not every preorder is a partial order.

Sure. But I also said

Calling Ord a trait for “total order” is okay if we interpret “equivalent” as “equal”. If we don't do that, then it's not okay. It's a conditional statement :slight_smile: just like your statement

is a conditional statement. Hence my reaction “That’s what I said, isn’t it?”.

By the way, since interpreting “equivalent” as “equal” doesn't even work when there's no Eq implementation, it's more consistent to never adopt this convention, since it couldn't be used to properly describe PartialEq or PartialOrd anyways.

It's a preorder. But if we interpret “equivalent” as “equal” then it (also) becomes a partial order. Again, there's an Eq bound involved, so we can do this step of re-interpreting “equivalent” as “equal” in the first place.

I don't know what you mean by "equivalent" here. There are plenty of equivalence relations on Vec<i32>. You can't say "it just means an equivalence relation" without specifying which equivalence relation you're talking about.

Eq specifically implements semantic equality, which is a particular equivalence relation. It being an equivalence relation on objects is just a requirement on implementations, not the definition of what it means.

Right, I forgot about it (or overread it).

Okay, I totally agree now.

Hmmmm… You mean there would be a mismatch if PartialEq isn't equality but Eq is? Not sure if that'd be so bad… But yeah, I see the oddness.

I'm not sure if that's true. That's because a.partial_cmp(&b) is only allowed to be None if a != b. But two equal objects could still be uncomparable, such as in case of NaN: (Playground). The rules of PartialOrd force us to make the equal (uncomparable) objects be considered non-equivalent.

I could've been more explicit. I mean equivalent under the equivalence relation that is the == method of the Eq trait. (Technically it’s part of the PartialEq supertrait, but without Eq, it’s not an equivalence relation.)

I'd like to give an update of the above summary.

There seems to be disagreement / unclarity whether Eq is (or should be) "the" equality relation or "an" equivalence relation.

Let's distinguish these two cases

Eq is some equivalence relation

  • PartialEq - partial equivalence relation
  • Eq - equivalence relation
  • PartialOrd - a transitive relation (requires implementing PartialEq such that if a <= b && b <= a , then a == b )
  • PartialOrd + Eq - preorder
  • Ord - total preorder or weak order (depending on p.o.v. / semantics)

Eq is equality

  • PartialEq - partial equivalence relation
  • Eq - equality
  • PartialOrd - a transitive relation (requires implementing PartialEq such that if a <= b && b <= a , then a == b )
  • PartialOrd + Eq - ?
  • Ord - total order

In no case, PartialOrd could be seen as partial order.

Note that there is also (still) disagreement on whether PartialOrd + Eq is a preorder if Eq is equality. (See my previous post.)

In other words, equal? :slight_smile:

I find this argumentation circular. You argue that Eq is "equivalence" (rather than equality). But now you said that what you mean by "equivalence" is whatever Eq implements.

Are you questioning the “it's a preorder” or the “(if we interpret stuff as “equal” then it becomes a) partial order” statement?

Note that “a.partial_cmp(&b) is only allowed to be None if a != b” is a requirement that's true for PartialOrd, but for a preorder it's also true that !(a <= b) && !(b <= a) (i.e. the equivalent of partial_cmp returning None) can only happen if !(a == b), and the same thing (but with == being true equality now) holds for partial orders.

You bring up NaN, but I don't quite get the relevance, since f64 does not implement PartialOrd + Eq.

You can only interpret Eq as “equality” if there’s an Eq bound in the first place, so it’s impossible to discuss PartialEq or PartialOrd on its own. So IMO you should just remove those “PartialEq - …” and “PartialOrd - …” lines

PartialOrd + Eq becomes “partial order” in this interpretation, to fill in your question mark.

To precisely describe the thing you gain when interpreting == as equality:

By definition, a == b is always equivalent to a <= b && b <= a (I hope we agree on that).

If a == b now becomes true equality, i.e. a = b, then

  • we already knew a = b implies a == b (by reflexivity in an equivalence relation)
  • we gain the insight that a == b implies a = b

Re-writing this in terms of <= means:

  • a <= b && b <= a implies a = b

which is exactly the antisymmetry axiom of a partial order. Which is the one axiom which distinguishes a partial order from a preorder (which only requires transitivity and reflexivity).

I agree it's a "preorder".

I just couldn't follow how it becomes a partial order if we interpret Eq as equality (instead of some equivalence relation). (But I'm trying hard :hot_face:)

Hmmm, I would say not implementing Eq means I can't compute whether two values are equal. I could still be able to compute if a <trans b, if <trans denotes a transitive binary relation.

Agreed, you convinced me.

I guess my point was that we cannot use PartialOrd + Eq in practice to describe a partial order, because IEEE 754 demands that a != a in some cases, which is contradictory to reflexivity. Yet floating point numbers have a partial ordering.

In other words: I agree now that PartialOrd + Eq indeed describe a partial order if we interpret Eq as equality (just like you said). But Rust forces us to implement PartialEq in the same way as Eq (the Eq trait doesn't even have an eq method). Therefore, we cannot use the traits in std::cmp if we want to implement both a partial order and a partial equivalence.

We're talking about the formal requirements for implementing the traits PartialEq, Eq, PartialOrd or Ord here, so any semantic interpretation of == as some kind of “equality” it kind-of irrelevant, if the goal is just to be precise about the actual “requirement on implementations”, not any (necessarily informal) “definition of what it means”.

In mathematics, equality is a concept that inherently already exists for all mathematical objects. We're trying to specify the properties of an (initially arbitrary) function eq: (&T, &T) -> bool and their relation with other (initially arbitrarily defined) functions like le: (&T, &T) -> bool or cmp: (&T, &T) -> Ordering; there really is no (good) “true” equality to consider anyways, when talking about values in Rust; hence when the goal is to figure out the right set of axioms for these functions/methods of the traits in question (including the method eq itself), it’s quite useful to only use terminology that doesn’t assume the pre-existence of any notion of true equality. Notions like “preorder” are great, because their axioms don’t feature equality, while the axioms of something like “partial order” do feature true equality.

1 Like

But you complained that the docs say:

Ord and PartialOrd are traits that allow you to define total and partial orderings between values

which is precisely about the "definition of what it means".

Indeed, you cannot use the PartialOrd for a partial order, unless the type also implements Eq in a way that reflects “true equality”.

Maybe it helps to distinguish between mathematical equality (which is perhaps/sometimes more like identity in programming, maybe?) and equality in programming (which is more like an equivalence relation in math).

So we should be careful when we speak of "equality" and clarify which of these we actually mean.

Alright. If “total and partial orderings” are imprecise terms that don’t mean anything at all, then the documentation is fine, I guess? (You can’t ever really be “wrong” when using imprecise terminology, right?) I don’t know how people without any mathematical background interpret the colloquial term “partial ordering”. I can on the other hand imagine a lot of useful intuition about the colloquial term “equality”. If the only intuition that people would have about “partial ordering” is to look up the term on Google, which immediately brings up Partially ordered set - Wikipedia, which has not much to do with the precise requirements of PartialOrd (in particular for types that don’t implement Eq), then I stand by my point of complaining about the docs.

1 Like