Add Effect.Foldable and Data.List.Effectful.Foldable implementati…

…on (#2300)

* draft initial implementation

* added `List` instances

* fix module name

* non-dependent instance for `vec`

* tweak

* added Nathan's morphism proofs

* add module for `Vec`

* tweak `import`s

* removed dependency

* removed dependency; more permissive `open`

* simplify with a local definition of the hom

* rename lemma; add a redundant lemma

* streamline `import` interface(s)

* remove the word instance from any of the comments. Tighten imports.

* Update Foldable.agda

Fixes the deprecated module import i hope

---------

Co-authored-by: Jacques Carette <[email protected]>

CHANGELOG.md

@@ -148,6 +148,12 @@ New modules
   ```
   plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`.
 
+* `Data.List.Effectful.Foldable`: `List` is `Foldable`
+
+* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable`
+
+* `Effect.Foldable`: implementation of haskell-like `Foldable`
+
 Additions to existing modules
 -----------------------------
 

src/Data/List/Effectful/Foldable.agda

@@ -0,0 +1,78 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- List is Foldable
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Effectful.Foldable where
+
+open import Algebra.Bundles using (Monoid)
+open import Algebra.Bundles.Raw using (RawMonoid)
+open import Algebra.Morphism.Structures using (IsMonoidHomomorphism)
+open import Data.List.Base as List using (List; []; _∷_; _++_)
+open import Effect.Foldable using (RawFoldableWithDefaults; RawFoldable)
+open import Function.Base using (_∘_; id)
+open import Level using (Level)
+import Relation.Binary.PropositionalEquality.Core as ≡
+
+private
+  variable
+    a c ℓ : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- Root implementation
+
+module _ (M : RawMonoid c ℓ) where
+
+  open RawMonoid M
+
+  foldMap : (A → Carrier) → List A → Carrier
+  foldMap f []       = ε
+  foldMap f (x ∷ xs) = f x ∙ foldMap f xs
+
+------------------------------------------------------------------------
+-- Basic implementation using supplied defaults
+
+foldableWithDefaults : RawFoldableWithDefaults (List {a})
+foldableWithDefaults = record { foldMap = λ M → foldMap M }
+
+------------------------------------------------------------------------
+-- Specialised version using optimised implementations
+
+foldable : RawFoldable (List {a})
+foldable = record
+  { foldMap = λ M → foldMap M
+  ; foldr = List.foldr
+  ; foldl = List.foldl
+  ; toList = id
+  }
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where
+
+  open Monoid M
+
+  private
+    h = foldMap rawMonoid f
+
+  []-homo : h [] ≈ ε
+  []-homo = refl
+
+  ++-homo : ∀ xs {ys} → h (xs ++ ys) ≈ h xs ∙ h ys
+  ++-homo []       = sym (identityˡ _)
+  ++-homo (x ∷ xs) = trans (∙-congˡ (++-homo xs)) (sym (assoc _ _ _))
+
+  foldMap-morphism : IsMonoidHomomorphism (List.++-[]-rawMonoid A) rawMonoid h
+  foldMap-morphism = record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = reflexive ∘ ≡.cong h }
+      ; homo = λ xs _ → ++-homo xs
+      }
+    ; ε-homo = []-homo
+    }

src/Data/Vec/Effectful/Foldable.agda

@@ -0,0 +1,51 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vec is Foldable
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Effectful.Foldable where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Base using (Vec; []; _∷_; foldr′; foldl′; toList)
+open import Effect.Foldable using (RawFoldableWithDefaults; RawFoldable)
+open import Function.Base using (id)
+open import Level using (Level)
+
+private
+  variable
+    a c ℓ : Level
+    A : Set a
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Root implementation
+
+module _ (M : RawMonoid c ℓ) where
+
+  open RawMonoid M
+
+  foldMap : (A → Carrier) → Vec A n → Carrier
+  foldMap f []       = ε
+  foldMap f (x ∷ xs) = f x ∙ foldMap f xs
+
+------------------------------------------------------------------------
+-- Basic implementation using supplied defaults
+
+foldableWithDefaults : RawFoldableWithDefaults {a} (λ A → Vec A n)
+foldableWithDefaults = record { foldMap = λ M → foldMap M }
+
+------------------------------------------------------------------------
+-- Specialised version using optimised implementations
+
+foldable : RawFoldable {a} (λ A → Vec A n)
+foldable = record
+  { foldMap = λ M → foldMap M
+  ; foldr = foldr′
+  ; foldl = foldl′
+  ; toList = toList
+  }
+

src/Effect/Foldable.agda

@@ -0,0 +1,77 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Foldable functors
+------------------------------------------------------------------------
+
+-- Note that currently the Foldable laws are not included here.
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Foldable where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+open import Algebra.Bundles using (Monoid)
+import Algebra.Construct.Flip.Op as Op
+
+open import Data.List.Base as List using (List; [_]; _++_)
+
+open import Effect.Functor as Fun using (RawFunctor)
+
+open import Function.Base using (id; flip)
+open import Function.Endo.Propositional using (∘-id-monoid)
+open import Level using (Level; Setω)
+open import Relation.Binary.Bundles using (Setoid)
+
+private
+  variable
+    f g c ℓ : Level
+    A : Set f
+    C : Set c
+
+
+------------------------------------------------------------------------
+-- The type of raw Foldables:
+-- all fields can be given non-default implementations
+
+record RawFoldable (F : Set f → Set g) : Setω where
+  field
+    foldMap : (M : RawMonoid c ℓ) (open RawMonoid M) →
+              (A → Carrier) → F A → Carrier
+
+  fold : (M : RawMonoid f ℓ) (open RawMonoid M) → F Carrier → Carrier
+  fold M = foldMap M id
+
+  field
+    foldr : (A -> C -> C) -> C -> F A -> C
+    foldl : (C -> A -> C) -> C -> F A -> C
+    toList : F A → List A
+
+
+------------------------------------------------------------------------
+-- The type of raw Foldables, with default implementations a la haskell
+
+record RawFoldableWithDefaults (F : Set f → Set g) : Setω where
+  field
+    foldMap : (M : RawMonoid c ℓ) (open RawMonoid M) →
+              (A → Carrier) → F A → Carrier
+
+  foldr : (A -> C -> C) -> C -> F A -> C
+  foldr {C = C} f z t = foldMap M₀ f t z
+    where M = ∘-id-monoid C ; M₀ = Monoid.rawMonoid M
+
+  foldl : (C -> A -> C) -> C -> F A -> C
+  foldl {C = C} f z t = foldMap M₀ (flip f) t z
+    where M = Op.monoid (∘-id-monoid C) ; M₀ = Monoid.rawMonoid M
+
+  toList : F A → List A
+  toList {A = A} = foldMap (List.++-[]-rawMonoid A) [_]
+
+  rawFoldable : RawFoldable F
+  rawFoldable = record
+    { foldMap = foldMap
+    ; foldr = foldr
+    ; foldl = foldl
+    ; toList = toList
+    }
+