Document "latent requirements" of PartialOrd

[gnzlbg]

The PartialOrd docs do not document what is de facto required of trait implementors in order for data structures to work correctly. We should update them!

Per @RalfJung's comment below:

FWIW our conclusion was that we basically already require < to be irreflexive, since that is the only way the following equivalences can be upheld:

• x < y iff x.partial_cmp(y) == Some(Less)
• x == y iff x.partial_cmp(y) == Some(Equal)
• x > y iff x.partial_cmp(y) == Some(Greater)

The docs are not explicitly stating that these equivalences must hold, but it seems very much against the spirit of this trait to allow violations of these equivalences. The fact that PartialOrd: PartialEq is very useful here as it makes the 2nd axiom well-defined.

This post used to say something different. Here is the original post

Why doesn't `PartialOrd` require irreflexivity `!(a < a)` over `<` ? AFAICT `PartialOrd` does not actually express any kind of ordering relation for `<`. For: * a strict partial order on `<`: we need `PartialOrd` + `Irreflexivity` * non-strict partial order on `<=`: we need `PartialOrd` + `Eq` since `==` must be reflexive. * total order: we need`PartialOrd + Eq + Total` Is this an oversight? If not, we should document that `PartialOrd` requires: * irreflexivity: `!(a < a)` as well. That would make `PartialOrd`'s `<` denote a strict partial order on `<`. AFAICT this is actually what was intended, since all the discussions I can find online about `PartialOrd` talk about floats, and floats are strictly partially ordered under `<`, but not non-strictly partially ordered under `<=`, which would fit our current model that floats don't implement `Eq`. --- Also, the docs of `PartialOrd` do not say what `le` (`<=`) and `ge` (`>=`) actually mean. AFAICT they mean nothing for `PartialOrd` in isolation. From reading the source the default implementation is `a < b || a == b`, which would denote a non-strict total ordering over `<=` when `Eq` is implemented. But since `Eq` is not required for `PartialOrd`, I'd guess that those overriding these implementations are allowed to do something else as long as they don't implement `Eq`. It is unclear to me what that "something else" might mean, but the docs should probably say something about this. --- Also, I haven't been able to find any document explaining why things are the way they are, but the fact that `PartialOrd` requires `PartialEq` makes no sense to me, and it doesn't make much sense either that `PartialOrd` exposes `le` (`<=`) and `ge` (`>=`) methods, since as mentioned above, without `Eq`, `le` and `ge` do not express any meaningful ordering relation. It seems that these traits, like all other "operators" traits, mix operator overloading with mathematical semantics: in some cases they are used to express mathematical concepts, like a strict partial ordering relation under `<`, and in some other cases they are used "to provide <= for floats". If anybody has any links to any discussions / documentation about why things are the way they are I'd like to read them, and maybe we should add rationale sections to the docs.

[LukasKalbertodt]

In the RFC thread for is_sorted, @ExpHP mentioned that PartialOrd probably also requires: (a < b) if and only if (b > a) (they called it "the 'notational' axiom").

Irreflexivity is implied by said notational axiom and the semantics of partial_cmp. Simple proof: for irreflexivity to not be satisfied, !(a < a) would have to be false for some a. This means that for some a, a < a would have to be true. Using the notational axiom that means that a > a would have to be true as well (I swapped the two as). But a < a and a > a cannot be true at the same time (this last fact is merely implied by the type Ordering... but I guess it's worth putting it in the docs explicitly).

Thus, instead of adding the axiom of Irreflexivity to the docs, one could also add the notational axiom (which we probably want to add anyway).

---

The docs are also unclear or plain wrong in regards to the provided methods lt, le and friends. The docs say:

PartialOrd only requires implementation of the partial_cmp method, with the others generated from default implementations.

However it remains possible to implement the others separately for types which do not have a total order.

This implies that one has to manually implement lt and friends to achieve a non-total ordering. This is false. In fact it's misleading because lt and friends need to be implemented in a way that has the same behavior as the default implementation. Otherwise partial_cmp would disagree with lt and friends. The docs should explicitly disallow such disagreement between methods. (Since semantics of lt and friends mustn't be changed, the only reason to provide a manual implementation is speed.)

[gnzlbg]

@RalfJung mentioned on IRC:

so x <= y must be (x < y || x == y)

PartialEq is more explicit: "Any manual implementation of ne must respect the rule that eq is a strict inverse of ne; that is, !(a == b) if and only if a != b."

I think that sentence was just forgotten for PartialOrd

That is, the docs should state that ge is equivalent to gt || eq and le is equivalent to lt || eq and that any manual implementation must respect that.

[RalfJung]

(Since semantics of lt and friends mustn't be changed, the only reason to provide a manual implementation is speed.)

Agreed. This is stated explicitly for PartialEq, it seems it as forgotten here.

it doesn't make much sense either that PartialOrd exposes le (<=) and ge (>=) methods, since as mentioned above, without Eq, le and ge do not express any meaningful ordering relation.

I think that's the wrong way to think about it: PartialOrd is only a single operation, partial_cmp. This operation is then used to define <, <=, > and >=. There is no choice left here, the only reason it is possible to override the default implementations (as @LukasKalbertodt said) is to make them go faster.

[RalfJung]

@ExpHP mentioned that PartialOrd probably also requires: (a < b) if and only if (b > a) (they called it "the 'notational' axiom").

Yeah that sounds pretty reasonable. I'd express this as "> is the dual to <", I think that's the common terminology in maths.

I briefly wondered how this relates to antisymmetry... but antisymmetry is a strange axiom in this context. In fact, antisymmetry is impossible to violate! If a < b, then partial_cmp(a, b) == Some(Less), so we already have !(a > b). So, I think we can just drop it. If we require that lt and gt are defined in terms of partial_cmp (or equivalent), antisymmetry will always hold.

(EDIT: This assume !(a < b) is the negated boolean a < b... because I cannot imagine any other reasonable interpretation.)

[gnzlbg]

So, I think we can just drop it. I

Wouldn't we then need to require that if partial_cmp(a,b) == Some(Less) then partial_cmp(b, a) == Some(Greater) or something like that?

EDIT: I see this as just trading one axiom for another. We probably should document the axioms both in term of the comparisons <, ==, ... (which is more easy for some people to understand) and in terms of partial_cmp (which is what everybody has to implement).

[RalfJung]

Wouldn't we then need to require that if partial_cmp(a,b) == Some(Less) then partial_cmp(b, a) == Some(Greater) or something like that?

That's the "notational" (or "duality") axiom: a < b implies b > a.

[gnzlbg]

That's the "notational" (or "duality") axiom: a < b implies b > a.

Aha! Yeah if we add that axiom then we don't need anti-symmetry. Nice!

The wikipedia page on strict partial orders actually mentions this, that one axiom follows from the other two:

* not a < a (irreflexivity),
* if a < b and b < c then a < c (transitivity), and
* if a < b then not b < a (asymmetry; implied by irreflexivity and transitivity).

(just note that we don't require irreflexivity yet)

[gnzlbg]

So to make a more concrete proposal. We currently have PartialOrd specified as:

Trait for values that can be compared for a sort-order.

The comparison must satisfy, for all a, b and c:

• antisymmetry: if a < b then !(a > b), as well as a > b implying !(a < b); and
• transitivity: a < b and b < c implies a < c. The same must hold for both == and >.

Note that these requirements mean that the trait itself must be implemented symmetrically and transitively: if T: PartialOrd<U> and U: PartialOrd<V> then U: PartialOrd<T> and T: PartialOrd<V>.

Including all feedback above, we could change that to (strawman):

Strict partial ordering relation.

The comparison must satisfy, for all a, b and c:

• transitivity: if a < b and b < c then a < c
• duality: if a < b then b > a

that is, in terms of partial_cmp:

• transitivity: if partial_cmp(a,b) == Some(Less) and partial_cmp(b, c) == Some(Less) then partial_cmp(a,c) == Some(Less)
• duality: if partial_cmp(a, b) == Some(Less) then partial_cmp(b, a) == Some(Greater)

The semantics of le (<=) and ge (>=) are defined as:

• le(a,b) == (a < b || a == b)
• ge(a,b) == (a > b || a == b)

The lt , le, gt, and ge methods are implemented in terms of partial_cmp according to these rules. The default implementations can be overridden for performance reasons, but manual implementations must satisfy the rules above.

From these rules it follows that PartialOrd must be implemented symmetrically and transitively: if T: PartialOrd<U> and U: PartialOrd<V> then U: PartialOrd<T> and T: PartialOrd<V>.

Stronger ordering relations:

• partial_cmp is a non-strict partial ordering relation if T: PartialOrd + Eq
• partial_cmp is a total ordering relation if T: Ord

Corollaries: follow from transitivity of < and duality

• irreflexivity of <: !(a < a)

• transitivity of >

• asymmetry of <: if a < b then !(b < a)

• antisymmetry of <: if a < b then !(a > b)

I am not sure if everything does indeed follow properly from duality and transitivity. Even if it does, this is a question that some might have, and even if this is all trivial to prove, I think we should have a "Proofs" section in the docs of PartialOrd with the proofs. Do you think that such a section makes sense?

[LukasKalbertodt]

@gnzlbg Awesome, thank you! A few things though:

(1.)

partial_cmp is a non-strict partial ordering relation if T: PartialOrd + Eq

Are you sure? I don't think transitivity ("a <= b and b <= c implies a <= c") can be derived from the axioms. E.g. if a == b and b < c, then either a < c or a and c could be uncomparable. I don't see how the current axioms prevent a and c from being uncomparable, but maybe I missed something.

(2.)

Strict partial ordering relation.

I would change this to "Strict partial ordering relationS." as the trait adds < and >, two new strict partial ordering relations. Maybe even change it to "Strict partial ordering relations < and >."

(3.)

Maybe we want to explicitly state that lt and friends return false if partial_cmp returns None. Or in general we might want to talk about what returning None means. And maybe add the information implied by Ordering: "At most one of a < b, a == b and a > b is true."

(4.)

transitivity of > is implied by symmetry of ==, transitivity of < and ==, and duality of <.

I don't think you only need duality and transitivity of < here:

      a > b ⋀ b > c ⇒ a > c        | using duality to mirror all relations
⇔    b < a ⋀ c < b ⇒ c < a        | just change the order of the AND operands
⇔    c < b ⋀ b < a ⇒ c < a        | we're done as this is the transitivity of `<` axiom

[gnzlbg]

2. I would change this to "Strict partial ordering relationS." as the trait adds < and >, two new strict partial ordering relations. Maybe even change it to "Strict partial ordering relations < and >."

I was talking here about partial_cmp, not < and > which "follow" from it. I don't know a better way to put it yet, but I wanted to emphasize that partial_cmp is the "relation" that users have to implement. From there it follows that < and > are strict partial orders. I don't know, I find partial_cmp a bit weird to think about.

Maybe we want to explicitly state that lt and friends return false if partial_cmp returns None

So when I wrote the axioms in term of partial_cmp I wrote a < b == (partial_cmp(a,b) == Some(less)). Maybe we should explicitly mention this:

• a < b is partial_cmp(a,b) == Some(Less)
• a > b is partial_cmp(a,b) == Some(Greater)

I don't think you only need duality and transitivity of < here:

Yes you are correct, I ninja edited the post.

("a <= b and b <= c implies a <= c") can be derived from the axioms. E.g. if a == b and b < c, then either a < c or a and c could be uncomparable.

Step by step: "if a == b and b < c implies a < c || a == c" is equivalent to "a < c implies a < c || a == c which is equivalent to "a < c implies a < c or a < c implies a == c" which is "true or false" which is "true". Or what am I missing?

I don't see how the current axioms prevent a and c from being uncomparable, but maybe I missed something.

The only requirement of Eq over PartialEq is reflexivity: a == a. So IIUC that requires a to be comparable with itself.

[LukasKalbertodt]

I was talking here about partial_cmp, not < and > which "follow" from it. I don't know a better way to put it yet, but I wanted to emphasize that partial_cmp is the "relation" that users have to implement. From there it follows that < and > are strict partial orders. I don't know, I find partial_cmp a bit weird to think about.

Mhh, yes that's tricky :/

But as far as I understand it, partial_cmp is not a relation in the mathematical sense. From the Wikipedia article it looks like a binary relation is just a subset of the cartesian product X × Y of two sets. Basically meaning that a relation just says true or false for every pair of members of the two sets. partial_cmp certainly says more than that.

In fact, I think that partial_cmp defines exactly three (disjunct) relations (disjunct meaning that no two of those relations have a member in common). I mean yes, "relation" is also just an English word that would fit here from a non-math standpoint. But since the documentation mentions some exact math terms, I wouldn't use "relation" (which has an exact mathematical definition) in the non-mathematical sense.

Maybe the first paragraph of PartialOrd docs should be targeted at the standard user who is not interested in axioms or exact mathematical terms. Maybe explain it in terms of "comparison"?

Types that can be compared to one another (defines the operators <, <=, => and >).

---

Maybe we should explicitly mention this:

I'd say so.

Step by step: "if a == b and b < c implies a < c || a == c" is equivalent to "a < c implies a < c || a == c" which is equivalent to "a < c implies a < c or a < c implies a == c" which is "true or false" which is "true". Or what am I missing?

I'm not sure about your first step: you say "a == b and b < c" is equivalent to "a < c". I mean it intuitively makes sense but can that be derived from the axioms? As far as I can think it through, you can only show that:

• a > c is false: otherwise a == b ⋀ b < c ⋀ a > c is true, which is equivalent to a == b ⋀ a > c ⋀ c > b (duality and swapping two terms), which is equivalent to a == b ⋀ a > b (transitivity of >), which is false (disjunction of > and == relation).
• a == c is false: otherwise a == b ⋀ b < c ⋀ a == c is true, which is equivalent to b == c ⋀ b < c, which is false (again due to disjunction of < and ==)

So we still have two possibilities: either a < c (what we want to show) or a and c are not comparable. To show that a < c is in fact implied, we'd have to show that a and c are necessarily comparable, right? And:

The only requirement of Eq over PartialEq is reflexivity: a == a. So IIUC that requires a to be comparable with itself.

This only requires everything to be comparable with itself, which doesn't help us because a and c are not the same element.

But again, maybe I'm missing something.

[RalfJung]

@gnzlbg nice first strawman! I overall like it. I think before stating any axioms, however, we should define <, <=, > and >= (or maybe just < and >) in terms of partial_cmp. Otherwise the axioms don't actually mean anything. Moreover, we should spell out what it means to "agree" with PartialEq, I guess we want an axiom like "partial_cmp(a, b) == Some(Equal) if and only if (a == b)"?

partial_cmp is a non-strict partial ordering relation

partial_cmp is a total ordering relation

As @LukasKalbertodt pointed out, these statements are not well-typed: partial_cmp is not a relation (it does not have type fn(T, T) -> bool). Please spell out which relation(s) you mean: <, <=, >, >=?

Corollaries: follow from transitivity of < and duality

I'd add "and from the definition of < et al. in terms of the same partial_cmp"

I'm not sure about your first step: you say "a == b and b < c" is equivalent to "a < c".

This is some kind of congruence statement: Essentially, we demand that a == b implies partial_cmp(a, c) == partial_cmp(b, c), or similar (and also for replacing the second argument).

So maybe, instead of what I said above, the real meaning of "PartialCmp agrees with PartialEq" is

• a1 == a2 and b1 == b2 imply partial_cmp(a1, b1) == partial_cmp(a2, b2), AND
• partial_cmp(a, b) == Some(Equal) if and only if (a == b)

However, these may be too strong for irreflexive equalities? NaN seems fine though (this mandates that partial_cmp(NaN, NaN) == None, but that seems reasonable).

Can we derive one of these axioms from the other? Or find one nicer axiom that implies both of them?

[ExpHP]

So, I've only been half-following this. I'm afraid I'll really only just be adding to the noise; but here's how I feel inclined to look at it:

• We need at least as many axioms as we have methods. This is unavoidable. Most axioms can be as boring as the notational/duality axiom, simply defining one method in terms of another.
• I am fairly certain that all methods of the traits can be defined in terms of <= alone. Is difficult to elaborate right now as I am on my phone, but I picture the directed graph formed by edges from a to b wherever a <= b.
• What are the axioms of <=? I think that for PartialOrd, it's just ~associativity.~ i mean transitivity!

[steveklabnik]

Tagging with @rust-lang/lang; they need to make a call before we can write docs.

[joshtriplett]

Seems reasonable. The docs in this comment seem plausible to me.

Would it make sense to use rfcbot to gather consensus asynchronously?

[gnzlbg]

Is there a recommended way to put up a documment that we could quickly edit for this collaboratively?

It appears to me that after @LukasKalbertodt and @RalfJung comments we are 95 % there, we just need to finish it, and for that it might be better if we would just have something that's "uptodate" and that we can quickly eidt.

[LukasKalbertodt]

@gnzlbg I don't know if that's what you had in mind, but I created a HackMD document from your comment. Everyone can login via GitHub and edit. But it might be better to have a tiny repository where we submit the documentation as PR and we can leave line comments?

[gnzlbg]

@LukasKalbertodt thanks! I worked a bit on it there and this is how it looks now (it would be cool if the tool could create diffs, so maybe a github repo would be better for something like this in the future):

---

PartialOrd Documentation

Strict partial ordering relation.

This trait extends the partial equivalence relation provided by PartialEq (==) with partial_cmp(a, b) -> Option<Ordering>, which is a trichotomy of the ordering relation when its result is Some:

• if a < b then partial_cmp(a, b) == Some(Less)
• if a > b then partial_cmp(a, b) == Some(Greater)
• if a == b then partial_cmp(a, b) == Some(Equal)

and the absence of an ordering between a and b when partial_cmp(a, b) == None.

Furthermore, this trait defines <= as a < b || a == b and >= as a > b || a == b.

The comparisons must satisfy, for all a, b, and c:

• transitivity: if a < b and b < c then a < c
• duality: if a < b then b > a

The lt (<), le (<=), gt (>), and ge (>=) methods are implemented in terms of partial_cmp according to these rules. The default implementations can be overridden for performance reasons, but manual implementations must satisfy the rules above.

From these rules it follows that PartialOrd must be implemented symmetrically and transitively: if T: PartialOrd<U> and U: PartialOrd<V> then U: PartialOrd<T> and T: PartialOrd<V>.

The following corollaries follow from transitivity of <, duality, and from the definition of < et al. in terms of the same partial_cmp:

• irreflexivity of <: !(a < a)
• transitivity of >: if a > b and b > c then a > c
• asymmetry of <: if a < b then !(b < a)
• antisymmetry of <: if a < b then !(a > b)

Stronger ordering relations can be expressed by using the Eq and Ord traits, where the PartialOrd methods provide:

• a non-strict partial ordering relation if T: PartialOrd + Eq
• a total ordering relation if T: Ord

---

[LukasKalbertodt]

@gnzlbg

(it would be cool if the tool could create diffs, so maybe a github repo would be better for something like this in the future)

Yes, diffs and PR-comments would be nice. I created a temporary repository and submitted the current documentation as PR. I'd suggest we could discuss everything there. I already left a few comments on the PR.

I also gave you push access to the repo, so feel free to change things as you like.

[eddyb]

(small note: < is the "strict partial order", and <= the "non-strict partial order" - but the latter also requires Eq - mathematically, the "operators" are the orders, not {partial_,}cmp)

[LukasKalbertodt]

@eddyb I added a comment with an alternative formulation here.

[eddyb]

Looks like C++ went with something a bit more complex. I'm not sure, but it almost seems like they have an Ord + PartialEq combination?

[gnzlbg]

@eddyb The latest paper is P0515r3. The most relevant section for this discussion is probably "Section 2: Design" which defines the following comparison categories as types:

• weak_equality
• strong_equality is a weak_equality
• partial_ordering is a weak_equality
• weak_ordering is a partial_ordering
• strong_equality is a weak_ordering and a strong_equality

The values of the equality categories are:

• weak_equality returns {equivalent, nonequivalent}
• strong_equality returns {equal, unequal} which are converted to {equivalent, nonequivalent} when converted to weak_equality results.

This is very similar to rust: interpret PartialEq::eq -> bool returning true as equivalent and false as nonequivalent, and when Eq is also implemented interpret these as equal and unequal respectively.

The orderings are also pretty similar:

• partial_ordering values are {less, equivalent, greater, unordered} which can be implicitly converted to the weak_equality values as {nonequivalent, equivalent, nonequivalent, nonequivalent}
• weak_ordering values are {less, equivalent, greater} and implicitly convert to:
  • weak_equality values as {nonequivalent, equivalent, nonequivalent}
  • partial_ordering values as {less, equivalent, greater}
• strong_ordering values are {less, equal, greater} and implicitly convert to:
  • weak_ordering values as {less, equivalent, greater}
  • strong_equality values as {unequal, equal, unequal}
  • weak_equality values as {nonequivalent, equivalent, nonequivalent}

The paper is a bit light on math details; maybe some of this is covered in Stepanov's "From Mathematics to Generic Programming" or "Elements of Programming, worth checking this out.

Basically, the paper says that a type should implement _equality if only a == b should be provided, and only _ordering if a < b should also be provided. It also says that it should implement partial_ if values can be unordered, weak_ if a == b does not imply f(a) == f(b), and strong_ if a == b implies f(a) == f(b), where in both last cases "f reads only comparison-salient state that is accessible using the public const members".

The most interesting examples are:

• floats: implement multiple orderings. The default provided by operator<=> is partial_order because of NaN, however a total ordering is available in an opt-in way via the named comparison functions. That is a < b returns the partial order, but std::strong_order(a, b) returns the IEEE total order. The system is flexible enough to support this. It is as if in Rust one could implement PartialOrd::partial_cmp with different semantics than Ord::cmp, and also choose whether the PartialOrdor the Ord implementations map to < (I happen to think that one of Rust's std lib biggest mistakes is mixing operator overloading with mathematical semantics; they are orthogonal concerns that don't mix well).

• CaseInsensitvieString implements weak_ordering because a == b does not imply f(a) == f(b)

[gnzlbg]

Another related concern I have with how the current traits work is that there is no way to express that some PartialOrd relations actually denote a total order. For example, given:

impl PartialOrd<Foo> for Bar { ... }

there is no way to implement Ord<Foo> for Bar.

[RalfJung]

I am confused, of course you can implement Ord...? Or do you mean because it requires Eq?

[gnzlbg]

@RalfJung I've filled an issue in the rfc repo: https://github.com/rust-lang/rfcs/issues/2511

Maybe the explanation there is more clear?

[RalfJung]

Yes, I understand now where you are coming from. Thanks.

[RalfJung]

Cc https://github.com/rust-lang/rust/pull/81198

[zacknewman]

I really like the proposal above by @gnzlbg, but we are still abusing terminology from math. Partial and full equivalence relations as well as partial and total orders are all defined using binary relations on the same set—which is roughly analogous to types. Since the traits core::cmp::{PartialEq, PartialOrd} allow one to talk about two different sets/types though, this means those terms aren't even applicable. After all what does "symmetric" or "reflexive" even mean when the binary relation is on two different sets?

If we use @RalfJung's encoding of a binary relation (i.e., a function, f: T x T2 -> bool, where the "inputs" that get mapped to true represent the binary relation), then I suppose that means we say the pair of functions (f: T x T2 -> bool, g: T2 x T -> bool) is "symmetric" iff for all t_1 in T and t_2 in T2 f(t_1, t_2) ⟺ g(t_2, t_1)?

No clue how one would adapt reflexivity and irreflexivity though. I feel like one can come up with some form of argument that invokes vacuous truths. Something like the function f is "reflexive" on T since it is impossible to come up with a counterexample (i.e., a value t_1 such that f(t_1, t_1) = false). Clearly this is a nonsense though since f isn't even defined on T x T.

[RalfJung]

Indeed symmetry can be defined on "heterogeneous" relations like you say, but (ir)reflexivity just doesn't make sense in general.

[zacknewman]

@RalfJung, should core::cmp::PartialEq require that types T that implement PartialEq<T2> for some type T2 to be either empty (e.g., !) or for there to exist elements/terms/instances, t_1 of T and t_2 of T2, such that t_1.eq(&t_2)? What is stopping all types from implementing that trait? Clearly the motivation of that trait is due to IEEE 754, but at least the binary and decimal formats defined by that have some values that evaluate as equivalent.

[RalfJung]

I am not sure what would be the point of such a requirement.

While f32/f64 are certainly the most prominent examples, the concept of a "partial equivalence relation" (a relation that's symmetric and transitive but not necessarily reflexive) is well established and used throughout the math/CS academic literature.

[zacknewman]

I realize that, but Rust is intentionally not the most "theoretically sound" language (nor should it be). Consequently there not existing some beautiful theoretical justification—as nice as that would be—is not enough reason to not add a requirement. After all, PartialEq doesn't even have the bound PartialEq<Self> on RHS despite clearly requiring such a thing in the interest of ergonomics.

The dilemma I am facing is differentiating between the semantics of a type not implementing PartialEq of itself vs. implementing PartialEq such that eq always returns false. I don't have this problem with most traits. When a type implements a trait, you are not just defining some functionality for that type but in fact imbuing the type with additional structure. This is where using sets as analogs to types breaks down since sets have effectively no structure unlike things like topological spaces or categories.

For example, it is "obvious" why uint does not implement core::iter::Iterator for any type T. There is a sufficient amount of structure that goes along with being an iterator that the difference between not implementing it and implementing the degenerative form of it (i.e., next always returning None) is clear. uints obviously don't have that kind of structure. In contrast, PartialEq is so "primitive" that I am genuinely struggling in gaining an intuition of when a type should not implement it vs. implement its degenerative form.

This is why I suggested the requirement that the type is either uninhabited or have at least two terms (potentially being the same) that evaluate as equivalent. This "solves" this dilemma since there is now a clear distinction between not implementing the trait and implementing its most degenerative form. I cannot come up with a type where not implementing PartialEq has obviously different semantics than implementing it such that eq always returns false. Can you provide one?

Edit

After reflecting on what I said, there are two interpretations of why a type would not implement PartialEq of itself: either the type has some terms that can be interpreted as being "similar", but this "similarity" fails either symmetry or transitivity or the type has no notion of equivalence for any of the terms. It is the latter situation that I am struggling in distinguishing from implementing PartialEq such that eq always returns false. Perhaps this is where my math background is rearing its ugly head and I am conflating extensional equality/equivalence with intentional?

[RalfJung]

I realize that, but Rust is intentionally not the most "theoretically sound" language (nor should it be).

You say that, and then you go on making arguments based entirely on theoretic concerns about the "structure" that a trait imbues on a type. I really don't know how to make sense of that.^^

Usually in partial equivalence relations (but you probably know this), R x x means that x is "valid" in some sense -- i.e., elements such as NaN that are not equal to themselves are considered "invalid" elements. I see no issue with having a type like

struct Invalid;
impl PartialEq for Invalid {
  // just always return `false`
}

So, I guess I don't share your issues with types whose equivalence relation is empty. Yes, there is a trivial partial equivalence relation for each type. However, note that there even is a trivial proper equivalence relation for each type, namely always returning true -- this even satisfies all the conditions for Eq! Would you say that Eq provides "no structure"? The type that picked false does provide more information than a bare type ("an unstructured set") just by virtue of picking this partial equivalence relation instead of any other one that it might have picked. The absence of any interesting structure is still some information about the structure of the type.

FWIW there also is a trivial and fairly canonical (I would say) Iterator implementation for each type that satisfies all the laws, namely always returning None. So I really can't follow your arguments for why you feel that a trait needs to be non-trivial to implement for it to provide meaningful "structure". I am a type theorist more than a set theorist, so I fully agree that structure is important, but I see no problem with a type that decides (via its PartialEq implementation) to have trivial structure. Having "free" instances of a structure is a common theme in algebra / category theory (and indeed "free" is a technical term here).

Can you come up with any concrete problems in real consumers of PartialEq that such a type might cause?

[zacknewman]

I suppose what I meant—but clearly did a poor job in conveying—is that I don't need the super technical encoding of some concept. While I realize having words like "structure" are more technical than others; from the perspective of math, it is very much informal (i.e., I am ignoring any formulation based on first-order logic/type theory of what that term means). I also hope I did not come off as rude or dismissive. Not that it matters one iota what I think, but I very much love Rust and have immense respect/envy for the language team. I hope my comments have not offended/upset you (or anyone else); but if so, I apologize. Any frustration I have is at myself for the difficulty I am having in gaining an intuition of what should likely be a pretty easy concept.

I realize that eq always returning true is also a trivial implementation, but I did not mention it since it "feels" more useful than one that always returns false. As a type theorist, I am sure this absurdly informal terminology is painful; but it is the best way I can convey what I mean in English.

As I said above, I realize that one can easily implement pretty much any trait they want for almost any type; but for some reason, my stupid brain has an intuition as to why one would not want to implement Iterator for something like uint but is having difficulty in justifying why one would define a type that does not implement PartialEq (because it could simply always have eq always return false).

I think we have come to a point where I just need to reflect more because I understand what you mean from a technical perspective that having Invalid implement a trivial version of PartialEq does give it more "structure" than if it were to not implement it at all (i.e., you go from a "set" to a "set with a partial equivalence relation").

I cannot think of a concrete problem for "real consumers" of PartialEq. It seems as though I should have exhibited more patience with myself in ruminating the differences, so I apologize for wasting your time. The subtlety of the additional structure that a trivial implementation of PartialEq provides is just not as "obvious" as the rather "obvious" amount of additional structure one gets from a trivial implementation of a trait like Iterator.

[RalfJung]

No offense was taken, I enjoyed this fun little exchange. :) But I agree that there's not much to go on with here, since sadly we don't have the tech for me to meet you in your brain space where you "feel" why things make sense on way but not the other. I know very well that expressing such intuition in words that make sense to other humans can be hard; I hope in pondering these issues you reach a better understanding that either resolves this concern or leaves you in a better way to express it. :)

[scottmcm]

Clearly the motivation of that trait is due to IEEE 754

I often wish Rust used more PartialOrd + !Ord things. For example, it makes sense to me that Ok(1) < Ok(2) and Err(1) < Err(2), but in Rust it's also true that either Ok(2) < Err(1) or Err(2) < Ok(1) -- and I can never remember which of them. (Is there a good justification for which? Is it really just completely arbitrary? Do people every really use Results as BTreeMap keys to care? How can one be consistent with two contradictory arbitrary choices?)

Admittedly that's a bit of a tangent, but maybe it'll help give you another scenario on which to reflect, Zack.

[RalfJung]

Wow, I had no idea that Result: PartialOrd... looks like it is a derive(PartialOrd), so I assume this is some kind of lexicographic order based on enum variants or so. But I agree just keeping unrelated variants unordered wrt each other would have been a better default... of course then it couldn't implement Ord though.

[scottmcm]

so I assume this is some kind of lexicographic order based on enum variants or so

Yup, that's right. Same as how the only place where the order of the fields in a struct matters is in how it impacts the derive.

[nikomatsakis]

All arguments aside, PartialEq has been stable in its current form for a long time. I'm inclined to say that changes to it have to pass a very high bar, and it seems like there isn't much consensus around this at all. I'd be inclined to close it.

[zacknewman]

My brain decided to just not work for a little bit. Now that I've gotten more sleep, I'm embarrassed by my confusion above. I think there would be some use for a "true equality" trait. I feel like core::marker::StructuralEq is too extreme where effectively the "raw bits" must be the same as opposed to indiscernibility based only on the public API of a type, but that is orthogonal to this.

[RalfJung]

I think there would be some use for a "true equality" trait. I feel like core::marker::StructuralEq is too extreme where effectively the "raw bits" must be the same as opposed to indiscernibility based only on the public API of a type, but that is orthogonal to this.

So you mean, like Eq but unsafe so that one can properly rely on its axioms? TrustedEq, so to speak? I don't know how to make sense of "indiscernibility based only on the public API", that seems hard to pin down.

[nikomatsakis]

Either way, I think this particular issue can be closed.

[RalfJung]

I think there is a lot of valuable information buried in this issue, like this comment. Sadly, the work of actually turning this into new docs for PartialOrd was never done. The intention, I think, is less to change PartialOrd and more to figure out what its true contract is and relate it to well-known mathematical concepts.

[nikomatsakis]

OK, perhaps we can modify the issue title. I'm a bit reluctant to "add new contracts" to PartialOrd (who knows what impls are out there?). At the same time, I think if we can say "what requirements already exist for things to behave properly" and document those, then this is great.

[RalfJung]

Yeah, this issue has gone a long way since it was created, and title / description have not kept up.

FWIW our conclusion was that we basically already require < to be irreflexive, since that is the only way the following equivalences can be upheld:

• x < y iff x.partial_cmp(y) == Some(Less)
• x == y iff x.partial_cmp(y) == Some(Equal)
• x > y iff x.partial_cmp(y) == Some(Greater)
• EDIT: and moreover, partial_cmp is a pure function (always returning the same result for the same inputs)

The docs are not explicitly stating that these equivalences must hold, but it seems very much against the spirit of this trait to allow violations of these equivalences. The fact that PartialOrd: PartialEq is very useful here as it makes the 2nd axiom well-defined.

[zacknewman]

@RalfJung, I find it useful to think of structures of things on a continuum where as one progresses along this continuum, additional properties must be upheld. So in this case, I'll call it the "continuum of equality" where towards one end you have notions like equivalence relations where you don't care about all the properties of equality but only those of reflexivity, symmetry, and transitivity. As you progress further, you then encounter notions of isomorphisms—or whatever the term is in that particular discipline (e.g., homeomorphisms in topology)—which have more properties associated with them than just equivalence. Since math doesn't typically have notions of "public API" or "internals", this is normally enough to model "equality"; however in set theory, one can still progress further and differentiate isomorphisms (i.e., bijections) from equality (i.e., where both sets are subsets of one another).

So where along this continuum does "indiscernibility based only on the public API" lie? Maybe I am mistaken here, but I feel like in Rust the properties one must uphold in relation to a trait are restricted to the public API of that type (unless otherwise stated). Because of this, I find core::marker::StructuralEq too restrictive since it requires the internals to be the same. It is certainly possible for one to achieve this "indiscernibility" without requiring the actual internals to be the same though at least from this "public API" perspective.

As an explicit example:

pub mod equality {
    pub trait Equality: Eq {
        fn equals(&self, other: &Self) -> bool;
    }
}
pub mod rational {
    use core::{convert::Into, num::NonZeroIsize};
    use crate::equality::Equality;
    pub struct RationalNumber {
        num: isize,
        den: NonZeroIsize,
    }
    impl RationalNumber {
        pub fn new(num: isize, den: NonZeroIsize) -> RationalNumber {
            RationalNumber {num, den}
        }
    }
    impl PartialEq<RationalNumber> for RationalNumber {
        fn eq(&self, other: &Self) -> bool {
            self.num.wrapping_mul(Into::<isize>::into(other.den)) == Into::<isize>::into(self.den).wrapping_mul(other.num)
        }
    }
    impl Eq for RationalNumber{}
    impl Equality for RationalNumber {
        fn equals(&self, other: &Self) -> bool {
            self.eq(other)
        }
    }
}

There is no way downstream code can differentiate something like 1/2 from 2/4 using the public API of RationalNumber. The only way one can is via pointer shenanigans which under this perspective would not constitute as a proof since you're in strict violation of this "public API" notion.

Now if one decides to expose a function like fn numerator(&self) -> isize as part of the public API of RationalNumber, then they must either construct the canonical representation of that rational number inside of new—in doing so, they'd now satisfy structural equality too—or do so as part of numerator—and hopefully cache this reduction since it is a rather "expensive" process.

Maybe this is too "niche" though. I just know that people tend to attach more properties associated with equivalence than they should since that equivalence relation really only says something about that type under that specific relation. For example, if ones knows x and y are both "equal" (technically equivalent), it is easy to treat x and y as the same regardless of what you plan to do with them; but that is simply untrue. This in turn can of course lead to invalid programs. I think some people would say that "the side effects" of using x may be different than y despite the two being equivalent. My proposal for a trait like Equality would be that terms that are equal have the same observable "side effects" from the perspective of the entire public API of that type.

For completeness sake, I'd argue that one can continue along this "continuum of equality" and incorporate something like spacetime and have stricter forms of equality than even structural equality where the "raw bits" are still not enough; but we are getting rather "absurd" at this point.

Edit

A cursory Google search led to this admittedly old Reddit discussion. As the type theorist, you likely are better equipped at formulating what drb226 and philipjf are talking about (warning: this concerns Haskell which I know is a different language with different goals than Rust).

[zacknewman]

FWIW our conclusion was that we basically already require < to be irreflexive, since that is the only way the following equivalences can be upheld:

As discussed, I'd hope terms like "irreflexive" would not be used in the documentation since it makes no sense in general; unless you explicitly qualify it with "when Self == RHS, …". I do like explicitly stating those bullet points though.

[RalfJung]

I think "irreflexive" is still a useful term, but we should probably say explicitly that it only makes sense when Self == RHS.

Regarding "indiscernibility based only on the public API", I think I got a rough idea of what you mean, and indeed I think I have seen ways to make that more precise -- but in the interest of not further derailing this thread, I won't reply in any more detail here. :)

[RalfJung]

I created a PR to update the docs: https://github.com/rust-lang/rust/pull/85637