Inconsistency: `map-compose` vs. `map-∘`

[gallais]

In Data.List.Properties we use map-compose whereas in Data.Vec.Properties we use map-∘.

[gallais]

And in Codata.* we use map-map-fusion.

[jamesmckinna]

Suggest map-∘ throughout?

[gallais]

:+1: That is consistent with the convention we use

[gallais]

I see that we also have map-++-commute instead of map-++.

[jamesmckinna]

And similarly sum-++-commute. I'll open a PR.

[jamesmckinna]

What about the *-commute properties in Data.Sum.Properties?

[JacquesCarette]

I wonder if map-++-commute might have been my doing. I like that name... but I'm completely fine with map-++ if that's the library convention.

[jamesmckinna]

@JacquesCarette I take your point about 'small' PRs: but #626 and #509 are about consistency/uniformity of names according to a systematic library convention (whose stipulation to a large extent is neither here nor there; consistency is the main consideration here); the case of map-id(entity) was, at least on my reading, of the same order of need for consistency, as that of map-∘ which started this issue for milestone 2.0...

I'm certainly open to the possibility that Codata.* properties might better want distinct names, to draw attention to the fact that

• in the case of -identity, the relation is that of bismilarity, not equality
• in the case of -∘, that the direction of the equation is opposite to that in Data.*

For this reason, I ~~have stopped pushing~~ did not yet push any commits regarding changes to Codata

[JacquesCarette]

@jamesmckinna it is indeed a philosophical disagreement. You see this PR as achieving consistency/uniformity as a complete unit, while I'd be quite happy with a sequence of PRs whose union would achieve that. Moving closer to the goal is worthwhile, even if the ultimate goal (for whatever reason) is not ultimately achieve for 2.0. [I use this philosophy quite strongly in my Drasil project.]

Ultimately the person who is actually doing the work gets to decide, as this is all volunteer work. I believe in that 'philosophy' even more strongly than in the above!

[jamesmckinna]

Thanks for clarification. Given our discussion on Monday about the 2.0 milestone, I was indeed keen to achieve 'completeness' in closing these two issues. But yes, experience with git(hub) has taught me that small(er) steps are usually better. But this one, 'bigger' as it may seem, has proved largely routine. Updating CHANGELOG is perhaps another matter.

[jamesmckinna]

Updated CHANGELOG.

[jamesmckinna]

Outstanding instances of -commute:

• [x] Data.Sum.Properties affecting Data.Fin.Properties and Data.Vec.Properties through [,]-map-commute and [,]-∘-distr (!), plus a couple of other map-commute-like lemmas not used elsewhere
• [x] Data.Vec.Recursive.Properties with a single lemma append-cons-commute used only internally
• [x] Data.Tree.Binary.Zipper.Properties with a number of toTree-*-commute lemmas
• [ ] Data.Integer.Properties affecting Data.Integer.Coprimality, Data.Integer.Divisibility.Signed, Data.Integer.Divisibility, Data.Integer.DivMod, and Data.Rational.Properties, through abs-*-commute and pos-+-commute

Only the first really seems worth tackling (not least for the mildly non-trivial knock-on viscosity); the second two are leaf modules in the library dependency graph (EDITED: and are therefore low-hanging-fruit, so I've knocked those off as well); and the last seems to require some prior work on #501 before proceeding. ~~Suggestions as to how to proceed further?~~