Data.Nat.Properties.≤-total should be implemented with _<ᵇ_

[Taneb]

It's very slow for ≤-total to decide which constructor to use, especially compared to ≤?. This is an issue using Data.Nat with code generic over a TotalOrder - it's far slower than it could be.

[jamesmckinna]

Given your comment about ≤?, is there an alternative, but still generic, implementation of ≤-total going via Decidable _≤_ rather than TotalOrder?

[Taneb]

@jamesmckinna I don't understand your question. I noticed this problem when I wrote some code generic over a TotalOrder (a record containing a proof that an order is total, i.e. every pair of elements is comparable - ≤-total witnesses this for ℕ). Data.Nat.Properties exports ≤-totalOrder, an instance of this record, using ≤-total.

We could define ≤-total in terms of _≤?_ and ≰⇒≥, but this requires some annoying reordering of Data.Nat.Properties. Here's what this might look like:

≤-total : Total _≤_
≤-total m n with m ≤? n
... | yes m≤n = inj₁ m≤n
... | no m≰n = inj₂ (≰⇒≥ m≰n)

[gallais]

We could define ≤-total in terms of _≤?_ and ≰⇒≥, but this requires some annoying reordering of Data.Nat.Properties.

I think that was the suggestion, and I think it's worth the reorganisation.

[jamesmckinna]

Yes, sorry if my comment was too oblique... @gallais is correct. Cf. my v2.0 refactorings of Data.Nat.DivMod in #2182 ...

Moreover, the proof you offer, modulo the equivalence of _≤?_ and _<ᵇ_, is morally the/a reimplementation of the issue's title, or not?

But I did even wonder if such a (re-)definition should moreover be under Relation.Binary.* (somewhere as Properties or Consequences of being a DecPoset?), and then that proof be instantiated in Nat-specific terms?

Not sure why the reordering of Data.Nat.Properties should be so annoying, other than the fact that refactoring/reimplementation might have such dependency reordering as a knock on consequence?

[jamesmckinna]

@gallais does this qualify as a bug though?

[JacquesCarette]

I'm not sure how much we should change things wrt efficiency. What I mean is that it makes a lot of sense to have (at least) two different definitions of many concepts, one 'conceptually clean' and one 'efficient'. There's quite a number of things in (for example) Data.Rational that would be better off existing in two version. A number already do.

I think it's a false choice to "choose" between certain definitions. Rather we should have parallel hierarchies of definitions (and equivalence proofs). I'd be happy with, say, Data.Rational.Efficient (and same for Data.Integer and likely many more).

There was a reason for that paper on "Realms"!!

[Taneb]

@JacquesCarette in this case, there shouldn't be anything downstream of ≤-total depending on its implementation. If we provide a choice between ≤-total and ≤-total-fast, there'd be no reason for a user to use ≤-total over ≤-total-fast, other than perhaps avoiding a single extra import. I'd be more inclined to accept your argument in cases where we do prove properties using specific implementation details (such as Data.Nat.Base._⊔_/_⊔′_, where we do exactly that)

[gallais]

I would be strongly against -fast suffixes: the fast version should IMO
be the default and we can have a -spec variant for the equivalent but
more proof-friendly version.

[Taneb]

I wasn't advocating using a -fast suffix! I was trying to argue against having two different versions at all

[jamesmckinna]

Again, re:labelling this issue, not sure why this is a bug, while at the same time arguing for improved reimplementation is not refactoring???

[gallais]

Ah sorry, I originally labeled it a refactoring before re-labeling it a performance bug and removing the
refactoring label. I had not noticed you had added it back and so assumed my shaky connection meant that
github had not taken my attempted update into account.

[jamesmckinna]

@gallais 's comment on the PR #2440 suggests that this would be a breaking change...(wrt intensional/reduction behaviour), so: v3.0?

[JacquesCarette]

So while I was probably misguided to rant about spec vs fast on this particular issue, it still seems that there is an issue (but with reduction behaviour). Though I must admit that I'm getting increasingly sad when we do have code that does that (depend on reduction behaviour). Having said that, I do understand that Agda may not be quite ready to deal elegantly with implementation-obliviousness.

[jamesmckinna]

@JacquesCarette writes:

... Though I must admit that I'm getting increasingly sad when we do have code that does that (depend on reduction behaviour). Having said that, I do understand that Agda may not be quite ready to deal elegantly with implementation-obliviousness.

I absolutely agree, and/but what I'm not clear about is whether we should be more diligent as contributors/reviewers in trying to enforce this: eg I'm increasingly fastidious about replacing uses of ⊥-elim and related things (which exploit the definition of negation as an implication, and hence privilege function application as an implicit short-cut definition) in favour of explicit appeals to contradiction etc.

A long time ago, I read a very good piece (where? google can't seem to help me find this... a mailing list somewhere?) by Frank Atanassow explicitly critiquing the use of dependent types in programming precisely because of the almost inevitable temptation/necessity of exposing implementations in types...

... and even longer ago, two authors argued for the use of dependent types in programming precisely because of its ability to (better!) support Wadler's idea of allowing pattern matching to cohabit with data abstraction, not least because such analyses tend/have tended to focus on extensional behaviour (wrt reduction) rather than complexity-sensitive intensional behaviour... so it seems we still have a long way to go ;-)