------------------------------------------------------------------------
-- 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 ≡ using (_≡_; cong)
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
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4