[ refactor ] use variables more systematically in Data.List.Fresh{.*}

[jamesmckinna]

@jkopanski 's recent #2914 nudged me to think about refactoring the associated modules

• to be more systematic about using variables (UPDATED: it seems the only reasonable way to do this for the whole library is ... little-by-little, at least wrt only 'small' groups of cognate modules?)
• to extend the range of permitted such declarations to also range over Rel and Pred arguments... (elsewhere discussed as a style-guide/library-design issue Policy on generalised variables #697 [ refactor ] Experimenting with variables in Data.List #701 etc.)

DRAFT, for discussion at this stage. Now open for review (including a self-review... ;-))

UPDATED: CHANGELOG now records the new notation x #[ R ] xs

[MatthewDaggitt]

I like these changes! The only comment I have is that according to the style guide, P should not be a variable as it is not involved in the type of the data definition.

EDIT: Ah I see you already commented above. So R is covered under the style guide already. I think the current style-guide rule is a good balance, and I don't see how one could extend it in a principled manner?

[jamesmckinna]

@MatthewDaggitt , you wrote

I like these changes! The only comment I have is that according to the style guide, P should not be a variable as it is not involved in the type of the data definition.

EDIT: Ah I see you already commented above. So R is covered under the style guide already. I think the current style-guide rule is a good balance, and I don't see how one could extend it in a principled manner?

Thanks!

UPDATED: TL;DR: you were right, and I was wrong. The additional commits for the Relation.Unary and Properties sub-modules don't, AFAICT, violate the existing guidelines, so there's no need to entertain any expansion of them.

(IGNORE FROM HERE) I (largely) agree, but in my more 'maximalist' style, I am reaching the point where I would like the style-guide to row back on the two Examples under Types in the style-guide for variable declarations, as follows:

• as you point out, here R is OK, because it is part of the type definition, where P is not;
• BUT, I think we should (at least) entertain the possibility that whenever a type arises as a parameter to a definition, or as a definiendum itself, then so too do all the dependent types which may derive from it.

That is to say, in this example, once we have A in scope as an allowable range of implicit quantification, all of Pred A _, Rel A _ etc. come with it, too... but also (but this may indeed be going too far), also Pred (Pred A _) _ etc. (So there is a first-order/higher-order distinction here which may simply reflect my own instincts/feelings about cognitive overload... as well as bitter experience with unsolved metas and the limitations of Agda's lack of higher-order unification ;-)).

Now, this would be a significant widening of the style-guide recommendations, for sure, so how to keep things under reasonable control so that variable blocks don't proliferate to ridiculous lengths/logical complexity? Two possible 'sensible' (!?) restrictions:

• stay first order, so Pred A _ is OK, similarly Pred (List A) _ under Data.List.* etc. would be OK, but not Pred (Pred A _) _ etc..
• allow Pred etc. variables in Properties modules, but not in Base? (except where already covered as with R in List A R)

The alternative (as we do now, but sometimes it gets very creaky, at least, that was how I felt doing this piece of work) is to be (more) disciplined about using

module _ {P : Pred A _} where

scoping mechanisms, but the creakiness comes, as with this PR when we pass to Properties, I might claim, when you end up with every significant block of functionality requiring such a prefix... at which point, a global variable becomes the 'obvious' choice to make, both for implementation (and the prenex scope discipline which derives from that) and for documentation... "we're going to be talking about predicates and relations in general about the types and functions defined in Base, so it will be convenient to standardise identifiers/lexemes for such things as follows:..."

I'm sure there are good reasons to reject the above ideas, but... testing the envelope!

UPDATED: I think the above can (mostly) stand, but I did at least re-read my own code contributed here, and agree with you. I was being an idiot! P is only really used for filter/takeWhile/dropWhile, so I should take my medicine.

[jamesmckinna]

I think in the interests of review overhead, I won't contribute the corresponding refactoring of Properties to this PR, but it's an obvious next step, unless the sensible thing is to do so now (I'd have to do those changes, of course!).
UPDATED: Properties hardly took any effort to add, so worth it, I think. And potentially the rest to follow for both the Relation and Membership subhierarchies...
UPDATED: now done, with some interesting minor gripes wrt the actual intended generalisation!

[jamesmckinna]

I keep scratching my head as to whether A could be bound implicitly here, or indeed should.
That would obviously be a breaking change to the API, so out-of-scope for this PR, but still...

[gallais]

My suggestions are orthogonal to the variable cleanup but I couldn't help myself.
Happy for them to be ignored though :)

[jamesmckinna]

Any thoughts @gallais @MatthewDaggitt concerning my suggested introduction of x #[ R ] xs as additional notation to disambiguate x # xs when R isn't inferrable?

UPDATED: by inserting appropriate {R = R} bindings, it seems the notation can be avoided altogether, but I've added it nonetheless, and done some experiments using it (sparingly)

[gallais]

I do like that x #[ R ] xs syntax

[jamesmckinna]

Regarding the discussions above about the type of map, I think that on balance it is worth making the breaking change to shift the implicit quantifier from prenex to the subset inclusion on Pred... but I guess that can wait to a followup under v3.0?

It's worth noting that at least as far as stdlib/make test is concerned, the change isn't observable... and indeed, such a change would bring Data.List.Fresh into line with Data.List wrt All and Any... sigh.

Similarly, we should followup this PR with one which is more systematic wrt use of variables in Data.List.* and Data.Vec.*?