Add foldMap and fold

CHANGELOG.md

@@ -285,12 +285,16 @@ Other minor additions
   wordsBy              : Decidable P → List A → List (List A)
   cartesianProductWith : (A → B → C) → List A → List B → List C
   cartesianProduct     : List A → List B → List (A × B)
+  foldMap              : (M : Monoid) → (A → Monoid.Carrier M) → List A → Monoid.Carrier M
+  fold                 : (M : Monoid) → List (Monoid.Carrier M) → Monoid.Carrier M
   ```
 
 * Added new proofs to `Data.List.Properties`:
   ```agda
   reverse-injective : reverse xs ≡ reverse ys → xs ≡ ys
   map-injective     : Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f)
+  ++-foldMap        : foldMap M f (xs ++ ys) ≈ foldMap M f xs ∙ foldMap M f ys
+  foldMap-morphism  : IsMonoidMorphism (++-monoid A) M (foldMap M f)
   ```
 
 * Added new proofs to `Data.List.Membership.Propositional.Properties`:

src/Data/List/Base.agda

@@ -11,6 +11,7 @@
 
 module Data.List.Base where
 
+open import Algebra.Bundles using (Monoid)
 open import Data.Bool.Base as Bool
   using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
 open import Data.Fin.Base using (Fin; zero; suc)
@@ -394,6 +395,19 @@ wordsBy {A = A} P? = go [] where
   ... | true  = cons acc (go [] cs)
   ... | false = go (c ∷ acc) cs
 
+------------------------------------------------------------------------
+-- Monoidal folding
+
+module _ {c ℓ} (M : Monoid c ℓ) where
+  open Monoid M
+
+  foldMap : ∀ {a} {A : Set a} → (A → Carrier) → List A → Carrier
+  foldMap f [] = ε
+  foldMap f (x ∷ xs) = f x ∙ foldMap f xs
+
+  fold : List Carrier → Carrier
+  fold = foldMap id
+
 ------------------------------------------------------------------------
 -- DEPRECATED
 ------------------------------------------------------------------------

src/Data/List/Properties.agda

@@ -13,6 +13,7 @@ module Data.List.Properties where
 
 open import Algebra.Bundles
 open import Algebra.Definitions as AlgebraicDefinitions using (Involutive)
+open import Algebra.Morphism using (IsMonoidMorphism)
 import Algebra.Structures as AlgebraicStructures
 open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
 open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁)
@@ -960,7 +961,27 @@ module _ {x y : A} where
   ∷ʳ-injectiveʳ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
   ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)
 
+------------------------------------------------------------------------
+-- foldMap
+
+module _ {c ℓ} (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where
+
+  open Monoid M using (_∙_; _≈_; identityˡ; ∙-cong)
 
+  ++-foldMap : ∀ xs ys → foldMap M f (xs ++ ys) ≈ foldMap M f xs ∙ foldMap M f ys
+  ++-foldMap [] ys = Monoid.sym M (identityˡ _)
+  ++-foldMap (x ∷ xs) ys = Monoid.trans M
+    (∙-cong (Monoid.refl M) (++-foldMap xs ys))
+    (Monoid.sym M (Monoid.assoc M _ _ _))
+
+  foldMap-morphism : IsMonoidMorphism (++-monoid A) M (foldMap M f)
+  foldMap-morphism = record
+    { sm-homo = record
+      { ⟦⟧-cong = λ p → Monoid.reflexive M (cong (foldMap M f) p)
+      ; ∙-homo = ++-foldMap
+      }
+    ; ε-homo = Monoid.refl M
+    }
 
 ------------------------------------------------------------------------
 -- DEPRECATED