To give a concrete example how <=
's transitivity is missing in the currently documented axioms:
#[derive(Copy, Clone)]
pub enum O { A, B, C }
use O::*;
use std::cmp::Ordering::{self, *};
impl PartialOrd for O {
fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
match (*self, *other) {
// all values equal themselves, A == B
(A, A) | (B, B) | (C, C) | (A, B) | (B, A) => Some(Equal),
// B < C
(B, C) => Some(Less),
(C, B) => Some(Greater),
// A and C not comparable
(A, C) | (C, A) => None,
}
}
}
impl PartialEq for O {
fn eq(&self, other: &Self) -> bool {
self.partial_cmp(other) == Some(Equal)
}
}
impl Eq for O {}
fn main() {
// violating congruence
assert_eq!(A == B, true);
assert_eq!(B < C, true);
assert_eq!(A < C, false);
// or
// violating `<=`'s transitivity
assert_eq!(A <= B, true);
assert_eq!(B <= C, true);
assert_eq!(A <= C, false);
}
(playground)
this enum fulfills1 all the axioms listed in the documentation for PartialEq
, PartialOrd
and even Eq
, yet behaves quite surprisingly lMO.
@jbe, looking at this example, turns out that without fixing the documentation of PartialOrd
, we don't even get that PartialOrd + Eq
is a preorder (or "intuitively a partial order, if we take Eq
as equality").
1Going through the axioms: The definition obviously defines an equivalence relation that identifies A
and B
. (==
is reflexive, transitive, symmetric.) The axioms listed as "ensured by the default implementation" on PartialOrd
's docs are also fulfilled, and "a == b
if and only if `partial_cmp(a, b) == Some(Equal)`` is true by definition.
This leaves:
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
.
This transitivity is true. The only instance of ... < ...
is B < C
, so there's no way to fulfill the precondition a < b
and b < c
for some a
, b
, c
, in the first place. And duality is also true, since the only instance of ... > ...
is C > B
, which corresponds to the only instance of ... < ...
being B < C