Clarify that PartialOrd does not give a partial order by Muon · Pull Request #140779 · rust-lang/rust (original) (raw)

I rarely encounter such terminology and would consider it sloppy. The typical thing people say in this case is "X is a poset".

Oh, it's definitely sloppy! But not any more than saying "X is a poset" :P

Picking the <= relation as the "canonical" one and identifying PartialOrd with <= is insofar justified as it is typical convention in mathematics to assume a "<=" relation and then freely use the other symbols as well as derived notions. But ofc sans reflexivity, PartialOrd is not actually a partial order. I don't think there is a standard term for a relation that's transitive but may not be reflexive.

Well, I tried to keep the mathematical correspondence by identifying PartialOrd with < (which it does promise is a strict partial order), but it seems like it might be best to dispense with it.

The first sentence explaining PartialOrd should probably avoid referencing any particular mathematical notion.

I suspect people look to PartialOrd mainly as a way of providing <, <=, > and >=. Perhaps the docs should begin with that in mind?

Maybe we should instead indicate that PartialOrd implementations should be reflexive, but we carved out an exception for floating types for ergonomic reasons?

I think calling out the exception would be good. However, I am worried that it might be misunderstood as a logical requirement with one weird exception. Maybe we should say something more like this:

"Despite its name, PartialOrd does not guarantee that <= is a partial order, because <= is not required to be reflexive. But if Eq is also implemented, this does imply that <= is reflexive and thus a partial order. In other words, to require T to be partially ordered, write T: PartialOrd + Eq."

or maybe

"Despite its name, PartialOrd does not guarantee that <= is a partial order, because <= is not required to be reflexive. However, <= is reflexive if == is reflexive, and vice versa. Thus, to require T to be partially ordered, write T: PartialOrd + Eq."

For completeness, here's the justification:

Proposition: In a compliant implementation of PartialOrd, <= is reflexive if and only if == is reflexive.
Proof: Let x be a value of the type. Since x <= x if and only if x < x || x == x, and < is irreflexive, we have x <= x if and only if x == x. Thus <= is reflexive if and only if == is reflexive. ∎