------------------------------------------------------------------------
-- 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
}
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