[ refactor ] Remove `sum` and `product` (and their properties) from `Data.List.*`

[jamesmckinna]

This is a long-standing legacy issue (cf. #1099 ) that causes problems esp. regarding:

• the dependency graph: Data.List.Base and Properties need to import Data.Nat.Divisibility otherwise unnecessarily; also, how much of Algebra should be imported by 'concrete' Data modules? Data.List.Properties ends up being where properties of sum and product get proved...
• abstraction level: these are operations definable on (Raw)Monoids, and should be treated as such
• extensibility: every time a 'new' property needs to be proven, the above questions need to be re-examined (esp. wrt dependency, eg do we want to import Data.List.Relation.Binary.Permutation.* into Data.List.Properties, etc.?)
• etc.

Just as, in the end, it was (judged to be) 'better' to lift out scans from Data.List.Base, sum and product should be lifted out from Data.List.Base (and correspondingly their properties from Data.List.Properties) into (at least!) a separate module.

Lots of design choices here:

• a general theory under Algebra.Definitions.RawMonoid/Algebra.Properties.Monoid? Deprecation problems wrt the existing definitions and properties of sum etc. so potentially lots of breaking changes, otherwise a mess of deprecations?
• theory of interaction(s) between them (esp. wrt distributivity) under Algebra.Properties.(Commutative)(Semi)Ring etc.
• instantiation for Nat (and the other numeric types Integer and Rational?): what should the module be called?
• definition in terms of concrete List, or abstract FreeMonoid? (the latter seems preferable, as an algebraic definition; the former for computation... usual issues/trade-offs arise cf. #2539 etc.) This might (usefully!) uncouple the dependency currently on Data.Vec.Functional for sum etc.

Possible implementation pathway (UPDATED):

• v2.3, a 'minimal', move+deprecation-only refactoring: #2558 and #2561
• v3.0, a breaking version to get things 'right' (we need to agree what this means!)

UPDATED: I got the locations wrong! But in many ways, having these Nat operations under List is even less appropriate!?

[mechvel]

the dependency graph: Data.List.Base and Properties need to import Data.Nat.Divisibility otherwise unnecessarily; also, how much of Algebra should be imported by 'concrete' Data modules? Data.List.Properties ends up being where properties > of sum and product get proved...

It is not natural for Data.List to use the function of product of a list of natural numbers, and for Data.List.Properties to prove the properties of this product. But it is possible to introduce, say Data.Nat.List and put there some items for List Nat. Digression: generally, the dependency problem Foo <--> Foo' can be solved by setting Foo and Foo-II, where Foo does not use Foo' while Foo-II does.

[JacquesCarette]

I emphatically agree with removing sum and product from Data.List.Base. That was a grave mistake that is relatively harmless in Haskell-like languages and deadly in Agda-like languages.

[jamesmckinna]

I emphatically agree with removing sum and product from Data.List.Base. That was a grave mistake that is relatively harmless in Haskell-like languages and deadly in Agda-like languages.

And how about @Taneb 's question on #2558 regarding and/or and all/any? Etc.

[mechvel]

I emphatically agree with removing sum and product from Data.List.Base.

In my proposal with IntegralSemiring, product and its properties for Nat are moved to Data/Nat/List.agda :
the items for List ℕ. This is implemented as over instances of Monoid and IntegralSemiring. The same can be done for sum, and the same approach can be applier to Integer. Another reasonable place can be Data/List/Nat/ {Properties/} , Data/List/Integer/ {Properties/} , and such. I like this latter place more than Data/Nat/List because List is a more general domain constructor than ℕ: Data, List, ℕ being a sequence of "classes" set in a non-increasing generality order.

[JacquesCarette]

And how about @Taneb 's question on https://github.com/agda/agda-stdlib/pull/2558 regarding and/or and all/any? Etc.

Ditto: this don't belong in Data.List.Base. Same wart, just that downstream effects are not as dire.