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