Initial documentation #1

LukasKalbertodt · 2018-05-30T06:41:33Z

Just the documentation from this comment.

LukasKalbertodt · 2018-05-30T06:44:59Z

doc.md

+`PartialOrd` Documentation
+==========================
+
+[Strict partial ordering relation](https://en.wikipedia.org/wiki/Partially_ordered_set#Strict_and_non-strict_partial_orders).


We still have the problem that PartialOrd is not a "strict partial ordering relation". The trait defines multiple ones. I'd also add a note about operator overloading because that's what most interesting to most users, I think.

Maybe something like this?

Defines the operators <, >, <= and >= for comparing values, where < and > form strict partial ordering relations.

In general: I think the first two paragraph are a bit too technical for most users. I think it would be a bit better if we first describe the trait in easy terms for the common user. For example, add something like this in the beginning:

In Rust, there are actually two traits related to ordering/comparisons: PartialOrd and Ord where the former is a super trait of the latter. This stems from the fact that many sets contain elements that can be compared, but these comparisons don't necessarily satisfy some nice-to-have properties. The easiest example are integers, like i32. Integers have these nice properties, in particular every integer is comparable to every other integer.

However, there are plenty of ordering relations with elements that are not comparable. For example, the "subset relation" on sets in which, for sets a and b, a < b is true if and only if a is a proper subset of b (e.g. {4, 9} < {1, 4, 5, 9} is true). The problem is that when neither a is a subset of b nor b is a subset of a nor a = b (e.g. {1, 3} and {1, 4}), we cannot sensible compare a and b.

Another popular example are the IEEE-754 floating point numbers. There exist the special NaN value which cannot be compared to any other value.

The PartialOrd has fewer requirements of the ordering relation than Ord. In particular, partial_cmp can return None if two elements cannot be compared. That means that PartialOrd can be implemented for floats and for ordering relations like subset relations.

(this is just a rough sketch to illustrate what kind of information and in what kind of formulation I mean)

Maybe something like this?

Defines the operators <, >, <= and >= for comparing values, where < and > form strict
partial ordering relations.

I think it would be worth it to re-state here that these operators always return bool.

LukasKalbertodt · 2018-05-30T07:26:07Z

doc.md

+
+The `lt` (`<`), `le` (`<=`), `gt` (`>`), and `ge` (`>=`) methods are implemented in terms of `partial_cmp` according to these rules. The default implementations can be overridden for performance reasons, but manual implementations must satisfy the rules above.
+
+From these rules it follows that `PartialOrd` must be implemented symmetrically and transitively: if `T: PartialOrd<U>` and `U: PartialOrd<V>` then `U: PartialOrd<T>` and `T: PartialOrd<V>`.


Not technically false, but from "T: PartialOrd and U: PartialOrd<V>" follow not only "U: PartialOrd<T> and T: PartialOrd<V>", but also V: PartialOrd and V: PartialOrd<T>. I think?

We should also state this.

@RalfJung noticed on IRC that this condition is not enough.

If T: PartialOrd, let a0: T, a1: T, b: U. Then assume a1 < b and b < a2. From transitivity it follows that a1 < a2, but we do not require T: PartialOrd<T> so this is currently not well-typed.

That is, if T != U, and the user implements T: PartialOrd, the user needs to implement T: PartialOrd<T>, U: PartialOrd<T>, and U: PartialOrd accordingly for all requirements (like transitivity) to be fulfilled.

Iff the user then adds an implementation of T: PartialOrd<V>, then it would also need to implement V: PartialOrd<V>, V: PartialOrd<T>, U: PartialOrd<V>, and V: PartialOrd.

fbstj · 2018-05-30T07:46:57Z

doc.md

+- irreflexivity of `<`: `!(a < a)`
+- transitivity of `>`: if `a > b` and `b > c` then `a > c`
+- asymmetry of `<`: if `a < b` then `!(b < a)`
+- antisymmetry of `<`: if `a < b` then `!(a > b)`


should this not be "if a < b then !(b < a) or else it's involving both < & > ?

Additionally, one bullet says asymmetry while the other says antisymmetry

Antisymmetry is wrong and should be deleted. Asymmetry is the correct one.

Antisymmetry is a property of total order only, and is:

if a ≤ b and b ≤ a, then a = b

ExpHP · 2018-05-30T14:24:59Z

doc.md

+- irreflexivity of `<`: `!(a < a)`
+- transitivity of `>`: if `a > b` and `b > c` then `a > c`
+- asymmetry of `<`: if `a < b` then `!(b < a)`
+- antisymmetry of `<`: if `a < b` then `!(a > b)`


I feel the above list could be organized better. It currently requires a bit of staring to realize that one of the properties is for >.

Agreed. And why state irreflexivity and others nit also for >? Also, antisymmetry as given is a property of both < and > in combination, which I don't think is the usual formulation. (Or rather, the usual definition of for > to be the dual of < to asymmetry and antisymmetry as given here are actually the same statement.)

Usually, antisymmetry is defined as "if a <= b and b <= a then a == b"

The line with antisymmetry is wrong and should be removed. @RalfJung is correct about how antisymmetry is defined, and that's a property of total orders, not strict partial orders.

RalfJung · 2018-05-30T19:56:53Z

doc.md

+
+This trait extends the partial equivalence relation provided by `PartialEq` (`==`) with `partial_cmp(a, b) -> Option<Ordering>`, which is a [trichotomy](https://en.wikipedia.org/wiki/Trichotomy_(mathematics)) of the ordering relation when its result is `Some`:
+
+* if `a < b` then `partial_cmp(a, b) == Some(Less)`


Why state these as one-way implications? If anything, it should be the other way around: If partial_cmp == Some(Less), then <. But probably we really want

a < b if and only if partial_cmp(a, b) == Some(Less)

That makes sense.

LukasKalbertodt · 2020-12-19T20:27:20Z

The last activity on this was years ago, I (obviously) don't have time/motivation to work on this further, and it clogs up my global GitHub PR list. Soo... I will close this. Sorry for the notification, everyone!

Create doc.md

9aaaa4f

LukasKalbertodt commented May 30, 2018

View reviewed changes

LukasKalbertodt mentioned this pull request May 30, 2018

Document "latent requirements" of PartialOrd rust-lang/rust#50230

Closed

fbstj reviewed May 30, 2018

View reviewed changes

ExpHP reviewed May 30, 2018

View reviewed changes

RalfJung reviewed May 30, 2018

View reviewed changes

gnzlbg mentioned this pull request Aug 8, 2018

RFC: Add is_sorted to the standard library rust-lang/rfcs#2351

Merged

LukasKalbertodt closed this Dec 19, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Initial documentation #1

Initial documentation #1

LukasKalbertodt commented May 30, 2018

LukasKalbertodt May 30, 2018

LukasKalbertodt May 30, 2018

gnzlbg Aug 2, 2018

LukasKalbertodt May 30, 2018

gnzlbg Aug 2, 2018

gnzlbg Aug 2, 2018

fbstj May 30, 2018

ExpHP May 30, 2018

gnzlbg Aug 2, 2018

ExpHP May 30, 2018

RalfJung May 30, 2018

RalfJung May 30, 2018

gnzlbg Aug 2, 2018

RalfJung May 30, 2018 •

edited

Loading

gnzlbg Aug 2, 2018

LukasKalbertodt commented Dec 19, 2020


		The `lt` (`<`), `le` (`<=`), `gt` (`>`), and `ge` (`>=`) methods are implemented in terms of `partial_cmp` according to these rules. The default implementations can be overridden for performance reasons, but manual implementations must satisfy the rules above.

		From these rules it follows that `PartialOrd` must be implemented symmetrically and transitively: if `T: PartialOrd<U>` and `U: PartialOrd<V>` then `U: PartialOrd<T>` and `T: PartialOrd<V>`.


		This trait extends the partial equivalence relation provided by `PartialEq` (`==`) with `partial_cmp(a, b) -> Option<Ordering>`, which is a [trichotomy](https://en.wikipedia.org/wiki/Trichotomy_(mathematics)) of the ordering relation when its result is `Some`:

		* if `a < b` then `partial_cmp(a, b) == Some(Less)`

Initial documentation #1

Initial documentation #1

Conversation

LukasKalbertodt commented May 30, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung May 30, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LukasKalbertodt commented Dec 19, 2020

RalfJung May 30, 2018 •

edited

Loading