Moved Category to Effect: issue #1636

[jamesmckinna]

Pretty much ready to go, but recent changes mean there are some conflicts to fix up, but none obviously from the compare diffs.

[MatthewDaggitt]

As this is quite a big change, I've posted an RFC on Zulip.

Also as the number of modules renamed are actually relatively small but widely used I'm afraid I'm going to be a pain and say that we should leave the old Category/Categorical behind and merely deprecate them, (e.g. see Strict). If this is too much grunt work for you @jamesmckinna, I can do at least some of it!

[jamesmckinna]

@MatthewDaggitt thanks for the thoughtful consideration and sensible pushback! I don't think it's 'a pain' as far as I am/was concerned (but see below). But unless/until there is a bit more movement towards the proposed change, I plan to sit tight for now. It was perhaps half a day's work, give or take (I missed quite some things first time around, not least remembering only eventually the need to update GenerateEverything.hs), and I'm sure it could be done/have been done more efficiently (there's a separate question, for a n00b like me, as to how to manage modifying the PR in line with your proposal with as little additional pain/grunt as possible).

As for the 'size' of the change, perhaps only 7/8 modules get renamed, but another 70-odd get touched by the change... quite some knock-on viscosity!

As for the deprecation proposal, this is a tough(er) one. @wenkokke 's original issue had a 'rider'... namely that the namespace freed up by the move would then be available for the proper incorporation of agda-categories... which is really what I think this ought to be about (a steer from @JacquesCarette on the associated timescale/workload associated with that topic would be welcome?). But that can't happen without (a lot?) more pain if the old hierarchy is retained. My understanding was that the 2.0 milestone was intended to allow for... 'serious' reconsideration of the 1.x-era library structure. The transition 1.6->1.7 accompanied the 2.6.1.y to 2.6.2 agda version bump, and that was definitely a major breaking change (for me, and coauthors; I'm not really sure sure when we will have energy to fast-forward our existing published 1.6 proof developments to 1.7, let alone 2.0, because of the way both agda and the stdlib changed together). If the old hierarchy is retained, but deprecated, I could imagine that it will/may/might be a long (?) time before the breaking change can be properly bedded in, as people continue to develop on top of 2.0 (or do deprecation warnings achieve change within one or at most two cycles of minor version bumps?). So, my gut feeling would be towards: better to lance the boil early. (Don't make the viscosity any worse than it is)

Consequently, wide consultation is a good idea here, and I wouldn't push for change before (mostly) everyone was (mostly) on board with it. Making the PR was way to kick-start that process.

And as for the name change, never mind the PR, this was an experiment on my part. (NB. always remembering to be prepared to 'murder your darlings'). I don't suppose (beyond narcissistically thinking that my ideas are usually good ones, in good taste etc. ;)) that I am wedded to the Effect/Effectful pairing... though I do think they fit better with our 'modern' understanding of the associated haskell Control.* hierarchy as being a particular way to manage the incorporation of effects/effectful behaviour into a pure language... without being tied to haskell's namespace choices, again as Wen and Jesper discussed previously. But I do find myself thinking that the Category/Categorical story really is not fit for purpose, neither then nor certainly now. And certainly not with a "we can't guarantee to maintain this in future versions, but for the time being..." caveat...

That said, I suppose, given that it involves 'mere' renaming, that it could be part of a 1.8 release, with a view to cutting the umbilical in the transition 1.8->2.0? Maybe that's my simple-mindedness/naivete/n00biety talking... ;-) and that such a thing would entail even more work to achieve...? Or maybe, as with the Codata.Sized move, we could have a temporary (and deprecated!) hierarchy under Control.Category/Control.Categorical etc. as a staging post? I would welcome expert insight into the cost/benefit of any of the above.

[MatthewDaggitt]

As for the deprecation proposal, this is a tough(er) one. @wenkokke 's original issue had a 'rider'... namely that the namespace freed up by the move would then be available for the proper incorporation of agda-categories... which is really what I think this ought to be about (a steer from @JacquesCarette on the associated timescale/workload associated with that topic would be welcome?). But that can't happen without (a lot?) more pain if the old hierarchy is retained.

That's a good point! @JacquesCarette does the currently library naming convention take up namespace that you'd like for agda-categories?

That said, I suppose, given that it involves 'mere' renaming, that it could be part of a 1.8 release, with a view to cutting the umbilical in the transition 1.8->2.0?

I'm afraid that that the v1.8 ship has sailed I'm afraid. In particular my widespread use of NonZero and @Taneb's work on stripping out the old function hierarchy would not be easy to back out. I agree, though deprecation is ideal, but if it is actively harmful to agda-categories then yes in v2.0 we could remove it entirely.

Ideally I would do the same with Codata.Sized but the number of modules there meant that I couldn't face it. If I pluck up the courage before release I might have a go at doing it though.

there's a separate question, for a n00b like me, as to how to manage modifying the PR in line with your proposal with as little additional pain/grunt as possible

Err, I haven't come up with a semi-automated way of doing it I'm afraid. It's usually a couple of hours of copy and pasting. Never quite sure how much user time is saved by the deprecation warnings, but I assume non-trivial. Then again estimates are difficult as I'm never quite sure what sort of order of magnitude the user-base of Agda/ the standard library is.

[wenkokke]

@JacquesCarette mentioned previously that the reason that the agda-categories library is in the Categories namespace is exactly because of this conflict. Regardless of whether or not they choose to "singularize" the module name, having both Categories and Category would be tremendously confusing to the user.

[JacquesCarette]

@wenkokke is correct about the choice of names.

My intent was indeed always to migrate parts of agda-categories in to stdlib. I should have time to start doing so from August onwards. There are a number of decisions to make. For one, it doesn't make sense to integrate all of agda-categories into stdlib (at least, as far as I'm concerned). I was thinking of doing the migration 'incrementally'.

There will be all sorts of decisions to make. There are various 'convenience' functions and sub-modules included in various records that cause bloat. They sure are convenient though. I doesn't seem like it should be a big problem, but it seems that details of Agda to make it so. I don't know why.

[MatthewDaggitt]

Okay well there doesn't seem to be any sort of feedback in the last 10 days so I'm of a mind to merge this in the next couple of days.

[MatthewDaggitt]

Thanks for taking the initiative on this @jamesmckinna!