Add alternative Fin operators for Fin with non-zero size

[jamesmckinna]

The proposed choice of names, involving primes, required one renaming of existing code, and propagation of that new name. But such a change is not a deprecation... so how does one account for this in the CHANGELOG?

Also: I did not yet re-add the various operations and properties of various subtractions originally defined in Data.Fin.Base in PR #1830... suspect that they are really no longer necessary.

REVISED: the following would make use of _ℕ-suc_ were it to be defined

• Data.Graph.Acyclic extensively
• Data.Fin.Properties, to show it does the right thing
• Data.List.Properties for downFrom

[jamesmckinna]

Hmmm. Starting to reconsider the wisdom of all this. It's doable in the style I've advocated, but wondering whether @MatthewDaggitt 's instincts towards deprecating the original functions/properties might be the right track after all. More thinking/investigation needed. The surprising thing is how little used is any of the functionality in Data.Fin.Base, with or without {{NonZero n}} preconditioning.

[jamesmckinna]

I now slightly regret deleting branch issue1800 which supported PR #1837, as there now seem (at least) to be additional knock-on changes from that PR, as well as the much earlier PR #1709, which also touch this one. In those past efforts, I clearly did not pay sufficient attention how much the library is not abstract with respect to the properties of m < n vs. suc m ≤ n, even including various modules under Reflection.* and Tactic.*... so I may yet end up opening another branch/Pr to resolve those first, before returning to this one. It may also shed light on how much work the library really exploits Fin.* structure, and hence how much it would benefit from {{NonZero n}} annotation...

[MatthewDaggitt]

Hi @jamesmckinna, thanks for this and apologies for not keeping up with my replies! What's your current plan?

From my perspective, I think you've convinced me that its significantly more subtle than I first thought when I thoughtlessly opened the issue. I'm happy to drop this from the v2.0 milestone if you think some more time for rumination would be useful?

[jamesmckinna]

As ever, at least two options, no, three:

• do nothing, abandon PR (I'd rather not: probably the worst outcome)
• merge what I have already, modulo CHANGELOG etc. (this is probably the locally-best outcome)
• carry on ruminating, and never reach a stable consensus, while still pushing changes (better than option #0, but suboptimal)

The main issue (for me; not necessarily for the maintainers/the originator of the proposal) is that by pursuing the, I think correct, worker/wrapper factorisation, the code has 'obviously, but trivially' blown up a bit (and I'm not sure if I've even capture every last possible call-site where a NonZero-prefixed wrapper might be helpful), but not I think in a harmful way.

I think perhaps let's try to get the PR into a state where it can be merged+closed, and then see how much use the 'new' functionality actually gets. But as you know, I've let other, useful but more 'trivial' PRs get in the way in the meantime... scatter-gun mentality, sorry!

Where there are potential sources of (fruitful?) exploitation might be in the Tactic/Reflection libraries, but these I have largely left untouched, because they are already highly tuned/optimised. There's a strange function, space, in the RingSolver libraries, with an associated property, space≤′nwhich looks as though it ought to be replaceable by an existing function|property in Data.Fin.Base|Property, but which AFAICT is only used to produce a mapping into the well-founded _<′_ ordering on Nat, in order to be be able to do a wf-recursion in the solver, modulo a lot of inlining. But this is part of the library which I am very reluctant to touch without good reason (except, perhaps, to eliminate this (redundant?) functionality).

[jamesmckinna]

@MatthewDaggitt I've just gone over my own 'thinking' on the topic, and the 13 files touched by this PR.

I've added two more functions to Data.Fin.Base, for the sake of completeness, with the same naming conventions; I've proved no Properties of them... they would simply delegate to the ones for their unprimed counterparts. Updated CHANGELOG.

I'm going to stop there:

• to do more would be to open the can-of-worms of the initial potential task list (REVISED above);
• to do yet more would be to touch Data.Fin.Permutation, which is currently being worked on by @Taneb, so I don't want to touch that;
• to do yet more would be to seriously investigate the possible use-cases of these functions (as discussed above), but I have neither time, brainspace nor bandwidth to undertake that.

So if you find me pushing anything further to this branch without an explicit maintainer request, please shoot me ;-)
(UPDATED: AAARGH! modulo one last tweak... follows below ;-_)

But please DO merge this if it still makes sense to you to do so; I think on balance that it might be worthwhile, because it would enable you (or anyone else) to actually do the experiments/engage in more subtle thinking about the problem.

Hopefully this is the/a 'good'/'locally best' middle way!

[JacquesCarette]

Monumental effort here. Real comments incoming on the issue.

[jamesmckinna]

Thanks @JacquesCarette . Suggest that we still merge this, and then row back on that later on, or should we in fact abandon? I'd rather the former than the latter, but I'm wondering if the effort was, monumental or otherwise, a Quixotic enterprise.

[JacquesCarette]

Definitely should merge. Can't let perfection be the enemy of the good.

[MatthewDaggitt]

Okay, so I really like these additions but I think they make Data.Fin.Base significantly more scary for the beginner/intermediate user. (I'm still very sad that they're not backwards compatible slot ins for the existing versions).

Having been mulling it over, how about we move all the new definitions to a separate module underneath Data.Fin, maybe Data.Fin.NonZeroOps? That way they're still accessible to users, but users won't end up seeing them unnecessarily? That would also mean that we could drop the backticks from all the function names?

[jamesmckinna]

@MatthewDaggitt , thanks for getting back to this one.
While I would perhaps have preferred @JacquesCarette 's suggestion to do this in two stages (merge, then refactor), I'll try to do this sometime between now and the New Year. My plate is a bit full this week, but I am keen to push this over the line.

[jamesmckinna]

... Given that 13 files are touched by this PR, are you (also; further) proposing that a *.NonZeroOps.agda be added systematically throughout, so Data.Fin.Properties.NonZeroOps etc. Suggested naming convention? This is the painful crunchy part of your proposed revision to the PR: all these knock-on, but probably provisional, design+naming decisions. This is the bit I dread (and will need fixing downstream, I suspect).

[jamesmckinna]

Also, I don't want to screw up the commits. What should I do (or do not) about merging in the updates to master that have happened in the meanwhile?

[jamesmckinna]

Re: backwards-compatible slot-ins.
It might be sad that it's not doable, but I think that is part-and-parcel of the costs (rather than benefits) of DTFP, in this instance (because we've changed --- indices occurring in --- the types of operations; something not the case for Data.Nat.Properties). @JacquesCarette 's comments on the original issue perhaps also indicate why we might expect this not to be without cost, just for the proliferation of applications of pred alone.

But perhaps I should say: I don't think it can be done, although the very simplest examples of zero' and suc' show, i think, the lie of the land. But if it could be done, then that would be a good argument for abandoning this approach/PR. But there hasn't been any serious effort on such alternatives, AFAICT.

[JacquesCarette]

Looking at this PR, it might be easier to abandon it and instead redo it "from scratch" using the naming convention that @MatthewDaggitt suggests. It would become a matter of cut-and-paste from this one into new files. Extremely tedious, but not so difficult.

The various Base and Core files are getting quite large already, I think it's a good idea to not make things worse.

(I've just spent 1.5 days refactoring some code where I'm co-author, a lot of it involving splitting things off into smaller files. The call graph is now close to explainable! I do listen to my own advice...)

[jamesmckinna]

Quick naming question before proceeding any further: what do you either if you think should be the names of homogeneous zero and successor? It strikes me that these will always need to coexist with the inhomogeneous constructor versions... the worm, as it were, is already in the apple. Even before anything else were to be added (wherever).

[JacquesCarette]

I've lost track: what's a homogeneous zero? an inhomogeneous zero?

[jamesmckinna]

@JacquesCarette if you look in the revised Data.Fin.Base, I introduce 'homogeneous' to refer to definitions made over the homegeneous telescope (n : Nat) (i : Fin n), although in the spirit of @MatthewDaggitt 's original issue, such things aren't going to be terribly useful without the additional silent qualification by {{NonZero n}}.

Homogeneous zero and suc are precisely what the inhomogeneous constructors end up as under such treatment.

They get used at various points (maybe they could be avoided altogether by some other trickery?) to ensure type correctness of various downstream definitions/properties. In a sense, for me, they are paradigmatic of (the essence) of Matthew's proposal. But I don't see these two special cases as available as slot-in replacements for the real constructors (or can they? not sure! I've perhaps spent/wasted too much time already thinking about this issue/PR to have a satisfactory solution), so already the question comes: what should they be called?

[jamesmckinna]

Actually, after sleeping (though not well) on this, I now realise my thinking has been changing over the course of yesterday's discussion, especially since the suggestion to do this PR over for a third iteration (first with NZ<wrapper>, towards an easy-but-tedious search-and-replace, followed by the \primed version, which simplified and tried to improve that first go, and now the suggestion of a, to my mind, still-worse compromise which would just leave more mess for someone else to clean up later). I think I may simply have run out of steam, and in any case have too much else on my plate right now.

Maybe the New Year (and the one-year anniversary of the original issue) might bring new energy, but I suspect not. @MatthewDaggitt has already indicated that the solution offered to the original issue is not really what he had had in mind, nor what he might have hoped would work. Comments here and on issue #1686 are perhaps a clue that some fresh thinking is required (quite possibly in the form of a direct attack on Data.Fin.Properties and Data.Fin.Base to avoid the 'awkward'/contradictory base cases of some definitions/proofs), but I think I'm not in a good position to offer it.

So if someone else has the ... patience? stubbornness?... to pursue this, I'd be happy for them to cherry pick from this branch, along the lines @JacquesCarette proposes.

[jamesmckinna]

I should revert this commit, and recommit as a separate PR

[JacquesCarette]

I might have the patience / stubbornness to do this.

But I would need to really understand the problem that needs to be solved. First, I think I need to read up on what the original problem was. I'll want to think about it to evaluate the various solutions for myself, afresh. Perhaps a new issue (#1686 seems to be more about the solution than the problem it solves) would help with that?

BTW, I would be very happy if the solution turns out to be what is referred to as the third iteration above. I just don't want to presupposed that.

[jamesmckinna]

Go for it! Happy to share anything I might have which isn't already encoded in the branch, or the various trails of issue comments/reviews etc.

As for the discussion under #1686, this may indeed focus too much on the solution(s) I originally developed/espoused (rather than leaving that discussion under the various PRs)... apologies for more GitHub blundering on my part.

But the top of the issue thread has a fairly crisp summary of Matthew's position: the 'problem' lies at the meeting of constructor-form specification/presentation of (the types of) library functions, and their subsequent deployment at call-sites where the (suc in this instance) constructor isn't discernible directly, but only through {{NonZero n}} instance inference.

As you yourself observed in that discussion, the problem is potentially pervasive (and subtle!) in DTFP, and the general setting ('type-checking modulo') might bring in a raft of possible technologies (frex-like functionality; 'Ford'-style equational presentation of such constructor-form types; tactics for resolving the generated typing constraints; etc.) towards its solution.

For the original applications to Nat and friends, Matthew's solutions were tractable, and with a good payoff, via instance inference; my attempts at extension to the Fin case... perhaps less so.

[jamesmckinna]

Suggest we also remove this PR from the v2.0 milestone.