From d2a7ee50161aaab4a4c14f554b3ae301c3d97a9e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 23 Feb 2024 16:58:12 +0000 Subject: [PATCH 01/15] draft initial implementation --- CHANGELOG.md | 2 + src/Effect/Foldable.agda | 85 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 87 insertions(+) create mode 100644 src/Effect/Foldable.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 7fa21bf90e..b67c258c9c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,6 +48,8 @@ New modules * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures +* `Effect.Foldable`: implementation of haskell-like typeclass + Additions to existing modules ----------------------------- diff --git a/src/Effect/Foldable.agda b/src/Effect/Foldable.agda new file mode 100644 index 0000000000..63a30d547d --- /dev/null +++ b/src/Effect/Foldable.agda @@ -0,0 +1,85 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Applicative functors +------------------------------------------------------------------------ + +-- Note that currently the applicative functor 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; [_]; _++_) +import Data.List.Properties as List + +open import Effect.Functor as Fun using (RawFunctor) + +open import Function.Base using (id; flip) +import Function.Endomorphism.Propositional as Endomorphism-≡ +open import Level using (Level; suc; _⊔_; Setω) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial + +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 + +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 + open Endomorphism-≡ C + M = Monoid.rawMonoid ∘-id-monoid + + foldl : (C -> A -> C) -> C -> F A -> C + foldl {C = C} f z t = foldMap M (flip f) t z + where + open Endomorphism-≡ C + M = Monoid.rawMonoid (Op.monoid ∘-id-monoid) + + 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 + } + From a1b575b5c4470dcca42533673fa828e4952ffe7e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 23 Feb 2024 18:51:22 +0000 Subject: [PATCH 02/15] added `List` instances --- CHANGELOG.md | 2 ++ src/Data/List/Effectful/Foldable.agda | 52 +++++++++++++++++++++++++++ src/Effect/Foldable.agda | 6 ++-- 3 files changed, 56 insertions(+), 4 deletions(-) create mode 100644 src/Data/List/Effectful/Foldable.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index b67c258c9c..51fa11436a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,6 +48,8 @@ New modules * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures +* `Data.List.Effectful.Foldable`: instance(s) of the following typeclass + * `Effect.Foldable`: implementation of haskell-like typeclass Additions to existing modules diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda new file mode 100644 index 0000000000..a72876eff0 --- /dev/null +++ b/src/Data/List/Effectful/Foldable.agda @@ -0,0 +1,52 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The Foldable instance of List +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.List.Effectful/Foldable where + +open import Algebra.Bundles.Raw using (RawMonoid) +open import Data.List.Base +open import Data.List.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 + + +------------------------------------------------------------------------ +-- 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 = foldr + ; foldl = foldl + ; toList = id + } diff --git a/src/Effect/Foldable.agda b/src/Effect/Foldable.agda index 63a30d547d..ebce2373f2 100644 --- a/src/Effect/Foldable.agda +++ b/src/Effect/Foldable.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Applicative functors +-- Foldable functors ------------------------------------------------------------------------ -- Note that currently the applicative functor laws are not included @@ -24,8 +24,6 @@ open import Function.Base using (id; flip) import Function.Endomorphism.Propositional as Endomorphism-≡ open import Level using (Level; suc; _⊔_; Setω) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) -import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial private variable @@ -53,7 +51,7 @@ record RawFoldable (F : Set f → Set g) : Setω where ------------------------------------------------------------------------ --- The type of raw Foldables, with default implementations +-- The type of raw Foldables, with default implementations a la haskell record RawFoldableWithDefaults (F : Set f → Set g) : Setω where field From 35590557ad40f0a125b0d3bf808944b98b07933b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 23 Feb 2024 18:57:27 +0000 Subject: [PATCH 03/15] fix module name --- src/Data/List/Effectful/Foldable.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index a72876eff0..becfb04890 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Data.List.Effectful/Foldable where +module Data.List.Effectful.Foldable where open import Algebra.Bundles.Raw using (RawMonoid) open import Data.List.Base From 5aec64cb3e7d5ec539fcdffded0f55f51bc6c2b0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 24 Feb 2024 06:42:00 +0000 Subject: [PATCH 04/15] non-dependent instance for `vec` --- src/Data/Vec/Effectful/Foldable.agda | 55 ++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 src/Data/Vec/Effectful/Foldable.agda diff --git a/src/Data/Vec/Effectful/Foldable.agda b/src/Data/Vec/Effectful/Foldable.agda new file mode 100644 index 0000000000..ddd9ab2111 --- /dev/null +++ b/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 + } + From a71af571eb0ae144acec54dd587a0bcfcf3d9f63 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 24 Feb 2024 06:42:29 +0000 Subject: [PATCH 05/15] tweak --- src/Effect/Foldable.agda | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/Effect/Foldable.agda b/src/Effect/Foldable.agda index ebce2373f2..8c0a3bdceb 100644 --- a/src/Effect/Foldable.agda +++ b/src/Effect/Foldable.agda @@ -59,16 +59,12 @@ record RawFoldableWithDefaults (F : Set f → Set g) : Setω where (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 - open Endomorphism-≡ C - M = Monoid.rawMonoid ∘-id-monoid + foldr {C = C} f z t = foldMap (Monoid.rawMonoid M) f t z + where M = Endomorphism-≡.∘-id-monoid C foldl : (C -> A -> C) -> C -> F A -> C - foldl {C = C} f z t = foldMap M (flip f) t z - where - open Endomorphism-≡ C - M = Monoid.rawMonoid (Op.monoid ∘-id-monoid) + foldl {C = C} f z t = foldMap (Monoid.rawMonoid M) (flip f) t z + where M = Op.monoid (Endomorphism-≡.∘-id-monoid C) toList : F A → List A toList {A = A} = foldMap (List.++-[]-rawMonoid A) [_] From a2b5679e36f97d01df58f6562844a98c673a8848 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 24 Feb 2024 07:55:29 +0000 Subject: [PATCH 06/15] added Nathan's morphism proofs --- src/Data/List/Effectful/Foldable.agda | 31 +++++++++++++++++++++++++-- 1 file changed, 29 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index becfb04890..ed44119c0f 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -8,14 +8,16 @@ 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 open import Data.List.Properties open import Effect.Foldable open import Function.Base open import Level -open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_; _≢_; _≗_; refl; module ≡-Reasoning) +import Relation.Binary.PropositionalEquality as ≡ +-- using (_≡_; _≢_; _≗_; refl; module ≡-Reasoning) private variable @@ -50,3 +52,28 @@ foldable = record ; foldl = foldl ; toList = id } + +------------------------------------------------------------------------ +-- Properties + +module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where + + open Monoid M using (_∙_; _≈_; identityˡ; ∙-congˡ) + renaming (rawMonoid to M₀) + + ++-foldMap : ∀ xs {ys} → + foldMap M₀ f (xs ++ ys) ≈ foldMap M₀ f xs ∙ foldMap M₀ f ys + ++-foldMap [] = Monoid.sym M (identityˡ _) + ++-foldMap (x ∷ xs) = Monoid.trans M + (∙-congˡ (++-foldMap xs)) + (Monoid.sym M (Monoid.assoc M _ _ _)) + + foldMap-morphism : IsMonoidHomomorphism (++-[]-rawMonoid A) M₀ (foldMap M₀ f) + foldMap-morphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = Monoid.reflexive M ∘ ≡.cong (foldMap M₀ f) } + ; homo = λ xs _ → ++-foldMap xs + } + ; ε-homo = Monoid.refl M + } From d53e21621f54bd69aa19750e5fadf6627024e59d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 24 Feb 2024 09:43:06 +0000 Subject: [PATCH 07/15] add module for `Vec` --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 51fa11436a..416820b5e2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -50,6 +50,8 @@ New modules * `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 From 009914ab889626eb9a2b9818757f60cae71fba42 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 24 Feb 2024 10:07:13 +0000 Subject: [PATCH 08/15] tweak `import`s --- src/Effect/Foldable.agda | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Effect/Foldable.agda b/src/Effect/Foldable.agda index 8c0a3bdceb..004972d23a 100644 --- a/src/Effect/Foldable.agda +++ b/src/Effect/Foldable.agda @@ -4,8 +4,7 @@ -- Foldable functors ------------------------------------------------------------------------ --- Note that currently the applicative functor laws are not included --- here. +-- Note that currently the Foldable laws are not included here. {-# OPTIONS --cubical-compatible --safe #-} @@ -21,8 +20,8 @@ import Data.List.Properties as List open import Effect.Functor as Fun using (RawFunctor) open import Function.Base using (id; flip) -import Function.Endomorphism.Propositional as Endomorphism-≡ -open import Level using (Level; suc; _⊔_; Setω) +open import Function.Endomorphism.Propositional using (∘-id-monoid) +open import Level using (Level; Setω) open import Relation.Binary.Bundles using (Setoid) private @@ -60,11 +59,11 @@ record RawFoldableWithDefaults (F : Set f → Set g) : Setω where foldr : (A -> C -> C) -> C -> F A -> C foldr {C = C} f z t = foldMap (Monoid.rawMonoid M) f t z - where M = Endomorphism-≡.∘-id-monoid C + where M = ∘-id-monoid C foldl : (C -> A -> C) -> C -> F A -> C foldl {C = C} f z t = foldMap (Monoid.rawMonoid M) (flip f) t z - where M = Op.monoid (Endomorphism-≡.∘-id-monoid C) + where M = Op.monoid (∘-id-monoid C) toList : F A → List A toList {A = A} = foldMap (List.++-[]-rawMonoid A) [_] From a8e91823d92bec31456bc6912e0a7825a6442197 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 1 Mar 2024 09:42:23 +0000 Subject: [PATCH 09/15] removed dependency --- src/Effect/Foldable.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Effect/Foldable.agda b/src/Effect/Foldable.agda index 004972d23a..67b5555bf0 100644 --- a/src/Effect/Foldable.agda +++ b/src/Effect/Foldable.agda @@ -15,7 +15,6 @@ open import Algebra.Bundles using (Monoid) import Algebra.Construct.Flip.Op as Op open import Data.List.Base as List using (List; [_]; _++_) -import Data.List.Properties as List open import Effect.Functor as Fun using (RawFunctor) From 8e7b7be203a76e60da5f335de8bd61e95b3ff092 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 1 Mar 2024 09:55:50 +0000 Subject: [PATCH 10/15] removed dependency; more permissive `open` --- src/Data/List/Effectful/Foldable.agda | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index ed44119c0f..f9bc27a1c8 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -12,12 +12,11 @@ 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 -open import Data.List.Properties open import Effect.Foldable open import Function.Base open import Level import Relation.Binary.PropositionalEquality as ≡ --- using (_≡_; _≢_; _≗_; refl; module ≡-Reasoning) + private variable @@ -58,22 +57,21 @@ foldable = record module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where - open Monoid M using (_∙_; _≈_; identityˡ; ∙-congˡ) - renaming (rawMonoid to M₀) + open Monoid M renaming (rawMonoid to M₀) ++-foldMap : ∀ xs {ys} → foldMap M₀ f (xs ++ ys) ≈ foldMap M₀ f xs ∙ foldMap M₀ f ys - ++-foldMap [] = Monoid.sym M (identityˡ _) - ++-foldMap (x ∷ xs) = Monoid.trans M + ++-foldMap [] = sym (identityˡ _) + ++-foldMap (x ∷ xs) = trans (∙-congˡ (++-foldMap xs)) - (Monoid.sym M (Monoid.assoc M _ _ _)) + (sym (assoc _ _ _)) foldMap-morphism : IsMonoidHomomorphism (++-[]-rawMonoid A) M₀ (foldMap M₀ f) foldMap-morphism = record { isMagmaHomomorphism = record { isRelHomomorphism = record - { cong = Monoid.reflexive M ∘ ≡.cong (foldMap M₀ f) } + { cong = reflexive ∘ ≡.cong (foldMap M₀ f) } ; homo = λ xs _ → ++-foldMap xs } - ; ε-homo = Monoid.refl M + ; ε-homo = refl } From 815a7aa94a8bb7e4f3a272a9d14ea6bac9140bc9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 1 Mar 2024 10:02:44 +0000 Subject: [PATCH 11/15] simplify with a local definition of the hom --- src/Data/List/Effectful/Foldable.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index f9bc27a1c8..657d945223 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -57,20 +57,20 @@ foldable = record module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where - open Monoid M renaming (rawMonoid to M₀) + open Monoid M - ++-foldMap : ∀ xs {ys} → - foldMap M₀ f (xs ++ ys) ≈ foldMap M₀ f xs ∙ foldMap M₀ f ys + private + h = foldMap rawMonoid f + + ++-foldMap : ∀ xs {ys} → h (xs ++ ys) ≈ h xs ∙ h ys ++-foldMap [] = sym (identityˡ _) - ++-foldMap (x ∷ xs) = trans - (∙-congˡ (++-foldMap xs)) - (sym (assoc _ _ _)) + ++-foldMap (x ∷ xs) = trans (∙-congˡ (++-foldMap xs)) (sym (assoc _ _ _)) - foldMap-morphism : IsMonoidHomomorphism (++-[]-rawMonoid A) M₀ (foldMap M₀ f) + foldMap-morphism : IsMonoidHomomorphism (++-[]-rawMonoid A) rawMonoid h foldMap-morphism = record { isMagmaHomomorphism = record { isRelHomomorphism = record - { cong = reflexive ∘ ≡.cong (foldMap M₀ f) } + { cong = reflexive ∘ ≡.cong h } ; homo = λ xs _ → ++-foldMap xs } ; ε-homo = refl From 58560736758d5b00459f2e5b57a86a1a65f4cfc6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 1 Mar 2024 10:06:49 +0000 Subject: [PATCH 12/15] rename lemma; add a redundant lemma --- src/Data/List/Effectful/Foldable.agda | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 657d945223..6fea3ff543 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -62,16 +62,19 @@ module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where private h = foldMap rawMonoid f - ++-foldMap : ∀ xs {ys} → h (xs ++ ys) ≈ h xs ∙ h ys - ++-foldMap [] = sym (identityˡ _) - ++-foldMap (x ∷ xs) = trans (∙-congˡ (++-foldMap xs)) (sym (assoc _ _ _)) + []-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 (++-[]-rawMonoid A) rawMonoid h foldMap-morphism = record { isMagmaHomomorphism = record { isRelHomomorphism = record { cong = reflexive ∘ ≡.cong h } - ; homo = λ xs _ → ++-foldMap xs + ; homo = λ xs _ → ++-homo xs } - ; ε-homo = refl + ; ε-homo = []-homo } From 68d176339168b2f3f0e627ffe2f66f6702382f58 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 1 Mar 2024 10:12:44 +0000 Subject: [PATCH 13/15] streamline `import` interface(s) --- src/Data/List/Effectful/Foldable.agda | 8 ++++---- src/Effect/Foldable.agda | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 6fea3ff543..7040c3fecb 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -11,7 +11,7 @@ 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 +open import Data.List.Base as List using (List; []; _∷_; _++_) open import Effect.Foldable open import Function.Base open import Level @@ -47,8 +47,8 @@ foldableWithDefaults = record { foldMap = λ M → foldMap M } foldable : RawFoldable (List {a}) foldable = record { foldMap = λ M → foldMap M - ; foldr = foldr - ; foldl = foldl + ; foldr = List.foldr + ; foldl = List.foldl ; toList = id } @@ -69,7 +69,7 @@ module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where ++-homo [] = sym (identityˡ _) ++-homo (x ∷ xs) = trans (∙-congˡ (++-homo xs)) (sym (assoc _ _ _)) - foldMap-morphism : IsMonoidHomomorphism (++-[]-rawMonoid A) rawMonoid h + foldMap-morphism : IsMonoidHomomorphism (List.++-[]-rawMonoid A) rawMonoid h foldMap-morphism = record { isMagmaHomomorphism = record { isRelHomomorphism = record diff --git a/src/Effect/Foldable.agda b/src/Effect/Foldable.agda index 67b5555bf0..991d1b838c 100644 --- a/src/Effect/Foldable.agda +++ b/src/Effect/Foldable.agda @@ -57,12 +57,12 @@ record RawFoldableWithDefaults (F : Set f → Set g) : Setω where (A → Carrier) → F A → Carrier foldr : (A -> C -> C) -> C -> F A -> C - foldr {C = C} f z t = foldMap (Monoid.rawMonoid M) f t z - where M = ∘-id-monoid 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 (Monoid.rawMonoid M) (flip f) t z - where M = Op.monoid (∘-id-monoid 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) [_] From df2a304406dcf018bab878edffecd10f51fd08ab Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 2 May 2024 23:00:28 -0400 Subject: [PATCH 14/15] remove the word instance from any of the comments. Tighten imports. --- CHANGELOG.md | 6 +++--- src/Data/List/Effectful/Foldable.agda | 16 +++++++--------- src/Data/Vec/Effectful/Foldable.agda | 20 ++++++++------------ 3 files changed, 18 insertions(+), 24 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 416820b5e2..92763aeca1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,11 +48,11 @@ New modules * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures -* `Data.List.Effectful.Foldable`: instance(s) of the following typeclass +* `Data.List.Effectful.Foldable`: `List` is `Foldable` -* `Data.Vec.Effectful.Foldable`: instance(s) of the following typeclass +* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable` -* `Effect.Foldable`: implementation of haskell-like typeclass +* `Effect.Foldable`: implementation of haskell-like `Foldable` Additions to existing modules ----------------------------- diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 7040c3fecb..188c885d10 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The Foldable instance of List +-- List is Foldable ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -12,18 +12,16 @@ 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 ≡ - +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 @@ -36,13 +34,13 @@ module _ (M : RawMonoid c ℓ) where foldMap f (x ∷ xs) = f x ∙ foldMap f xs ------------------------------------------------------------------------ --- Basic instance: using supplied defaults +-- Basic implementation using supplied defaults foldableWithDefaults : RawFoldableWithDefaults (List {a}) foldableWithDefaults = record { foldMap = λ M → foldMap M } ------------------------------------------------------------------------ --- Specialised instance: using optimised implementations +-- Specialised version using optimised implementations foldable : RawFoldable (List {a}) foldable = record diff --git a/src/Data/Vec/Effectful/Foldable.agda b/src/Data/Vec/Effectful/Foldable.agda index ddd9ab2111..4dedfff390 100644 --- a/src/Data/Vec/Effectful/Foldable.agda +++ b/src/Data/Vec/Effectful/Foldable.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The Foldable instance of Vec +-- Vec is Foldable ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -9,14 +9,11 @@ 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) +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 @@ -24,7 +21,6 @@ private A : Set a n : ℕ - ------------------------------------------------------------------------ -- Root implementation @@ -37,13 +33,13 @@ module _ (M : RawMonoid c ℓ) where foldMap f (x ∷ xs) = f x ∙ foldMap f xs ------------------------------------------------------------------------ --- Basic instance: using supplied defaults +-- Basic implementation using supplied defaults foldableWithDefaults : RawFoldableWithDefaults {a} (λ A → Vec A n) foldableWithDefaults = record { foldMap = λ M → foldMap M } ------------------------------------------------------------------------ --- Specialised instance: using optimised implementations +-- Specialised version using optimised implementations foldable : RawFoldable {a} (λ A → Vec A n) foldable = record From 976dff6283a92e806b9983d204221604ac3ab771 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 7 Dec 2024 05:21:21 +0000 Subject: [PATCH 15/15] Update Foldable.agda Fixes the deprecated module import i hope --- src/Effect/Foldable.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Effect/Foldable.agda b/src/Effect/Foldable.agda index 991d1b838c..de25c8faf6 100644 --- a/src/Effect/Foldable.agda +++ b/src/Effect/Foldable.agda @@ -19,7 +19,7 @@ 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 Function.Endo.Propositional using (∘-id-monoid) open import Level using (Level; Setω) open import Relation.Binary.Bundles using (Setoid)