module Haskell.Data.Bifoldable where

open import Haskell.Prelude

--------------------------------------------------------------------------------

record Bifoldable (p : Type → Type → Type) : Type₁ where
  field
    bifoldMap : ∀ {a b m} ⦃ _ : Monoid m ⦄ → (a → m) → (b → m) → p a b → m
    bifoldr   : {a b c : Type} → (a → c → c) → (b → c → c) → c → p a b → c

  bifold : ∀ {m} ⦃ _ : Monoid m ⦄ → p m m → m
  bifold = bifoldMap id id

record BifoldableFromBifoldMap (p : Type → Type → Type) : Type₁ where
  field
    bifoldMap : ∀ {a b m} ⦃ _ : Monoid m ⦄ → (a → m) → (b → m) → p a b → m

  bifoldr : {a b c : Type} → (a → c → c) → (b → c → c) → c → p a b → c
  bifoldr f g z t = bifoldMap ⦃ MonoidEndo ⦄ f g t z

record BifoldableFromBifoldr (p : Type → Type → Type) : Type₁ where
  field
    bifoldr : {a b c : Type} → (a → c → c) → (b → c → c) → c → p a b → c

  bifoldMap : ∀ {a b m} ⦃ _ : Monoid m ⦄ → (a → m) → (b → m) → p a b → m
  bifoldMap f g = bifoldr (_<>_ ∘ f) (_<>_ ∘ g) mempty

open Bifoldable ⦃ ... ⦄ public
{-# COMPILE AGDA2HS Bifoldable existing-class #-}

--------------------------------------------------------------------------------

instance

  iBifoldableFromBifoldMapTuple : BifoldableFromBifoldMap _×_
  iBifoldableFromBifoldMapTuple .BifoldableFromBifoldMap.bifoldMap f g (x , y) = f x <> g y

  iBifoldableTuple : Bifoldable _×_
  iBifoldableTuple = record {BifoldableFromBifoldMap iBifoldableFromBifoldMapTuple}

  iBifoldableFromBifoldMapEither : BifoldableFromBifoldMap Either
  iBifoldableFromBifoldMapEither .BifoldableFromBifoldMap.bifoldMap f g (Left x)  = f x
  iBifoldableFromBifoldMapEither .BifoldableFromBifoldMap.bifoldMap f g (Right y) = g y

  iBifoldableEither : Bifoldable Either
  iBifoldableEither = record {BifoldableFromBifoldMap iBifoldableFromBifoldMapEither}