Add Effect.Foldable and Data.List.Effectful.Foldable implementation

CHANGELOG.md

@@ -48,6 +48,12 @@ New modules
 
 * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
 
+* `Data.List.Effectful.Foldable`: instance(s) of the following typeclass
+
+* `Data.Vec.Effectful.Foldable`: instance(s) of the following typeclass
+
+* `Effect.Foldable`: implementation of haskell-like typeclass
+
 Additions to existing modules
 -----------------------------
 

src/Data/List/Effectful/Foldable.agda

@@ -0,0 +1,80 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The Foldable instance of List
+------------------------------------------------------------------------
+
+{-# 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
+open import Function.Base
+open import Level
+import Relation.Binary.PropositionalEquality 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 instance: using supplied defaults
+
+foldableWithDefaults : RawFoldableWithDefaults (List {a})
+foldableWithDefaults = record { foldMap = λ M → foldMap M }
+
+------------------------------------------------------------------------
+-- Specialised instance: 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,55 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The Foldable instance of Vec
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Effectful.Foldable where
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+open import Data.Nat.Base
+open import Data.Vec.Base
+open import Data.Vec.Properties
+open import Effect.Foldable
+open import Function.Base
+open import Level
+open import Relation.Binary.PropositionalEquality as ≡
+ using (_≡_; _≢_; _≗_; refl; module ≡-Reasoning)
+
+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 instance: using supplied defaults
+
+foldableWithDefaults : RawFoldableWithDefaults {a} (λ A → Vec A n)
+foldableWithDefaults = record { foldMap = λ M → foldMap M }
+
+------------------------------------------------------------------------
+-- Specialised instance: 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.Endomorphism.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
+ }
+