Rename `Category.*` modules to `Effect.*` to avoid confusion with agda-categories

[wenkokke]

I am open to suggestions for better names then Control, it was merely chosen to imitate Haskell.

However, the current name is rather confusing given the existence of the agda-categories library, and the fact that these modules in the standard library do not implement categories in the general sense.

[wenkokke]

Using Control.* might conflict with the agda-hs library, but I suppose these two are never meant to be used in conjunction, @jespercockx?

[jespercockx]

The modules of the agda2hs library are all prefixed with Haskell., so there is no problem with conflicts. I agree that Categories is a confusing name for this part of the library, though I must say that Control has always been a bit mysterious to me. I'm not sure what would be a better name though, perhaps Computation?

[JacquesCarette]

Well, Category.* implements 'categories internal to Agda', minus laws, a la Haskell. Its presence is why agda-categories uses Categories. as the main name-space!

I'm not super fond of Control. for this - but not against it either. I'd almost be tempted to use the name Haskell.* for this! [Part tongue-in-cheek, part serious.] Yes, it would be in the same name space as agda2hs, but perhaps that would be a good thing.

Computation is an interesting suggestion indeed.

[wenkokke]

I mostly think that Control. is a good option because it is familiar to Haskell programmers. I think that using Computation. would be deeply confusing, and I think that Category. is confusing because the module hierarchy does not implement categories in general.

On the upshot, @JacquesCarette, with a change made agda/agda-categories could move to inhabit the Category. namespace!

[jamesmckinna]

Effect(s).*?

[jamesmckinna]

So... no-one other than @wenkokke responded to my Effect suggested renaming. I'm pursuing this on a branch, and it raises the question (renaming in git is boring... but perhaps there's a way to do this automagically) as to whether the modules which use these notions, typically falling under ...Categorical might better be also renamed, viz as ...Effectful. Thoughts?

[jamesmckinna]

Beside: this will definitely be a label:breaking change ;-)

[JacquesCarette]

Effectful is an interesting suggestion. So is Effect.

[jamesmckinna]

Branch at jamesmckinna/agda-stdlib:issue1636.
DONE: follow-up with the Categorical to Effectful renaming, as per my speculative CHANGELOG entry.
EDITED: PR#1735 now.