sum and product for lists

[mechvel]

Data.List.Base has sum and product for lists over Nat.

Probably it is better to replace this with a generic design:

module Algebra.Properties.Monoid  ... where
C = Carrier

Π₁ : C → List C → C   -- product of a nonempty list of elements                 
Π₁ x = foldr _∙_ x                                                              
                                                                                  
Π : List C → C         -- product of a list of elements                
Π = Π₁ ε                                                                        
    
----------------------------------------
module Algebra.Properties.Semiring ... where
...
sum1 : C → List C → C                                                           
sum1 = Algebra.Properties.Monoid.Π₁  +-0-monoid                                                            
                                                                                  
sum : List C → C                       
sum = Algebra.Properties.Monoid.Π  +-0-monoid 

with adding to Algebra.Properties the needed modules for Monoid and Semiring.

?

[gallais]

cf. #1281

[mechvel]

I have an impression that #1281 does not relate to what I am suggesting.
In particular, #1281 starts with "List is a free semigroup". Probably the author means that (List A) it isomorphic to the domain of words over A with the operation of the word concatenation, and the latter domain is a free semigroup.

But I do not see its relevance to my simple suggestion.
Do you?
I suggest to have the product function for a list (calling it Π ) over any Monoid instead of only for list over Nat.
And to have sum via Π in +-0-monoid in Semiring.

[JacquesCarette]

That's exactly what fold : (M : Monoid) → List (Monoid.Carrier M) → Monoid.Carrier M is. You can define sum and product as 1-liners from there, by specialization of the Monoid argument.