Deprecate _≺_ in Data.Fin.Base

[MatthewDaggitt]

I think we already have more than enough definitions of this relation (I think this is the 5th?), and I'd prefer to have less. This is a moderately odd definition with virtually no properties about it.

Anybody object to the deprecating it in v2.0? I'll ask on Zulip as well.

[jamesmckinna]

Did you ask on Zulip? I was beginning to wonder if the #stdlib channel/stream should have a specific > deprecation or > RFC (or something of that ilk...) sub-channel/stream for discussion of proposed changes, esp. wrt deprecation and/or labelled as breaking (cf. issue #1636)

[MatthewDaggitt]

Nope, not yet. Will do so now.

[MatthewDaggitt]

Asked.

[jamesmckinna]

It looks as though, from the deafening silence here, that this deprecation, at least, will (and should!) go through...

[JacquesCarette]

I've never used it, so I won't miss it! 😁

[jamesmckinna]

Whatever happened to this? Removing it eventually will yield some more dependency simplification arising from #1837...

[JacquesCarette]

Looks caught in the lack of available cycles from the maintenance team. I'll assign myself, in a great fit of hope.

[jamesmckinna]

It looks as if, perhaps, this was a relic from early/earlier experiments with Data.Fin.Induction... (?), and recent commits to that make no use of this relation.

[jamesmckinna]

So I now have a branch with this almost working: but the main thing in Data.Fin.Properties is to show this relation equivalent to _<_. Now, if such a relation (and its constructor, coding for a cute inversion principle akin to Data.Fin.Properties.toℕ< ) is to be deprecated, how do I go about deprecating properties of it? I can't seem to avoid getting the deprecation warnings arising from even mentioning the relation symbol.

[jamesmckinna]

I suppose one solution might be to only deprecate the constructor in Data.Fin.Base, and then deprecate the relation+properties in Data.Fin.Properties?

[jamesmckinna]

@JacquesCarette how have you got on progressing a solution? Discuss f2f on Wednesday?

[MatthewDaggitt]

how do I go about deprecating properties of it? I can't seem to avoid getting the deprecation warnings arising from even mentioning the relation symbol.

See the docs on how to turn off these warnings locally in an OPTIONS pragma

https://agda.readthedocs.io/en/v2.6.2.2/language/pragmas.html#the-warning-on-pragmas

e.g.

agda-stdlib/src/Data/List/Solver.agda

Line 10 in bc9c1b6

{-# OPTIONS --warn=noUserWarning #-}

[jamesmckinna]

It's a bit unfortunate that such an OPTIONS pragma can only go at the top of the module, and not permit selectively turning off the warning just in the Deprecations section at the bottom of Data.Fin.Properties. Seems a slightly unsatisfactory state of affairs. Ah well. Ready for review now, even for merging, I claim.

[jamesmckinna]

Funnily enough, I don't want this relation in the library any more than anyone else, but the refined analysis of my new, private, deprecated proofs perhaps suggest that it (once might have?) met a need: when you want to invert toℕ {n} knowing n. That is, it's a view of an ℕ-value m such that m < n as being in the image of toℕ {n}... but still, murder your darlings! ;-)

[JacquesCarette]

I have totally stalled on all my coding work. All my time in the last couple of weeks has gone into preparing talks, meeting a couple of paper deadlines and meetings with various people. Right now, I have a lot of reviewing of my student's work to catch up on. [But I'm doing some productive procrastination by reviewing my backlog of agda-stdlib emails.]

[jamesmckinna]

Never one to row back on work I've invested time in, but I've started to wonder whether this is the interesting relation on Nat, and it's all the (multiply) primed versions of < which should go; < is the conceptually prior one, with its primed version optimised for the proofs of WF induction (plus it's more flexible on open terms, being closer to an interval type than being anchored at 0...).

But this one set for deprecation is the one relation which encodes a view/records how to invert the toNat function... which is what makes it 'interesting' (to me at least).

This is why I would have made a bad assassin... the temptation to show sympathy towards my intended targets. Ah well.

[jamesmckinna]

I'm considering re-opening this issue... in view (sic) of my comment above, and the recent work I've been doing on PR #1287, for mediating between Nats satisfying k <ᵇ n and the corresponding i : Fin n such that toℕ i < n. But as with some other recent work on views, pushing the development down the tree to Data.Nat.Relation.Binary might be the way to go... but advice welcome (and sought!) on the best way to proceed.

[JacquesCarette]

As I said on another issue: as long as it doesn't end up in Data.Nat.Base, I'm quite happy to have alternatives in stdlib. Data.Nat.Relation.Binary seems like a good place indeed.