search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
570 stars 233 forks source link

Derived operators in the theory of `Relation.Binary.Structures.IsTotalOrder` #2448

Closed jamesmckinna closed 1 month ago

jamesmckinna commented 1 month ago

The conclusion I now draw from the discussion of Alex Chapman's Zulip issue is that we should move the definitions of _⊓_ and _⊔_ from Algebra.Construct.NaturalChoice.{Min|Max} to Relation.Binary.Structures.IsTotalOrder (and perhaps their properties!?).

Cf. #2247 / #2251 in the algebraic case, where no IsGroup properties were required in defining _//_/_\\_, by contrast with this case, where the min/max operators require the total property even to be definable.

jamesmckinna commented 1 month ago

Hmmm... or perhaps not? #2436 / #2440 seem to turn on the contrast between generic properties of IsTotalOrder, and hand-rolled versions in the case where there is a (more) efficient direct implementation of the operations... so some version of defaulting mechanism... a case for Relation.Binary.Bundles.Biased for the 'generic' case, but specialisable in concrete cases?

(I confess I filed this issue ignorant of the complexities of the API vs. Implementation gymnastics of MinOperator etc. but still might be worth revisiting? Cf DivMod)

MatthewDaggitt commented 1 month ago

Yup, I don't have a coherent story for this, aside from the fact that I deeply don't want to be adding new definitions of operators or relations in anything other than raw bundles...

jamesmckinna commented 1 month ago

Yup, I don't have a coherent story for this, aside from the fact that I deeply don't want to be adding new definitions of operators or relations in anything other than raw bundles...

Quite! In which case I might be tempted to leave this open for now, but it might well end up closed as status:won't fix until/unless we find that "coherent story" and a plan to implement? or even: close now with that label?

MatthewDaggitt commented 1 month ago

Happy with either approach.

jamesmckinna commented 1 month ago

Closing for the time being: more thought required!