{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Monoid where

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

import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Core (CategoryOf (..), Promonad (..), arr, obj)
import Proarrow.Object.BinaryCoproduct (COPROD (..), Coprod (..), HasCoproducts, codiag)
import Proarrow.Object.BinaryProduct (Cartesian, HasProducts, PROD (..), Prod (..), diag, (&&&))
import Proarrow.Object.Initial (initiate)
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 (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)

instance (HasCoproducts k, Ob a) => Monoid (COPR (a :: k)) where
  mempty :: Unit ~> 'COPR a
mempty = (InitialObject ~> a) -> Coprod (~>) ('COPR InitialObject) ('COPR a)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
  mappend :: ('COPR a ** 'COPR a) ~> 'COPR a
mappend = ((a || a) ~> a) -> Coprod (~>) ('COPR (a || a)) ('COPR a)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (a || a) ~> a
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag

memptyAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Monoid a, Ob n) => n ~> Act a n
memptyAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
n ~> Act a n
memptyAct = (Unit ~> a) -> (n ~> n) -> Act Unit n ~> Act a n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (m :: m). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n) (Act Unit n ~> Act a n) -> (n ~> Act Unit n) -> n ~> Act a n
forall (b :: c) (c :: c) (a :: c). (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
. forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m

mappendAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Monoid a, Ob n) => Act a (Act a n) ~> Act a n
mappendAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
Act a (Act a n) ~> Act a n
mappendAct = ((a ** a) ~> a) -> (n ~> n) -> Act (a ** a) n ~> Act a n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (m :: m). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n) (Act (a ** a) n ~> Act a n)
-> (Act a (Act a n) ~> Act (a ** a) n)
-> Act a (Act a n) ~> Act a n
forall (b :: c) (c :: c) (a :: c). (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
. forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @c @a @a @n

type ModuleObject :: forall {m} {c}. m -> c -> Constraint
class (MonoidalAction m c, Monoid a, Ob n) => ModuleObject (a :: m) (n :: c) where
  action :: Act a n ~> n

type Comonoid :: forall {k}. k -> Constraint
class (Monoidal k, Ob c) => Comonoid (c :: k) where
  counit :: c ~> Unit
  comult :: c ~> c ** c

instance Comonoid (a :: Type) where
  counit :: a ~> Unit
counit a
_ = ()
  comult :: a ~> (a ** a)
comult a
a = (a
a, a
a)

instance (HasProducts k, Ob a) => Comonoid (PR (a :: k)) where
  counit :: 'PR a ~> Unit
counit = (a ~> TerminalObject) -> Prod (~>) ('PR a) ('PR TerminalObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  comult :: 'PR a ~> ('PR a ** 'PR a)
comult = (a ~> (a && a)) -> Prod (~>) ('PR a) ('PR (a && a))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag

counitAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Comonoid a, Ob n) => Act a n ~> n
counitAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> n
counitAct = forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m (Act Unit n ~> n) -> (Act a n ~> Act Unit n) -> Act a n ~> n
forall (b :: c) (c :: c) (a :: c). (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
. (a ~> Unit) -> (n ~> n) -> Act a n ~> Act Unit n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (c :: m). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n)

comultAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Comonoid a, Ob n) => Act a n ~> Act a (Act a n)
comultAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> Act a (Act a n)
comultAct = forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @c @a @a @n (Act (a ** a) n ~> Act a (Act a n))
-> (Act a n ~> Act (a ** a) n) -> Act a n ~> Act a (Act a n)
forall (b :: c) (c :: c) (a :: c). (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
. (a ~> (a ** a)) -> (n ~> n) -> Act a n ~> Act (a ** a) n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (c :: m). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n)