Irrelevant instance arguments for _<_

[jamesmckinna]

So: (DRAFT)

• issue Possible Regression at fromℕ< #1988
• the discussion around Should the constructors of Data.Nat._≤_ be declared as instances? #1951
• ditto. regarding An alternative to #1698 #1709 and friends
• @MatthewDaggitt 's heroic work on Switch Positive/Negative/etc. to use irrelevant instance arguments #1581 RFC: changed _/_ and _%_ to use irrelevant instance arguments #1538 etc.
• etc.

lead me to conclude that we should add (!?) an irrelevant-instance version of LessThan to Data.Nat.Base, along the analogy with NonZero, and forever after use this relation for 'computational' appeals to _<_, such as in the (old/refactored; mea culpa) definition of fromN<...

... the only question being whether this can already be achieved by back-porting Positive etc. to Data.Nat, as any instance of LessThan m n (sic) defined in terms of _<ᵇ_would eventually reduce to one of Positive k for some k? or else defining Positive in terms of LessThan?

[Taneb]

It's possible to define LessThan in terms of NonZero and _∸_, as well, which avoids having to implement new instances

[jamesmckinna]

Ah!? ... I think I'd been going from _<ᵇ_ being a builtin primitive in Agda.Builtin.Nat, but then of course so too is _-_... (before being renamed to _∸_ in Data.Nat.Base). Hmm. Thanks for the nudge!

[JacquesCarette]

I found that working with things that were in terms of _<ᵇ_ to be quite difficult to work with, as they made it super unclear what I needed to 'nudge' to get things to reduce further. Basically because they had already reduced to things that were so incredibly far from the original "question" (involving fromN<) that I just gave up.

For my examples, I suspect that a version using _∸_ would have made 'semantic sense' to me.

In the end, I refactored absolutely everything to not use _<_ at all. [I was formalizing a notion of 'interval' in an Enumerable set. There are so so many potential design choices, it's quite ridiculous.]

[jamesmckinna]

Hmmmph, yes, I share your frustrations. If we can prove (we do!) that vanilla _<_ is Irrelevant, then why should we worry about whether arguments of that form are used strictly or non-strictly? But it seems we must, because back-end erasure / run-time efficiency is not the only consideration, we want also to improve compile-time type-checking efficiency. And it would seem that there are regression tests out there to detect my introduction of overly aggressive/strict approach to matching on such proofs.

And so the further I go with #2000 , the more I end up thinking that it can all be reduced to having moved the former definitions in now-deprecated Data.Nat.Properties.Core (introduced to break a dependency cycle) back into Data.Nat.Base. And reverting the former changes to Data.Fin.*... sigh.

That's (seems to be) a completely defensible position, to me at least (but not, seemingly, to prior authors/maintainers of the library? their insistence on the separation between Base and Properties seemed absolute), because Data.Nat.Base already introduces the datatype definitions of _≤_/_<_ (and their smart constructors), so adding the two inversion principles seems 'harmless', 'virtuous' even (I don't think of these as 'properties' as such; one-step inversions of inductive families, like their simply-typed counterparts, eg head and tail, are simply 'functions' on the raw data).

I might tidy up what I've done, and then not pursue this too much further. The questions there regarding DivMod seem more subtle than I quite appreciate at the moment... but it does seem a weird detour (to me) to have to go via _≤″_ in order to be able to eventually erase the equation defining division-with-remainder, if fromℕ< can be restored to its former irrelevant glory. But it seems as though that is actually a separate issue for a separate PR.

[jamesmckinna]

As for the 'semantic sense' regarding _<ᵇ_ and _∸_, the latter has bitten me a couple of times, because it, too, is non-strict in its first argument (when the second is zero). So in order to observe NonZeroness, sometimes an additional pattern-match is required. Whereas _<ᵇ_, which is similarly non-strict in its first argument (when the second is zero), nevertheless immediately returns a matchable constructor form, because Boolean...

... so even my enthusiasm for @Taneb's solution via _∸_ has been ... qualified somewhat.

UPDATED: PR #2000 is now based on _<ᵇ_ and seems to be a bit smoother than going via NonZero. Moreover, I didn't need a separate record declaration for LessThan (because T true is already a record?).

[jamesmckinna]

@JacquesCarette comments welcome on the (at-present) slightly more long-winded definition of fromℕ< now. I'm sure that lots of things could be further streamlined, but the PR is an exploration of some the choices.
TL;DR: the function is now (once again!) irrelevant in its _<_ argument, and extensionally equivalent to a version fromℕLessThan which uses an irrelevant instance of LessThan.

But it remains perhaps debatable whether any of this helps at all...

[jamesmckinna]

NB for @JacquesCarette : from my perspective (partial/biased), it is actually (now) easier to understand _<ᵇ_ via _<_, precisely because the new 'smart' constructors/pattern synonyms z<s and s<s are in harmony (both in form, and in strictness) with the clauses defining _<ᵇ_ (instead of the, to my mind, nonsense indirection via suc _≤_), whereas, as above, the appeal to _∸_ goes via an even-less-strict pattern analysis (as well as being a function with a complicated (in)equational theory). So I'd be interested to learn if it were possible to (re-)make a streamlined definition of interval for Enumerables which wasn't quote as painful as your previous attempt(s)?

[JacquesCarette]

I will dig into this, but after the POPL deadline. I've got tons of paper proofs that need formalized (they are almost all written in detailed equational style as it is, so it is feasible.)

[JacquesCarette]

As commented on the code itself, it looks nice. I have now added an explicit task on my list to re-try my experiments with Enumerable.

[jamesmckinna]

Any update on Enumerable?

[JacquesCarette]

Sorry, not yet. My time slices are still thin...

[jamesmckinna]

I'm (now) less committed to working towards getting #2000 in sufficient shape for merging into v2.0, but I'm definitely still interested in this issue, for basically two reasons:

• (general) the earlier issue Deprecate _≺_ in Data.Fin.Base #1726 regarding thinning down the profusion of definitions of _<_ on Nat;
• (specific, but related) whether an irrelevant definition of DivMod might thereby be obtainable without going via --with-K and the UIP-derived definitions based on _≤″_... which feels as though it would be some sort of win (would it, though?), because we wouldn't have to maintain parallel implementations of DivMod,... possibly dispense with _≤″_ altogether, cf. Redefines Data.Nat.Base._≤″_ #1948 ... etc.

[jamesmckinna]

So... before (thinking about) closing this issue, which has led to a lot of subsequent re-thinking of things, on my part at least, I'm left with a open design/implementation question: where the library as it stands (eg Data.Digit) uses (variations on)

• True (n <? numeral)

as a precondition on functions (either as an implicit argument, or better, as an irrelevant instance to resolve by search), can/should we instead simplify to the computationally more efficient

• T (n <ᵇ numeral)?

NB this is distinct from cases such as count or filter etc. on List/Vec, where we really need the decision, and its subsequent compilation to an if-then-else in the backend...

(... considering lifting this out as a fresh issue/nudge towards a possible PR. )

[JacquesCarette]

On the latest design question: I have no current opinions. I have not looked around that part of the design space at all. [Sometimes a null answer is better than the feeling of speaking into the void.]

[jamesmckinna]

Well in fact, besides Data.Digit, there is only Data.Nat.Show, Data.Fin, Data.Fin.Show, and various (Co)Data.*.Literals, so while it might be practically important in marshalling to-and-fro numerals, the footprint isn't big enough to be worth separate effort beyond dealing with #2218 ... so closing this now.