[ 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... ;-))

No CHANGELOG. If not exactly 'cosmetic'...

[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]

The whole intention behind this PR is to better support generalisation over R when using List#, and specifically the ability to generalise over arguments xs : List# A R correctly.

Unfortunately, this sometime means that some statements involving x # xs fail to generalise correctly wrt the implied/implicit argument R relative to other generalisation sites in the type. My current solution is to nudge the type checker by sprinkling a few {R = R} implicit bindings where needed, but this seems slightly less satisfactory, when the real culprit seems to be the relation _#_

I see two possible solutions:

• delegate to using the explicit fresh operation where needed for disambiguation; but this changes the 'visible'/'legible' API when stating lemmas
• introduce a small additional piece of notation, eg x #[ R ] xs where R needs to be made visible (and for some reason I couldn't seem to do this as syntax...?)

Thoughts? Eg. as

-- Convenient notation for freshness making A (and R) implicit
infix 5 _#[_]_ _#_

_#[_]_ : A → (R : Rel A r) → Pred (List# A R) _
x #[ R ] xs = fresh _ R x xs

_#_ : REL A (List# A R) _
x # xs = x #[ _ ] xs

[jamesmckinna]

Eg if we were to introduce _#[_]_ then this could typecheck as:

Suggested change

	take-# : ∀ n y (xs : List# A R) → y # xs → y # take n xs
	take-# : ∀ n y xs → y #[ R ] xs → y # take n xs

[jamesmckinna]

Similarly

Suggested change

	takeWhile-# : ∀ y (xs : List# A R) → y # xs → y # takeWhile xs
	takeWhile-# : ∀ y xs → y #[ R ] xs → y # takeWhile xs

[jamesmckinna]

Suggested change

	filter-# : ∀ y (xs : List# A R) → y # xs → y # filter xs
	filter-# : ∀ y xs → y #[ R ] xs → y # filter xs

etc.

[jamesmckinna]

Suggested change

	toAll : (xs : List# A R) → x # xs → All (R x) (proj₁ (toList xs))
	toAll : ∀ xs → x #[ R ] xs → All (R x) (proj₁ (toList xs))

[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...

[jamesmckinna]

This is the one glaring wart in the refactoring, but I couldn't find a clean way out of the bottle, other than to introduce the abbreviation pr : x #[ R ] xs. Suggestions welcome!

UPDATED: this seems to be a problem with the relative order in which P gets generalised... But simple-minded permutation of the varaiable block doesn't seem to fix it. Oh well.