module Haskell.Prim.Monoid where
open import Haskell.Prim
open import Haskell.Prim.Bool
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either
open import Haskell.Prim.Tuple
record Semigroup (a : Set) : Set where
infixr 6 _<>_
field
_<>_ : a → a → a
open Semigroup ⦃ ... ⦄ public
{-# COMPILE AGDA2HS Semigroup existing-class #-}
instance
iSemigroupList : Semigroup (List a)
iSemigroupList ._<>_ = _++_
iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a)
iSemigroupMaybe ._<>_ Nothing m = m
iSemigroupMaybe ._<>_ m Nothing = m
iSemigroupMaybe ._<>_ (Just x) (Just y) = Just (x <> y)
iSemigroupEither : Semigroup (Either a b)
iSemigroupEither ._<>_ (Left _) e = e
iSemigroupEither ._<>_ e _ = e
iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b)
iSemigroupFun ._<>_ f g x = f x <> g x
iSemigroupUnit : Semigroup ⊤
iSemigroupUnit ._<>_ _ _ = tt
iSemigroupTuple₀ : Semigroup (Tuple [])
iSemigroupTuple₀ ._<>_ _ _ = tt
iSemigroupTuple : ⦃ Semigroup a ⦄ → ⦃ Semigroup (Tuple as) ⦄ → Semigroup (Tuple (a ∷ as))
iSemigroupTuple ._<>_ (x ; xs) (y ; ys) = x <> y ; xs <> ys
record Monoid (a : Set) : Set where
field
mempty : a
overlap ⦃ super ⦄ : Semigroup a
mappend : a → a → a
mappend = _<>_
mconcat : List a → a
mconcat [] = mempty
mconcat (x ∷ xs) = x <> mconcat xs
open Monoid ⦃ ... ⦄ public
{-# COMPILE AGDA2HS Monoid existing-class #-}
instance
iMonoidList : Monoid (List a)
iMonoidList .mempty = []
iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a)
iMonoidMaybe .mempty = Nothing
iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b)
iMonoidFun .mempty _ = mempty
iMonoidUnit : Monoid ⊤
iMonoidUnit .mempty = tt
iMonoidTuple₀ : Monoid (Tuple [])
iMonoidTuple₀ .mempty = tt
iMonoidTuple : ⦃ Monoid a ⦄ → ⦃ Monoid (Tuple as) ⦄ → Monoid (Tuple (a ∷ as))
iMonoidTuple .mempty = mempty ; mempty
MonoidEndo : Monoid (a → a)
MonoidEndo .mempty = id
MonoidEndo .super ._<>_ = _∘_
MonoidEndoᵒᵖ : Monoid (a → a)
MonoidEndoᵒᵖ .mempty = id
MonoidEndoᵒᵖ .super ._<>_ = flip _∘_
MonoidConj : Monoid Bool
MonoidConj .mempty = True
MonoidConj .super ._<>_ = _&&_
MonoidDisj : Monoid Bool
MonoidDisj .mempty = False
MonoidDisj .super ._<>_ = _||_