Std implementations of PartialOrd are violating the conditions regarding transitivity and symmetry. And the transitivity requirements are i̶m̶p̶o̶s̶s̶i̶b̶l̶e̶ hard to ensure in a multi-crate ecosystem anyways.

[steffahn]

Std implementations of PartialOrd are violating the conditions regarding transitivity and symmetry.

From the standard library docs:

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 .

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> .

(emphasis mine)

focus on the final paragraph in the quote above and look at the following example

use std::path::Path;
use std::ffi::OsStr;
let c: &str = "c";
let b: &OsStr = "b".as_ref();
let a: &Path = "a".as_ref();

assert!(b < c); // works
// assert!(c > b); // doesn’t compile

assert!(a < b && b < c); // works
// assert!(a < c); // doesn’t compile

(in the playground)

So either the library documentation is off or the implementations are flawed.

And the transitivity requirements are impossible hard to ensure in a multi-crate ecosystem anyways.

Note that, technically, it’s impossible to enforce transitive existence of impls for the trait unless using operands of fully “external” types is completely prohibited:

If I’m writing a crate foo providing a type struct Foo(…); and an impl PartialOrd<i32> for Foo as well as an impl PartialOrd<Foo> for i32, it seems like I’m following the rules set by PartialOrd’s documentation.

If I’m writing a crate bar providing a type struct Bar(…); and an impl PartialOrd<i32> for Bar as well as an impl PartialOrd<Bar> for i32, it seems like I’m following the rules set by PartialOrd’s documentation.

Now, if I’m writing a third crate that imports both foo and bar, then I’ll have impl PartialOrd<Foo> for i32 as well as impl PartialOrd<i32> for Bar, but obviously impl PartialOrd<Foo> for Bar is missing.

In this example, the crates foo and bar each provided an impl where one of the operands, i32, was a type that’s fully external to the crate itself (in the sense that neither the type nor any of its generic arguments are part of foo, or part of a different crate that has the same owners as foo [i32 has no generic arguments to begin with]).

@rustbot label C-bug, T-libs

[sfackler]

Those requirements are for values that are actually comparable.

[steffahn]

@sfackler
Let me repeat what I already stated:

focus on the final paragraph in the quote above

and that final paragraph is

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> .

[sfackler]

Ah right - we already changed that language for PartialEq: #81198. We should make the same change here IMO.

[steffahn]

The solution that PartialEq takes isn’t perfect either. The following example is a bit artificial because I couldn’t find or come up with a real/realistic one (yet). According to those docs, if I have one crate a with

// crate `a`
pub struct A(pub u8);

and a crate b depending on a

// crate `b`, depends on `a`
#[derive(PartialEq)]
pub struct B;

then – AFAICT – this kind of PartialEq implementation would be allowed

// still in crate `b`
use a::A;
impl PartialEq<A> for B {
    pub fn eq(&self, _other: &A) -> bool {
        true
    }
}
impl PartialEq<B> for A {
    pub fn eq(&self, _other: &B) -> bool {
        true
    }
}

However, now the crate a could make a minor version change adding a PartialEq implementation itself:

// in crate `a`, minor version update adding:
impl PartialEq for A {
    pub fn eq(&self, other: &Self) -> bool {
        self.0 == other.0
    }
}
// or equivalently, adding `#[derive(PartialEq)]` to `A`

AFAIK, minor version updates are allowed to add trait impls such as the PartialEq for A one above. But now we have

A(0) == B && B == A(1)

but

A(0) != A(1)

[sfackler]

In what context are those PartialEq implementations actually reasonable?

[steffahn]

This PartialEq documentation also doesn’t disallow something like

struct A(u8);
struct B(u8);
struct C(u8);
struct D(u8);


impl PartialEq<B> for A {
    fn eq(&self, other: &B) -> bool {
        self.0 == other.0
    }
}
impl PartialEq<A> for B {
    fn eq(&self, other: &A) -> bool {
        self.0 == other.0
    }
}


impl PartialEq<C> for B {
    fn eq(&self, other: &C) -> bool {
        self.0 == other.0
    }
}
impl PartialEq<B> for C {
    fn eq(&self, other: &B) -> bool {
        self.0 == other.0
    }
}


impl PartialEq<D> for C {
    fn eq(&self, other: &D) -> bool {
        self.0 == other.0
    }
}
impl PartialEq<C> for D {
    fn eq(&self, other: &C) -> bool {
        self.0 == other.0
    }
}


impl PartialEq<A> for D {
    fn eq(&self, other: &A) -> bool {
        true
    }
}
impl PartialEq<D> for A {
    fn eq(&self, other: &D) -> bool {
        true
    }
}

since it doesn’t disallow a situation where

b == c && c == d && d == a
// but
b != a

// using 
let (a, b, c, d) = (A(1), B(0), C(0), D(0));

---

Similarly, this wouldn’t be disallowed either

struct A(u8);
struct B(u8);
struct C(u8);

impl PartialEq<B> for A {
    fn eq(&self, other: &B) -> bool {
        self.0 == other.0
    }
}

impl PartialEq<C> for B {
    fn eq(&self, other: &C) -> bool {
        self.0 == other.0
    }
}

impl PartialEq<A> for C {
    fn eq(&self, other: &A) -> bool {
        true
    }
}

where we’ll have

b == c && c == a
// but
a != b

// using 
let (a, b, c) = (A(1), B(0), C(0));

---

These kinds of examples can also be used for new examples like in my previous comment demonstrating that semver makes it unclear which crate needs to ensure which kinds of properties: imagine C being in a different crate (together with the two impls involving C). Then a future version of the crate containing A and B could add the missing symmetric impl PartialEq<A> for B implementation and this change introduces a case of b == c && c == a && b != a.

[sfackler]

The documentation states useful properties that code working with partial equality can assume. I don't think it is necessary or even particularly useful to guard against every hypothetically possible malicious or bizarre combination of impls.

[steffahn]

In any case, I agree that the conditions as in PartialEq are better than before and better than the ones in PartialOrd.

[RalfJung]

Ah right - we already changed that language for PartialEq: #81198. We should make the same change here IMO.

That sounds reasonable.

Similarly, this wouldn’t be disallowed either

So the point is that if b == a would type-check then it would be required to hold (and then a != b would be forbidden), but there is a "gap" in the chain and thus this fails to be disallowed?

These kinds of examples can also be used for new examples like in my previous comment demonstrating that semver makes it unclear which crate needs to ensure which kinds of properties: imagine C being in a different crate (together with the two impls involving C). Then a future version of the crate containing A and B could add the missing symmetric impl PartialEq for B implementation and this change introduces a case of b == c && c == a && b != a.

This still requires C to have a clearly weird notion of equality though, doesn't it? Namely it depends on the crate defining A and B and provides a way to (transitively) compare As and Bs in a way that disagrees with directly comparing them. So IMO it is quite clear where the bug is here, even if we don't go through the effort of making the docs completely water-tight in this regard. (We'd have to also state some symmetric cases of transitivity to achieve that.)

[steffahn]

So the point is that if b == a would type-check then it would be required to hold (and then a != b would be forbidden), but there is a "gap" in the chain and thus this fails to be disallowed?

Yes

Namely it depends on the crate defining A and B and provides a way to (transitively) compare As and Bs in a way that disagrees with directly comparing them.

That’s true…

it is quite clear where the bug is here

I agree, intuitively it’s clear

even if we don't go through the effort of making the docs completely water-tight in this regard

My problem is perhaps more the problem that I’m not even sure if there exists a way to make it watertight without contradictions at all. And even if there is a way there might be multiple ways to make this mathematically accurate and watertight. And then one crate creator could intuitively have one understanding of the rules while another one could have a different, incompatible intuition (either intuition might be justified by one of the multiple ways to make the situation formally rigid), with the incompatibility of the approaches resulting in violation of even the minimal set of rules we’d like to have.

TL;DR: What I already said, “semver makes it unclear which crate needs to ensure which kinds of properties”. We have no story of who’s responsibility for what in order to enforce the rules we want to have. The problem seems highly non-trivial because you’d need to consider semver as well as orphan rules. Maybe there’d be a need to establish additional orphan-rule-like restrictions, e.g. the example of a type C being introduced as a means to – indirectly – compare two previously uncomparable types A and B. So this might be disallowed by some “orphan rule”-style convention of not introducing any way to compare two external types A and B even indirectly. Introducing direct comparison in this case is already prevented by ordinary orphan rules preventing impl PartialOrd<B> for A, but the indirect case would IMO be best documented in the docs of the respective traits like PartialOrd.

[RalfJung]

Yeah I agree it's not entirely trivial. Basically, instead of reasoning about the impls that currently exist, you have to reason about the impls that might exist in the future -- "For all legal supersets of the current set of implemented traits, if A: PartialEq<B> and B: PartialEq<C> and A: PartialEq<C>, then ..."

This can be made precise with a "multiple worlds" kinds of model -- coherence already talks about "compatible words" and I recall blog posts along those lines but can't find them right now. The statement in the PartialEq doc must be interpreted not in the current worlds, but in any compatible (future) world.

[m-ou-se]

This was briefly discussed in the library api meeting last week. Our conclusion was that since we already accepted #81198 for PartialEq, we should accept the same change for PartialOrd.

[tczajka]

The problem with how PartialEq conditions have been changed is that now it contradicts the statement that PartialEq implements partial equivalence relations.

See this IRLO thread.

Example code from the thread:

enum A {
    A1,
    A2,
}

enum B {
    B1,
    B2,
}

impl PartialEq<B> for A {
    fn eq(&self, other: &B) -> bool {
        match (self, other) {
            (A::A1, B::B1) => true,
            (A::A1, B::B2) => true,
            (A::A2, B::B1) => true,
            (A::A2, B::B2) => false,
        }
    }
}

This satisfies the PartialEq conditions, but is inconsistent with it being a partial equivalence relation.

Therefore any generic code bound by PartialEq cannot assume that the relation between different types forms a partial equivalence relation, rendering these conditions more or less useless.

I think the solution is to only require these conditions for T: PartialEq<T> and T: PartialOrd<T> and not between different types.

An even more drastic potential solution would be to only have these symmetry and transitivity requirements for Eq and Ord, and not for PartialEq and PartialOrd. I haven't seen a practical use case requiring a partial equivalence relation or a partial order but not Eq or Ord.

[RalfJung]

This satisfies the PartialEq conditions, but is inconsistent with it being a partial equivalence relation.

The notion of a PER is defined on binary relations over some set X. I am not aware of it even being a well-defined question to ask whether a relation on X x Y (like your example) is a PER. Where are you taking that notion from? Your Wikipedia link does not provide a definition that could be applied here.

We should probably clarify the docs to say that "if T == U, then these rules imply that the relation is a PER".

[tczajka]

We should probably clarify the docs to say that "if T == U, then these rules imply that the relation is a PER".

Agreed!

But what is the value of having such rules for T != U != W if they don't even imply anything like PER? They still seem tricky to satisfy when different people implement different parts of this in different crates, even the weaker version.

The rules seem totally useless if you can't even deduce basic equivalence properties between objects, such as "when a = x, a = y, b = x, then b = y".

The notion of a PER is defined on binary relations over some set X.

Agreed. That's one reason why I suggested weakening the conditions to only apply to T == U.

I am not aware of it even being a well-defined question to ask whether a relation on X x Y (like your example) is a PER. Where are you taking that notion from?

I am taking the notion that it should be a PER directly from the first line of documentation of PartialEq, and from the name of the trait itself.

You could in theory have PER between different types: it's just same thing as Wikipedia says, as a relation on (T ∪ U) x (T ∪ U). So my point was: my example violates PER for all possible ways that A: PartialEq<A>, B: PartialEq<B>, B: PartialEq<A> could be implemented, and violates various corollaries of these elements being in some partial equivalence relation.

In another world, one would more reasonably define three traits like this:

• T: EqualityOperator<U> (no requirements, except perhaps that x != y is the same as !(x == y))
• PartialEq : EqualityOperator<Self> (partial equivalence relations)
• Eq : PartialEq (equivalence relations)

Frankly, I don't really see the practical value of even having a trait for "partial equivalence relations". Is there some code that specifically wants partial equivalence relations? I doubt it. Hence my other possible proposal: given that PartialEq is defined on two types, treat it as if it was EqualityOperator and not have any conditions on it.

Having a trait require certain things for T == U only might be a bit strange for generic implementation that doesn't know whether T == U. But perhaps it's fine.

I suspect the only reason the trait was conceived with that name in the first place is that somebody noticed that IEEE-754 floating point equality happens to satisfy this strange concept of partial equivalence relations, not because anything required such a trait specifically.

[RalfJung]

I am taking the notion that it should be a PER directly from the first line of documentation of PartialEq, and from the name of the trait itself.

Your previous post presupposes that there is some definition of "PER on (A, B)", which is not the case.

The stdlib docs also presuppose this, but your example doesn't demonstrate a problem with the stdlib docs, it just repeats the same mistake that the stdlib docs made by using a term outside of the domain it is defined on.

You could imagine defining PER on different types as the same thing as the mathematical PER on the union of T ∪ U

That doesn't seem like a sensible definition to me. Symmetry is impossible to satisfy for elements in the symmetric difference of T and U, meaning those elements would be forced to be unrelated. (Rust enum types are nominal, so mathematically A::A1 and B::B1 are distinct values and the only heterogeneous PERs would be the empty relations.)

I suspect the only reason the trait was conceived with that name in the first place is that somebody noticed that IEEE-754 floating point equality happens to satisfy this strange concept of partial equivalence relations, not because anything required such a trait specifically.

When precedence for such a concept exists in mathematics, I think it would be foolish to deviate from that without a good justification. It's also not at all a strange concept; partial orders are pretty common and partial equivalence relations are the natural name for a partial order that is also symmetric.

---

But anyway, we seem to agree that the docs should emphasize PERs less. It still seems like a useful fact to mention for the common case where T == U.

[tczajka]

But anyway, your ad-hoc extension of PERs to heterogeneous types

It's not "my ad-hoc extension" -- before #81198 it was actually required by the docs.

[RalfJung]

No it was not. The docs never said to consider a relation on (T ∪ U) x (T ∪ U).

[tczajka]

No it was not. The docs never said to consider a relation on (T ∪ U) x (T ∪ U).

I feel like you're just trying to trap me on some word games. They didn't say so in those words, but what they did say mathematically implied it.

The docs implied that if == on T x U is defined, then it must also be defined on U x T, and also (by transitivity) on T x T and on U x U.

In other words, the rules implied that it must be defined on (T ∪ U) x (T ∪ U), because mathematically (T ∪ U) x (T ∪ U) = (T x U) ∪ (U x T) ∪ (T x T) ∪ (U x U).

The requirements also stated that == must be symmetric and transitive for all combinations of these types. Which is the definition of the concept "partial equivalence relation" on (T ∪ U).

The docs also did say explicitly that this constitutes a "partial equivalence relation". And they were correct.

After the change, it's no longer correct except for T = U.

[RalfJung]

They didn't say so in those words, but what they did say mathematically implied it.

No they did not. They used (and use) the term PER in an ill-defined way. That doesn't imply anything, except that the docs need to be fixed.

[RalfJung]

#115386 intends to fix this for PartialEq. If that lands, we can then do the same for PartialOrd.