Total equality relations as `std::cmp::Eq<Rhs>`

[dvdhrm]

Is there a particular reason Eq and Ord do not support arbitrary right-hand-side types just like PartialEq and PartialOrd?

I have been trying to extend the documentation of std::cmp and there is a huge mix of mathematical references and rust terminology, and not all of it makes sense. A lot of the mathematical terminology is defined on homogeneous relations and have no obvious definition for heterogeneous relations. @RalfJung has previously improved some of the docs to define transitive and symmetric by referring to conditional impls (e.g., if A: PartialEq<B> and B: PartialEq<A> then a == b implies b == a).

By extending this approach, most of the properties of homogeneous relations can be extended to heterogeneous relations, and nicely fall back to their homogeneous counterpart if the right-hand-side is itself. There is one exception, reflexive behavior is non-trivial to extend for arbitrary right-hand-sides. I assume this is the reason Eq and Ord require homogeneous relations.

Fortunately, reflexive behavior is not the only way to define equivalence relations or total orders. Requiring homogeneous orders to be total implies that they are reflexive. And the total property is defined for heterogeneous orders, unlike reflexive.

So could we extend Eq and Ord to support a Rhs generic-type argument and change the requirement to total rather than reflexive?

Especially for new-types or smart-pointers, I find myself implementing PartialEq<INNER>. Deref often alleviates this, but only where auto-deref applies. Collections like hashmap currently require K: Borrow<Q> to allow searching with key of different types than the stored key. This could be replaced by K: Eq<Q> and avoid the borrow-requirement.

[tczajka]

The current conditions of symmetry and transitivity for PartialEq between different types don't really correspond to the mathematical idea of a (partial or not) equivalence relation.

In mathematics, the idea behind (partial or not) equivalence relations is that they split the universe into equivalence classes, and regular mathematical symmetry and transitivity conditions ensure that. Whereas PartialEq's version of symmetry and transitivity conditions do not.

For example, with PartialEq's conditions you may have a = b = c = d ≠ a (where a and c are of type A, b and d are of type B).

But the docs don't actually claim that this is a partial equivalence relation between different types, they only (correctly) claim that PartialEq<Self> is a partial equivalence relation. So PartialEq<Rhs> between different types is actually a misnomer that is with us for historical reasons.

[dvdhrm]

@tczajka

For example, with PartialEq's conditions you may have a = b = c = d ≠ a (where a and c are of type A, b and d are of type B).

You sure? The docs of PartialEq (PartialEq in std::cmp - Rust) contain:

• Symmetric: if A: PartialEq<B> and B: PartialEq<A>, then a == b implies b == a; and
• Transitive: if A: PartialEq<B> and B: PartialEq<C> and A: PartialEq<C>, then a == b and b == c implies a == c.

This contradicts your example, doesn't it?

[tczajka]

@dvdhrm

This contradicts your example, doesn't it?

How so? I believe this does not contradict the example.

[dvdhrm]

@tczajka

How so? I believe this does not contradict the example.

You have:

• a, c of type A
• b, d of type B
• a == b, b == c, c == d, d != a

This implies (because you compare the values):

• A: PartialEq<B>
• B: PartialEq<A>

With the Symmetry rule you get:

• b == a
• c == b
• d == c

With the Transitivity rule you get (set C to A or B respectively):

• d == b (d == c and c == b implies d == b)
• d == a (d == b and b == a implies d == a)

This contradicts d != a.

[tczajka]

@dvdhrm

With the Transitivity rule you get (set C to A or B respectively):

• d == b (d == c and c == b implies d == b)

You don't get that conclusion. The conclusion you get is: if B: PartialEq<B> then d == b

But in my example I only need to have A: PartialEq<B> and B: PartialEq<A>. Imagine B does not implement PartialEq<B>.

[dvdhrm]

@tczajka

You don't get that conclusion. The conclusion you get is: if B: PartialEq<B> then d == b

You are right. Sorry!

Going back to the initial question: Does that prevent us from supporting Eq and Ord with arbitrary Rhs?

[tczajka]

@dvdhrm

Does that prevent us from supporting Eq and Ord with arbitrary Rhs?

If Eq<Rhs> doesn't provide you any guarantees about equivalence classes (just like PartialEq<Rhs> doesn't), why not just use PartialEq<Rhs> where you want to use Eq<Rhs>?

Edit: Oh I suppose Eq<Rhs> would guarantee compatibility with Hash. That might make sense. It would be simpler to require that Hash is compatible with PartialEq<Rhs> instead, but that's not backwards compatible.

[dvdhrm]

@tczajka

If Eq<Rhs> doesn't provide you any guarantees about equivalence classes (just like PartialEq<Rhs> doesn't), why not just use PartialEq<Rhs> where you want to use Eq<Rhs>?

Right. But doesn't the same apply to the current situation with Borrow<Rhs> in the standard collections? So why would it be problematic for Eq<Rhs> but not for the current way we use Borrow<Rhs>?

Is it because the docs of Borrow require x.borrow() == y.borrow() to yield the same as x == y? One could interpret this to mean if A: PartialEq<A> then B: PartialEq<B>.

So, would something like this help for Eq:

• If A: Eq<A> and A: Eq<B>, then B: Eq<B> (or just A: Eq<B> requires A: Eq and B: Eq)

This would ensure that equivalence classes are retained, since you must be able to compare values in their respective class.

[tczajka]

@dvdhrm

So, would something like this help for Eq:

• If A: Eq<A> and A: Eq<B>, then B: Eq<B> (or just A: Eq<B> requires A: Eq and B: Eq)

I think this would probably work for the hash table lookup use case.

But it would still not give the property that this is compatible with a global equivalence relation across types. You might still have a = b = c = d ≠ a for four different types connected by Eq.

[steffahn]

There’s also prior topic(s?) on this question

Why don't `Eq` and `Ord` have a `Rhs` parameter (anymore)?

I see that way back (pre-1.0) when Stabilize cmp by aturon · Pull Request #20065 · rust-lang/rust · GitHub was merged, it removed the Rhs type parameter from the Eq and Ord traits but not from the PartialEq and PartialOrd traits: However, RFC 439 that it was apparently implementing specifically proposed a Rhs parameter for those traits. Neither in the discussions around the RFC nor those around the stabilisation PR can I see very much that explains why the parameter was removed: all I have f…

(don’t ask me why the preview doesn’t properly render)

[RalfJung]

@tczajka

The current conditions of symmetry and transitivity for PartialEq between different types don't really correspond to the mathematical idea of a (partial or not) equivalence relation.

In mathematics, the idea behind (partial or not) equivalence relations is that they split the universe into equivalence classes, and regular mathematical symmetry and transitivity conditions ensure that. Whereas PartialEq's version of symmetry and transitivity conditions do not.

In mathematics, these notions are only defined for homogeneous relations, i.e., for the case of T: PartialEq<T>. For that case, PartialEq's version of symmetry and transitivity do imply that we have a partial equivalence relation.

It makes no sense to ask whether A: PartialEq<B> is a partial equivalence relation, the question is ill-typed.

Your example shows that we can have a sequence of relations that compose to a homogeneous relation that is not reflexive. But this can only happen if the relation of "which of the involved types do implement PartialEq on each other" is not itself an equivalence relation, which is a kind of broken situation to begin with. Arguably B is a "nonsense" type if it doesn't even have a PartialEq with itself.

@dvdhrm

Fortunately, reflexive behavior is not the only way to define equivalence relations or total orders. Requiring homogeneous orders to be total implies that they are reflexive. And the total property is defined for heterogeneous orders, unlike reflexive.

Could you spell out exactly what you mean here?

[tczajka]

@RalfJung

In mathematics, these notions are only defined for homogeneous relations, i.e., for the case of T: PartialEq<T>.

In the usual formalization of mathematics (set theory), you don't talk about relations on types, you talk about relations on sets. If you have a set A and a disjoint set B, there is also the sum set A ∪ B. There is no problem formalizing what I was saying in mathematics.

Sure, you can argue that you prefer type theory as a foundation of mathematics and refuse to talk about unions of types, but that just distracts from the point I was making. Regardless of the mathematical notation, I think my point is well defined and unambiguous.

My point can be translated by saying that PartialEq isn't required to represent any equivalence relation on the sum of the sets representing the types involved (i.e. it can't be extended to one), and in particular there are no equivalence classes on the sum of the sets.

Another way to say this is that the relation isn't required to be transitive across types along a sequence longer than 2. So the transitivity requirement across types is degenerate and not that useful.

[steffahn]

@tczajka

If Eq<Rhs> doesn't provide you any guarantees about equivalence classes (just like PartialEq<Rhs> doesn't), why not just use PartialEq<Rhs> where you want to use Eq<Rhs>?

Something I point out in the linked other thread is that Ord would have reasonable extra requirements even for a A: Ord<B> relationship (i.e. that partial_cmp never returns None ^[1]) and due the the super trait relationship Ord: Eq, making Ord support the heterogeneous case would need us to make Eq support it as well.

---

1. whether an extended Ord like this would be particularly useful is a different question ↩︎

[dvdhrm]

@RalfJung

@dvdhrm

Fortunately, reflexive behavior is not the only way to define equivalence relations or total orders. Requiring homogeneous orders to be total implies that they are reflexive. And the total property is defined for heterogeneous orders, unlike reflexive.

Could you spell out exactly what you mean here?

Assume Eq is extended to Eq<Rhs> and we drop the reflexive requirement and instead add:

• If A: Eq<B>, then for every a in A there must be a b in B so that a == b (i.e., the relation is (left-)total).

The totality of A: Eq<A> would imply reflexive. So we would have a solid definition of Eq<Rhs> that falls back to the previous properties if Rhs = Self.

The symmetry-requirement would also imply right-total behavior if B: Eq<A>.

@RalfJung

Your example shows that we can have a sequence of relations that compose to a homogeneous relation that is not reflexive. But this can only happen if the relation of "which of the involved types do implement PartialEq on each other" is not itself an equivalence relation, which is a kind of broken situation to begin with. Arguably B is a "nonsense" type if it doesn't even have a PartialEq with itself.

So how about the docs in PartialEq recommend PartialEq<B> requires PartialEq<Self>? This would prevent the known weirdness and unexpected outcomes, wouldn't it?

@steffahn

There’s also prior topic(s?) on this question

Thanks a lot! I failed searching for Eq and Ord, but apparently lots of background.

[RalfJung]

@tczajka

In the usual formalization of mathematics (set theory), you don't talk about relations on types, you talk about relations on sets. If you have a set A and a disjoint set B, there is also the sum set A ∪ B. There is no problem formalizing what I was saying in mathematics.

There is also no problem formalizing it in type theory. But the question isn't "can you formalize this", the question is about standard terminology. Every single time I have seen a definition of symmetry, it worked like "given some set A and a relation R ⊆ A x A, ...". I think it is fair to say that the terminology only applies to the homogeneous case. (And note that the choice of A matters for some of these notions, like reflexivity: the same set R ⊆ A x A can be reflexive for some A and not reflexive for a larger A'. So while set theorists like to pretend they are in a completely untyped world, that is not entirely true. The precise term would be "R is an equivalence relation over A" -- it is meaningless to ask whether R is an equivalence relation without specifying A. So for equivalence relations, standard math is definitely restricted to the homoegenous case.)

@tczajka

Another way to say this is that the relation isn't required to be transitive across types along a sequence longer than 2. So the transitivity requirement across types is degenerate and not that useful.

That is an interesting observation! So maybe it would be a good idea to extend this requirement in the PartialEq docs to an arbitrarily long transitive chain?

@dvdhrm

So how about the docs in PartialEq recommend PartialEq<B> requires PartialEq<Self>? This would prevent the known weirdness and unexpected outcomes, wouldn't it?

Is that sufficient to imply that an arbitrarily long transitive chain behaves as expected?

[dvdhrm]

@RalfJung

@dvdhrm

So how about the docs in PartialEq recommend PartialEq<B> requires PartialEq<Self>? This would prevent the known weirdness and unexpected outcomes, wouldn't it?

Is that sufficient to imply that an arbitrarily long transitive chain behaves as expected?

Hard to pin down what "behaves as expected" means, given that a lot of the (previous) discussion revolves around lacking terminology for properties of heterogeneous relations.

(edit: the following sadly does not hold)

I think it would prevent a0 = b0 = c0 = [...] = a1 = b1 = c1 = [...] chains to diverge, because you would now be allowed to compare all elements, except in the final domain. And once you form a circle, you would be able to compare in all domains.

[tczajka]

@RalfJung

The precise term would be "R is an equivalence relation over A" -- it is meaningless to ask whether R is an equivalence relation without specifying A.

The set is well specified. What I meant was that despite the symmetry and transitivity requirements, PartialEq implementations for multiple types might still not correspond to any possible partial equivalence relation on the union of the disjoint sets representing the types involved. That set union is your A set. It's perfectly valid mathematical terminology and consistent with what you're saying about having to specify a set.

@RalfJung

That is an interesting observation! So maybe it would be a good idea to extend this requirement in the PartialEq docs to an arbitrarily long transitive chain?

It doesn't work with the crate system for a chain of 4 or more types.

Suppose you add an analogous requirement for 4 types: If A: PartialEq<B>, B: PartialEq<C>, C: PartialEq<D>, A: PartialEq<D>, a==b, b==c, c==d, then a==d.

Now types B and D may be implemented independently by two completely unrelated crates. Both of those crates only have to know about A and C, they don't have to know about each other. So there is no way to say which of the two would be responsible for violating this property.

It works with 3 types because for at least one of these types, the crate implementing it must know about the other two.

@RalfJung

@dvdhrm

So how about the docs in PartialEq recommend PartialEq<B> requires PartialEq<Self>? This would prevent the known weirdness and unexpected outcomes, wouldn't it?

Is that sufficient to imply that an arbitrarily long transitive chain behaves as expected?

No, it's not.

You may have a == a, b == b, c == c, d == d, a == b, b == c, c == d, but a != d.

[RalfJung]

@tczajka

Suppose you add an analogous requirement for 4 types: If A: PartialEq<B>, B: PartialEq<C>, C: PartialEq<D>, A: PartialEq<D>, a==b, b==c, c==d, then a==d.

Now types B and D may be implemented independently by two completely unrelated crates. Both of those crates only have to know about A and C, they don't have to know about each other. So there is no way to say which of the two would be responsible for violating this property.

This shows that if A1, A2 are types from other crates that cannot be compared with each other, you shouldn't add a type B that can be compared with both. That seems like a sensible requirement to me?

@tczajka

You may have a == a, b == b, c == c, d == d, a == b, b == c, c == d, but a != d.

a == b, b == c should imply a == c (since a, c: A and we require A: PartialEq and therefore the transitivity statement kicks in). Or not?

Can you pick variable names that indicate the type? Currently this is all super cryptic to read.^^

[tczajka]

@RalfJung

@tczajka

You may have a == a, b == b, c == c, d == d, a == b, b == c, c == d, but a != d.

a == b, b == c should imply a == c (since a, c: A and we require A: PartialEq and therefore the transitivity statement kicks in). Or not?

Can you pick variable names that indicate the type? Currently this is all super cryptic to read.^^

I meant: a: A, b: B, c: C and d: D, with 4 different types. Each of those types implements PartialEq<Self>, and yet you can get that, so the answer to your question was: no, it's not sufficient to require PartialEq<Self> to get arbitrarily long transitivity.