module Haskell.Data.Bifoldable where
open import Haskell.Prim using (Type; id; _∘_)
open import Haskell.Prim.Functor using (Functor)
open import Haskell.Prim.Monoid using (Monoid; MonoidEndo; _<>_; mempty)
open import Haskell.Prim.Tuple using (_×_; _,_; fst; snd)
open import Haskell.Prim.Either using (Either; Left; Right)
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}