From a14e89d54c4b5b4a7024311cf6cf2aafeb17e1d0 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sun, 23 Aug 2020 11:24:29 +0100
Subject: [PATCH 1/2] Add fold and foldMap functions to Data.List

---
 CHANGELOG.md            |  2 ++
 src/Data/List/Base.agda | 14 ++++++++++++++
 2 files changed, 16 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2eafff9ccb..98a0a99379 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -285,6 +285,8 @@ 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`:
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 0ae32f479e..446c539d50 100644
--- a/src/Data/List/Base.agda
+++ b/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
 ------------------------------------------------------------------------

From 5c990e773bbe0a01b7959f6210a715978e47fdab Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sun, 23 Aug 2020 11:39:31 +0100
Subject: [PATCH 2/2] Add some properties of foldMap

---
 CHANGELOG.md                  |  2 ++
 src/Data/List/Properties.agda | 21 +++++++++++++++++++++
 2 files changed, 23 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 98a0a99379..e10c20ccae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -293,6 +293,8 @@ Other minor additions
   ```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`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 8873f84720..29203b5a72 100644
--- a/src/Data/List/Properties.agda
+++ b/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