Introduce NonZero to Data.Fin as well

[MatthewDaggitt]

Just noticed we have similar constructor issues in various Fin operations and proofs.

[jamesmckinna]

Oh? I found only pred< in Data.Fin.Properties, and that seems used nowhere else...
EDITED: and ignore that branch... I failed to separate it from all the other commits on pr1698-extended. D'oh.

[jamesmckinna]

Interesting corridor discussion. My eyes are somewhat more open about this now.

[MatthewDaggitt]

In summary we want to avoid arguments of the form Fin (suc n) as that makes it very difficult to use the functions when the Fin index is known to be non-zero but is not of that form, e.g. Fin (n !)...

[jamesmckinna]

Yes, OK. In the first instance, though, moving to .{{_ : NonZero n}} arguments on indices does/would generate a lot of explicit use/mention of pred... maybe that is simply a pain for the library (and its developers) but better for downstream clients? is that an argument for a (more?) disciplined separation of public/private interfaces to modules... with the private interfaces being more dependently-typed/constructor-form index-aware, with the public interface being more destructor-form index focused? In miniature, I guess that was part of the #1709 discussion, with Data.Nat.Properties.Core.≤-pred being precisely such a form...

Sorry for not having had a more nuanced sense of these things until our discussion yesterday. Hmmm.

[MatthewDaggitt]

Yes it would mean more uses of pred, and I agree with your analysis about the cost/gain benefits for devs vs users. One thing to say is that it also makes the proofs slightly harder to read for the users... but I think the gain is usability outweighs that.

As for the more general point, yes that sounds reasonable. Although unfortunately we have no real (enforced) notion of private/public interfaces...

[jamesmckinna]

Worker/wrapper idiom: I'd suggest leaving in the old 'worker' proofs then, and only add new ones expressed in terms ofpred... not least because these latter will most likely be easy 'wrapper's around the former... and then any client module importing these can decide which they need/prefer to use?

[jamesmckinna]

How's this one going?
I've opened a branch on my repo and done some initial experiments with introducing wrapper functions...
... but there is clearly huge client dependency in the library on Data.Fin.* so this might be a big job.
I'll push the beginnings with a view to discussing this and then perhaps moving forward towards a PR on this.

[jamesmckinna]

Hmm. See this branch for the beginnings:

• systematically introduce {{NonZero n}}-qualified wrappers prefixed by NZ for any worker operations which are not homogeneous/uniform in the telescope {n}(i : Fin n), with generic definition NZ<wrapper> {n = suc n} = <worker> (with some interesting exceptions, where the constraints can be further simplified);
• additional infrastructure in Data.Fin.Base: a uniform zero and uniform suc operation, as well as a lot of other stuff besides, in the same idiom as above.

What isn't there yet are:

• operations in Data.Vec.Functional waiting for the -relative issue Use -local consistently for properties #626/PR Resolves issue #509 and resolves issue #626 #1822 to be resolved;
• further deployment of the NZ operations in downstream/client modules (how far can this be pushed? where? why?)
  @MatthewDaggitt would you take a look before I open a PR, to see if this is the kind of thing you had in mind?

Oh... and the CHANGELOG...

[MatthewDaggitt]

Looks good, a PR along those lines would be welcome! But I was actually thinking of making the changes to the original operators rather than just adding the NZ ones. It's a pretty backwards compatible change, and should drastically increase usability!

[jamesmckinna]

So I think I took the view that it was better to add wrapper operations

• for the sake of backwards compatibility (existing code won't break)
• because the new operations/proofs have to use NZ consistently, otherwise things don't typecheck (all kinds of horrible error messages while developing this branch)

Question: where's the usability gain in changing the types of existing code? (my old friend knock-on viscosity...)

[jamesmckinna]

My first PR #1830 to resolve this along the lines sketched above ... led to some controversial naming decisions. Suggest that we try to resolve that discussion here before proceeding with any further commits.

Elsewhere, you've suggested using primes for the 'non-dependent' version of dependently typed functions. Here the situation is (slightly (?)) different, in that we are making distinctions on whether the telescope over which we eliminate is homogeneous/inhomogeneous in its indices... and I haven't elsewhere seen a naming convention for that... so suggestions welcome!

[jamesmckinna]

Over and above the naming issue, do we also, if the spirit of this issue is to taken seriously, need to further expand the library to include 'computation'equational rules for all the consequent uses of pred? Is there a good closed form for eg pred(n !)?

[jamesmckinna]

I will try to get back to this issue and linked PR later this week. Suggest we then close, but with the possibility of subsequent re-opening if there are good reasons to.

[JacquesCarette]

So this feels like the tip of a very large iceberg. It's a symptom of a fundamental "how do we do APIs in dependently-typed programming?" question. Repeating some of the analysis above:

One API uses arguments of the form Fin (suc n), but

In summary we want to avoid arguments of the form Fin (suc n) as that makes it very difficult to use the functions when the Fin index is known to be non-zero but is not of that form, e.g. Fin (n !)...

The flip side is

moving to .{{_ : NonZero n}} arguments on indices does/would generate a lot of explicit use/mention of pred

i.e. replacing a particular shape (on which we can match) with a particular proof (made an instance argument here, but that's ergonomics, not fundamental). The downside is the use of pred.

This feels like it is mainly punting the problem down the road! The pred is only going to reduce if it's applied to something whose shape is known. [And sometimes, that's going to be exactly the right API.]

My feeling would be to split things. This change is making a bunch of modules expose a very large interface, with no guidance to users as to which one to use. I would be tempted to put all of these new functions into *.NonZero sub-modules. One advantage of that would be that all their names could lose the annoying prime suffix.

[jamesmckinna]

Regarding 'splitting': in the spirit of earlier responses to other issues/PRs of mine, I suggest that such a proposal/suggestion be the topic of a subsequent refactoring, My energy for pursuing this one is mostly exhausted by now, so I'd like it to be merged, and then we think again. Or do you regard the 'pushing down the road' as evidence that this approach is a non-starter?

[JacquesCarette]

I'm fine with that (i.e. leave it to a subsequent refactoring). Fair to say that if I believe in this splitting enough, I should be willing to do it myself & not force you to do it.

I don't think this approach is a non-starter. It feels almost as equally flawed as the current one. But, absent even a proposal for something better, all we're left is to try both of these and see what happens. It's just too bad we don't have a 2-layer standard library, with time-tested stuff in the stable layer, and stuff that hasn't been sufficiently tested in practice in an outer layer.

Given the current development processes, best thing to do is to merge this one in as is. Then see how quickly I have energy to refactor.

[jamesmckinna]

I'd be happy with that!

[jamesmckinna]

@MatthewDaggitt what's your current thinking on this (and PR#1847)?

[MatthewDaggitt]

Thanks for the prompt! I'll reply in the PR 👍

[jamesmckinna]

Suggest removing this from the v2.0 milestone.

[jamesmckinna]

See also #1923, #1921. One way to think about the NonZero/'homogeneous vs. inhomogeneous telescope' decomposition of Fins is... to introduce suitable views of those telescopes, and to program against those views. The indicated PRs are... instances of that idea. Exploiting NonZero (of a Fin index) is about saying "under such-and-such view [that the index is suc n for some n], such-and-such consequence becomes available".

Now, @MatthewDaggitt 's objection (barrier to entry for newcomers) applies, perhaps (sigh), in spades to view-based programming in general (cf. @Taneb 's comment on #1921) but ... since at least as early as 2004 is something that I (and Conor, and others) think is an essential contribution of DTFP to programming in general, never mind to writing proofs in stdlib.

[jamesmckinna]

@MatthewDaggitt how attached are you/we to keeping this open?
Besides the various attempts to add the 'homogeneous' constructors to Data.Fin.Base, I don't think any of us have made significant progress either on agreeing the form of a desirable design to resolve this, nor in merging any existing attempt, nor ... anything else in the subsequent 12 months... :-( So suggest we close?

[MatthewDaggitt]

Yup sounds good. The idea was misguided I think.