Clarify upfront that PartialOrd is for strict partial orders

[Muon]

Fixes #140654.

[rustbot]

r? @Mark-Simulacrum

rustbot has assigned @Mark-Simulacrum.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[Mark-Simulacrum]

I'm going to move this to the libs-api agenda -- maybe we can find someone better suited to review this. It's not clear to me from the description in the issue (#140654) whether this is actually a semantic change or not in what we're promising -- it seems like it is maybe not, based on the diff, but I'm a little confused why we didn't land on this when initially landing the docs here.

[Muon]

I do not believe this a semantic change. That would require the changed sentences to be normative, but that's impossible unless f32 and f64 are not meant to be PartialOrd, since their <= is already not a partial order.

Also note that the docs later clarify that this is indeed for strict partial orders only: https://doc.rust-lang.org/std/cmp/trait.PartialOrd.html#strict-and-non-strict-partial-orders

[traviscross]

cc @hanna-kruppe @RalfJung @tczajka @BartMassey @quaternic @rust-lang/lang

[RalfJung]

I think this PR is a bad idea. The prefix "strict" for partial orders is used to distinguish < and ≤ on e.g. numbers. PartialOrd has both < and ≤, so it doesn't make sense to say that it is specifically the strict or non-strict version of any partial order.

[hanna-kruppe]

While the trait does not require all implementations to have reflexivity, if you do want to implement a partial order that is reflexive (e.g., subset relation) then PartialOrd is the right trait for it. So at least the change to the module level docs seems misleading in context:

Ord and PartialOrd are traits that allow you to define total and strict partial orderings between values, respectively.

Code that is generic over T: PartialOrd can't assume reflexivity, and since equality is partial as well, the usual way of flipping between < and <= doesn't really work. Making this "what can I know about an arbitrary impl PartialOrd" angle clearer could be useful, but may be better achieved by applying the following suggestion from #140654 directly:

The docs should make clear upfront that reflexivity is not required.

I know what reflexivity is, but I'm not confident I would infer that the passing mention of "strict partial order" if I didn't know it already. (I’d probably be a bit confused for the reason @RalfJung explained)

(Spelling out more corollaries is useful IMO, but I haven't checked the one added here.)

[mathisbot]

The doc mentions:

Trait for types that form a [strict partial order](https://en.wikipedia.org/wiki/Strict_partial_order).

In fact you cannot say a set (here, the set of all possible values of a type) form a partial order.
However, you can say a set and a binary relation form a partially ordered set.

PartialOrd actually is implemented for types that:

• Are strictly partially ordered with < (and the conjugate >)
• Verify some properties with <= (and the conjugate >=) that do not allow to say it is neither strictly nor weakly partially ordered. <= defined as such isn't even an order (mathematically speaking).

So I am joining @RalfJung on his point.

However, the corollary is in fact true (using the duality of </> and properties 4/5).

[Muon]

I think this PR is a bad idea. The prefix "strict" for partial orders is used to distinguish < and ≤ on e.g. numbers.

"Partial order" on its own always refers to a relation like ≤ on numbers (i.e. reflexive, antisymmetric, and transitive), so the original sentence is definitely misleading.

PartialOrd has both < and ≤, so it doesn't make sense to say that it is specifically the strict or non-strict version of any partial order.

This is an argument against having the current sentence too.

While the trait does not require all implementations to have reflexivity, if you do want to implement a partial order that is reflexive (e.g., subset relation) then PartialOrd is the right trait for it. So at least the change to the module level docs seems misleading in context:

Agreed, but then I'm not sure how to concisely describe what precisely PartialOrd is for in that context, whereas a correct implementation of Ord definitely produces a total order, in that (modulo equivalence) <= is reflexive, antisymmetric, transitive, and connected. Though I did propose this change because implementing PartialOrd correctly does give you a < that is (modulo equivalence) a strict partial order.

In fact you cannot say a set (here, the set of all possible values of a type) form a partial order. However, you can say a set and a binary relation form a partially ordered set.

In my experience, when we say "X forms a partial order", this is short for "the usual order on X is a partial order".

<= defined as such isn't even an order (mathematically speaking).

Agreed, which is why I reported the issue and made the PR.

---

In summary, I think we should at least agree that the original wording in the docs is wrong?

[RalfJung]

In my experience, when we say "X forms a partial order", this is short for "the usual order on X is a partial order".

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

I am not particularly attached to the current wording. 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. The first sentence explaining PartialOrd should probably avoid referencing any particular mathematical notion.

[traviscross]

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. The first sentence explaining PartialOrd should probably avoid referencing any particular mathematical notion.

It seems best to me to describe this explicitly, i.e. to say in the documentation that usually the term partial order would require reflexivity, but that PartialOrd does not, and give an example to demonstrate the difference. This might be similar to what it already does here, perhaps, but maybe framed somewhat differently.

[BartMassey]

@traviscross The floating NaN example you linked is, as far as I can remember, the only irreflexive "PartialOrd" defined anywhere in std? Maybe we should instead indicate that PartialOrd implementations should be reflexive, but we carved out an exception for floating types for ergonomic reasons? I'm not sure there would be any real consequences of going this route, except better expressing intent.

[Muon]

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

[RalfJung]

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

I don't think that reflects the intent of this trait. Is is indeed truly okay for for this relation to not be reflexive.

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

Yeah that makes sense.

[rustbot]

⚠️ Warning ⚠️

• The following commits have merge commits (commits with multiple parents) in your changes. We have a no merge policy so these commits will need to be removed for this pull request to be merged.

  • 7455dbc

  You can start a rebase with the following commands:

  $ # rebase
  $ git pull --rebase https://github.com/rust-lang/rust.git master
  $ git push --force-with-lease