About LawfulOrd

Stream: std4

[François G. Dorais]

What should LawfulOrd actually be? This was briefly mentioned in another thread. The current version in Std.Classes.Ordering seems to run against other usages of Lawful* in at least two ways:

1. The current version applies to a function cmp : α → α → Ordering rather than an instance of Ord α, which is just a wrapper around such a function. This seems to be against other such classes such as LawfulBEq which is about an instance of BEq α rather than a function beq : α → α → Bool.

2. The current version of LawfulOrd only requires symmetry, the extension TransOrd additionally requires transitivity, neither requires that equality is tight in the sense that cmp x y = eq → x = y. In other cases, Lawful* is not the greatest common denominator but rather "least common generalization". Using that guidance, it would be better if the symmetry-only version to be called SymmOrd, then extended to TransOrd as it is now, and finally LawfulOrd should require tight equality on top of symmetry and transitivity.

Of course, there are arguments that warrant going against prior usage. That LawfulOrd and TransOrd use a function cmp : α → α → Ordering rather than an instance of Ord α makes these classes more nimble. There is also an argument that Lawful* should actually be the greatest common denominator rather than everything but the kitchen sink.

Personally, I like all the options here with no preference for one or the other, but we can't have it every way. That said, I do like some uniformity and a mix of all these options is not uniform at all.

[Gabriel Ebner]

The names are indeed misleading there. TotalBLE says it requires a total order, but then omits all axioms for the order. I also think that the name LawfulCmp implies a linear order (since LawfulBEq excludes "non-Hausdorff" equivalence relations as well).

[François G. Dorais]

To play devil's advocate, LinearCmp would be much clearer in actual meaning.

Returning to angel's advocate, for typical development process LawfulCmp can be assumed to have all the typical properties I could need, just like any other Lawful* class.

[François G. Dorais]

PS: Just trying to clarify why this case is difficult in my mind, I don't mean anything special by "devil" and "angel".

[Gabriel Ebner]

Practically speaking, I don't think we can buy anything by weakening transitivity or reflexivity. Most of this "lawful" zoo is pointless busywork in my eyes.

The only generalization that I can see practical applications for is weakening antisymmetry (and analogous properties). We often want to e.g. sort on one field, or use an id field for indexing, etc. Having LawfulPartialBEq (refl.+trans.+symm.), LawfulPartialOrd ("defined by a total preorder," there must be some slick way to say this), LawfulHashable (LawfulPartialBEq + equivalent elems have the same hash), etc., helps with that.

[pcpthm]

There is two different potential meaning of Lawful:

1. fun a b => compare a b = .lt satisfies some order laws (such as a partial order)
2. [LE α] [LT α] and a ≤ b ⇔ compare a b ≠ .gt a < b ⇔ compare a b = .lt.

I think the current LawfulBEq has meaning (2) because it is not about general equivalent relation, rather it requires BEq α aligns with Eq α.
One benefit of (2) is that additional constraints (totality, transitivity) can be added as additional class instance requirements like [PartialOrd α] or [TotalOrd α].

[Mario Carneiro]

I'm open to renaming the classes if they seem confusing. I don't really want to take a stand on what LawfulOrd should mean, and these classes exist primarily as internal things for std to be able to state its invariants.

[Mario Carneiro]

Gabriel Ebner said:

The names are indeed misleading there. TotalBLE says it requires a total order, but then omits all axioms for the order.

To be fair, it is actually an order that is total. It just isn't anything else.

[Mario Carneiro]

Linear order and total order are often used interchangeably, but the former suggests that transitivity is an axiom more strongly IMO

[Mario Carneiro]

But this kind of bikeshedding over what the classes "mean", or whether cmp should be a regular argument or a typeclass arg to LawfulCmp, are something I would like to avoid. These classes have the shapes that are required for the use cases that exist in std. We talked in the other thread about maybe making RBMap take its cmp argument via typeclass instead of explicitly, and if we do that then LawfulCmp would also change to match.

[Mario Carneiro]

One other point of possible confusion is that when we say a relation is "symmetric" we usually mean R x y -> R y x, and that is not the kind of symmetry that LawfulCmp is talking about. The requirement of LawfulCmp is more like "this comparator induces an order coherently".

[Mario Carneiro]

Personally, I think LawfulBEq is not well named. (I would like us to get to the point that we can call it DecidableEq, but we aren't there yet.) LawfulX in my opinion should refer to the weakest requirements under which reasoning is possible, something close to "well formed". I think we should expect the "default case" for BEq is that it represents an equivalence relation, i.e. Setoid. Asking for equality on-the-dot is quite often too much to ask for in programming contexts, so I'm skeptical that LawfulOrd meaning a comparator that induces a (transitive, antisymmetric) linear order will get much use in data structures, although it might show up in instances when you happen to have this stronger property.

[Gabriel Ebner]

Yes, I also think that an antisymmetry-less version could be very useful.

[François G. Dorais]

I agree with everything that has been said. After some greping, I noticed that with the exception of LawfulBEq, all of the Lawful* classes in core are exact characterizations. For example, LawfulFunctor, LawfulApplicative, LawfulMonad are all unambiguously what they should mean. So perhaps the issue is that Lawful* shouldn't be used in contexts where it's not obvious what that means. So neither LawfulBEq nor LawfulOrd should exist because the meaning is too ambiguous?

Since Leo appears to be in favor of Gabriel's redefinition of DecidableEq, the issue with LawfulBEq might disappear on its own in core lean4. In the mean time, perhaps Lawful* should be avoided in std4 unless the meaning is unambiguous? Does that sound like a reasonable conclusion?

[Mario Carneiro]

I think that still leaves open the question of what to call LawfulCmp though. I don't think SymmCmp is a good name because I don't think symmetry has the right connotation in this context, even though the axiom itself can be called a kind of symmetry. What about OrderedCmp, in the sense "comparator that induces an order"? Although if it is replaced with a theorem about an Ord implementation then OrderedOrd doesn't make a whole lot of sense.

[François G. Dorais]

How about OppCmp? (It might help to rename Ordering.swap to Ordering.opp at the same time.)

[François G. Dorais]

OrderedCmp doesn't make sense to me since the Condorcet pattern satisfies the axiom:

  | a | b | c |
a | = | < | > |
b | > | = | < |
c | < | > | = |

[Gabriel Ebner]

I think a key part in this confusion is the meaning of the word "order". From what I can tell, Mario doesn't regard transitivity as a key requirement for orders.

[Gabriel Ebner]

since the Condorcet pattern satisfies the axiom

Or for anybody who can't read diagrams: a < b and b < c but c < a.

[Mario Carneiro]

Gabriel Ebner said:

I think a key part in this confusion is the meaning of the word "order". From what I can tell, Mario doesn't regard transitivity as a key requirement for orders.

This is why I said the naming question is hard. It's just a relation. (Actually this one axiom is enough to at least prove that .eq is reflexive and .lt is irreflexive.)

[Mario Carneiro]

but it does have orderish names like .lt as a result of its return type

[François G. Dorais]

This is called a complete simple directed graph, or a tournament, but that's irrelevant. I have no good suggestion. Maybe ProperCmp? It has the same issue as LawfulCmp but at least there are no other uses of Proper* as far as I know.

[François G. Dorais]

What about DirectedCmp?

[François G. Dorais]

To me, that suggests that every comparison has only one direction.

[Mario Carneiro]

Unfortunately Directed already has a meaning in order theory and it's not what we want

[Mario Carneiro]

What about OrientedCmp? Kind of similar connotation but the nearest math word is not used in order theory

[François G. Dorais]

OrientedCmp sounds great to me!

Do you mean Directed in the sense that any two elements have an upper bound? I don't think that confusion would occur in this case since any preorder arising from a comparison function must be total, so any subset is automatically directed.