List of wrinkles in `Data.List.Properties`

[MatthewDaggitt]

Various things spotted during https://github.com/agda/agda-stdlib/pull/2355/ that require breaking changes:

• head-map should take an explicit rather than an implicit f
• zipWith-comm should be generalised to take two functions f and g.

[mildsunrise]

thanks! noting some other inconsistencies i spotted while writing it:

• concat-map should take an explicit rather than implicit f
• map-∘ should take explicit rather than implicit f and g
• reverse-map should be named map-reverse
• properties in the alignWith section (with the exception of cong) should take explicit rather than implicit f
• foldr-cong (and foldl-cong, if #2355 is merged in its current state) should only take functional equality, not propositional equality
• drop-all and take-all should take implicit n and xs, since they can usually be inferred from the passed proof
• concat-++ should return concat (xs ++ ys) == concat xs ++ concat ys (i.e. the symmetric proof)
• concat-[-] should be removed in favor of concatMap-pure

[jamesmckinna]

Not sure about the third point regarding fold*-cong: currently Data.List.Properties is strongly biased towards PropositionalEquality, and as with #2360 , we maybe need a more systematic approach to making (all of) those Properties more Setoidal...

[mildsunrise]

currently Data.List.Properties is strongly biased towards PropositionalEquality

hmm, that looks like a separate problem to me? my point is that all other current congruence proofs in Data.List.Properties (map-cong, alignWith-cong, unalignWith-cong, concatMap-cong) only take equality on the function, not on the input list. only foldr-cong takes equality on the input list.

then yes, it would be nice to port more of these properties to setoids, but in our current module structure those belong in Data.List.Relation.Binary.Equality.Setoid, is that correct? are you suggesting to move them?

[jamesmckinna]

Re: moving properties to ...Setoid: not as part of this PR ;-)

Re: cong properties (I think I may be responsible for some of the ones that you and @MatthewDaggitt identify) I have always tended to regard fold* in this sense as a 3-ary function, so I expect cong properties to involve equality on each of its 3 arguments. That said, and given the bias towards Propositional equality, it makes sense to refactor them only to concentrate on the function arguments as being extensionally equal, given that refl looks after the other ones. So my mistake, both historically, and now in commenting... :-(

TL;DR: you and @MatthewDaggitt are right!

As for Setoidal refactoring (for which an 'n-ary' statement of cong would make more sense...?), that's enough work for a bunch of downstream PRs... and some discussion ahead of time about how best to tackle it (rather than following my own first thoughts on the matter ;-))

[JacquesCarette]

Amusingly in code that Conor and I are currently writing, we've gone in the opposite direction: we've generalized some cong-like functions to take that explicit proofs on the 'obvious input' so that we had somewhere more obvious to hand certain proofs, instead of being more-or-less forced to do it in 2 steps.

My current thinking on that: this feels like a false choice. Why not have both kinds? Now, the default ones could certainly have a different design than the ones provided in an 'extended' module.

[jamesmckinna]

Thanks again to @mildsunrise for the prompt to reconsider some of the fundamentals. But we should focus on merging your #2355 before either getting too caught in the weeds... or any of the other PRs which yours has prompted!

[mildsunrise]

@JacquesCarette that's right, we can have two proofs for every higher order function, one accepting only functional equality and the other accepting also equality on the inputs. i'd only ask for things to be consistent among all functions.

@jamesmckinna yes, that would be nice :) let me see if there's anything missing there on my part