module Proarrow.Monoid where

import Data.Kind (Type, Constraint)
import Prelude qualified as P

import Proarrow.Core (CategoryOf(..), Promonad(..), arr)
import Proarrow.Category.Monoidal (Monoidal(..))
import Proarrow.Object.BinaryProduct ((&&&), Cartesian)
import Proarrow.Object.Terminal (terminate)


type Monoid :: forall {k}. k -> Constraint
class (Monoidal k, Ob m) => Monoid (m :: k) where
  mempty :: Unit ~> m
  mappend :: m ** m ~> m

instance P.Monoid m => Monoid (m :: Type) where
  mempty :: Unit ~> m
mempty () = m
forall a. Monoid a => a
P.mempty
  mappend :: (m ** m) ~> m
mappend = (m -> m -> m) -> (m, m) -> m
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry m -> m -> m
forall a. Semigroup a => a -> a -> a
(P.<>)

newtype GenElt x m = GenElt (x ~> m)

instance (Monoid m, Cartesian k) => P.Semigroup (GenElt x (m :: k)) where
  GenElt x ~> m
f <> :: GenElt x m -> GenElt x m -> GenElt x m
<> GenElt x ~> m
g = (x ~> m) -> GenElt x m
forall {k} (x :: k) (m :: k). (x ~> m) -> GenElt x m
GenElt ((m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m) -> (x ~> (m ** m)) -> x ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> m
f (x ~> m) -> (x ~> m) -> x ~> (m && m)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& x ~> m
g))
instance (Monoid m, Cartesian k, Ob x) => P.Monoid (GenElt x (m :: k)) where
  mempty :: GenElt x m
mempty = (x ~> m) -> GenElt x m
forall {k} (x :: k) (m :: k). (x ~> m) -> GenElt x m
GenElt (Unit ~> m
TerminalObject ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty (TerminalObject ~> m) -> (x ~> TerminalObject) -> x ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> TerminalObject) -> x ~> TerminalObject
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr x ~> TerminalObject
forall {k} (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)

class (Monoidal k, Ob c) => Comonoid (c :: k) where
  counit :: c ~> Unit
  comult :: c ~> c ** c