Skip to content
This repository was archived by the owner on Jun 21, 2021. It is now read-only.

Initial documentation #1

Closed
wants to merge 1 commit into from
Closed

Initial documentation #1

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 34 additions & 0 deletions doc.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
`PartialOrd` Documentation
==========================

[Strict partial ordering relation](https://en.wikipedia.org/wiki/Partially_ordered_set#Strict_and_non-strict_partial_orders).
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


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)`
Copy link

@RalfJung RalfJung May 30, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That makes sense.

* if `a > b` then `partial_cmp(a, b) == Some(Greater)`
* if `a == b` then `partial_cmp(a, b) == Some(Equal)`

and the absence of an ordering between `a` and `b` when `partial_cmp(a, b) == None`. Furthermore, this trait defines `<=` as `a < b || a == b` and `>=` as `a > b || a == b`.

The comparisons must satisfy, for all `a`, `b`, and `c`:

- _transitivity_: if `a < b` and `b < c` then `a < c`
- _duality_: if `a < b` then `b > a`

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>`.
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should also state this.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

If T: PartialOrd<U>, 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<U>, the user needs to implement T: PartialOrd<T>, U: PartialOrd<T>, and U: PartialOrd<U> 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<U>.


The following corollaries follow from transitivity of `<`, duality, and from the definition of `<` et al. in terms of
the same `partial_cmp`:

- 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)`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Additionally, one bullet says asymmetry while the other says antisymmetry

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


Stronger ordering relations can be expressed by using the `Eq` and `Ord` traits, where the `PartialOrd` methods provide:

- a [non-strict partial ordering relation](https://en.wikipedia.org/wiki/Partially_ordered_set#Strict_and_non-strict_partial_orders) if `T: PartialOrd + Eq`
- a [total ordering relation](https://en.wikipedia.org/wiki/Total_order) if `T: Ord`