{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Monoid where

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

import Proarrow.Category (Supplies)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), par)
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), arr, dimapDefault, obj)
import Proarrow.Object.BinaryCoproduct (COPROD (..), Coprod (..), HasBinaryCoproducts (..), HasCoproducts, codiag)
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), HasProducts, PROD (..), Prod (..), diag, (&&&))
import Proarrow.Object.Dual (CompactClosed (..), StarAutonomous (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Identity (Id (..))

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

combine :: (Monoid m) => Unit ~> m -> Unit ~> m -> Unit ~> m
combine :: forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g = (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m) -> (Unit ~> (m ** m)) -> Unit ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Unit ~> m
f (Unit ~> m) -> (Unit ~> m) -> (Unit ** Unit) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` Unit ~> m
g) ((Unit ** Unit) ~> (m ** m))
-> (Unit ~> (Unit ** Unit)) -> Unit ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> (Unit ** Unit)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv

class (Monoid m) => CommutativeMonoid (m :: k)

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 :: 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 :: 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 :: 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 = Id InitialObject a -> Coprod Id ('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) -> Id InitialObject a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id 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 = Id (a || a) a -> Coprod Id ('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) -> Id (a || a) a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (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 :: 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 :: 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 Comonoid '() where
  counit :: '() ~> Unit
counit = '() ~> Unit
Unit '() '()
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ()). Ob a => Unit a a
id
  comult :: '() ~> ('() ** '())
comult = '() ~> ('() ** '())
Unit '() '()
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ()). Ob a => Unit a a
id

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 :: 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 :: 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)

class (Monoidal k) => CopyDiscard k where
  copy :: (Ob (a :: k)) => a ~> a ** a
  default copy :: (k `Supplies` Comonoid) => (Ob (a :: k)) => a ~> a ** a
  copy = a ~> (a ** a)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult
  discard :: (Ob (a :: k)) => a ~> Unit
  default discard :: (k `Supplies` Comonoid) => (Ob (a :: k)) => a ~> Unit
  discard = a ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit

instance (HasProducts k) => CopyDiscard (PROD k)
instance CopyDiscard Type
instance CopyDiscard ()
instance (CopyDiscard j, CopyDiscard k) => CopyDiscard (j, k) where
  copy :: forall (a :: (j, k)). Ob a => a ~> (a ** a)
copy = Fst a ~> (Fst a ** Fst a)
forall (a :: j). Ob a => a ~> (a ** a)
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy (Fst a ~> (Fst a ** Fst a))
-> (Snd a ~> (Snd a ** Snd a))
-> (:**:)
     (~>) (~>) '(Fst a, Snd a) '(Fst a ** Fst a, Snd a ** Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Snd a ~> (Snd a ** Snd a)
forall (a :: k). Ob a => a ~> (a ** a)
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: (j, k)). Ob a => a ~> Unit
discard = Fst a ~> Unit
forall (a :: j). Ob a => a ~> Unit
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard (Fst a ~> Unit)
-> (Snd a ~> Unit)
-> (:**:) (~>) (~>) '(Fst a, Snd a) '(Unit, Unit)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Snd a ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

type data MONOIDK (m :: k) = M
data Mon a b where
  Mon :: Unit ~> m -> Mon (M :: MONOIDK m) M
instance (Monoid m) => Profunctor (Mon :: CAT (MONOIDK m)) where
  dimap :: forall (c :: MONOIDK m) (a :: MONOIDK m) (b :: MONOIDK m)
       (d :: MONOIDK m).
(c ~> a) -> (b ~> d) -> Mon a b -> Mon c d
dimap = (c ~> a) -> (b ~> d) -> Mon a b -> Mon c d
Mon c a -> Mon b d -> Mon a b -> Mon c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
((Ob a, Ob b) => r) -> Mon a b -> r
\\ Mon{} = r
(Ob a, Ob b) => r
r
instance (Monoid m) => Promonad (Mon :: CAT (MONOIDK m)) where
  id :: forall (a :: MONOIDK m). Ob a => Mon a a
id = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f . :: forall (b :: MONOIDK m) (c :: MONOIDK m) (a :: MONOIDK m).
Mon b c -> Mon a b -> Mon a c
. Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)

-- | A monoid as a one object category.
instance (Monoid m) => CategoryOf (MONOIDK m) where
  type (~>) = Mon
  type Ob a = a P.~ M

instance (Monoid m) => HasInitialObject (MONOIDK m) where
  type InitialObject = M
  initiate :: forall (a :: MONOIDK m). Ob a => InitialObject ~> a
initiate = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (Monoid m) => HasTerminalObject (MONOIDK m) where
  type TerminalObject = M
  terminate :: forall (a :: MONOIDK m). Ob a => a ~> TerminalObject
terminate = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (Monoid m) => HasBinaryProducts (MONOIDK m) where
  type a && b = M
  withObProd :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @M @M Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(a && b) ~> a
fst @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  snd :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(a && b) ~> b
snd @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f &&& :: forall (a :: MONOIDK m) (x :: MONOIDK m) (y :: MONOIDK m).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)
instance (Monoid m) => HasBinaryCoproducts (MONOIDK m) where
  type a || b = M
  withObCoprod :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @M @M Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
a ~> (a || b)
lft @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rgt :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f ||| :: forall (x :: MONOIDK m) (a :: MONOIDK m) (y :: MONOIDK m).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)

instance (CommutativeMonoid m) => MonoidalProfunctor (Mon :: CAT (MONOIDK m)) where
  par0 :: Mon Unit Unit
par0 = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f par :: forall (x1 :: MONOIDK m) (x2 :: MONOIDK m) (y1 :: MONOIDK m)
       (y2 :: MONOIDK m).
Mon x1 x2 -> Mon y1 y2 -> Mon (x1 ** y1) (x2 ** y2)
`par` Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)
instance (CommutativeMonoid m) => Monoidal (MONOIDK m) where
  type Unit = M
  type M ** M = M
  withOb2 :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: MONOIDK m). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  leftUnitorInv :: forall (a :: MONOIDK m). Ob a => a ~> (Unit ** a)
leftUnitorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rightUnitor :: forall (a :: MONOIDK m). Ob a => (a ** Unit) ~> a
rightUnitor = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rightUnitorInv :: forall (a :: MONOIDK m). Ob a => a ~> (a ** Unit)
rightUnitorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  associator :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  associatorInv :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (CommutativeMonoid m) => SymMonoidal (MONOIDK m) where
  swap :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty

instance (CommutativeMonoid m) => StarAutonomous (MONOIDK m) where
  type Dual (M :: MONOIDK m) = M
  dual :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(a ~> b) -> Dual b ~> Dual a
dual f :: a ~> b
f@Mon{} = a ~> b
Dual b ~> Dual a
f
  dualInv :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv Dual a ~> Dual b
f = b ~> a
Dual a ~> Dual b
f
  linDist :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist (a ** b) ~> Dual c
_ = a ~> Dual (b ** c)
Mon M M
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MONOIDK m). Ob a => Mon a a
id
  linDistInv :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv a ~> Dual (b ** c)
_ = (a ** b) ~> Dual c
Mon M M
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MONOIDK m). Ob a => Mon a a
id
instance (CommutativeMonoid m) => CompactClosed (MONOIDK m) where
  distribDual :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  dualUnit :: Dual Unit ~> Unit
dualUnit = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (CommutativeMonoid m) => Closed (MONOIDK m) where
  type a ~~> b = M
  withObExp :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Mon Unit ~> m
m) = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
m
  apply :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty

instance (Comonoid c) => Monoid (OP c) where
  mempty :: Unit ~> 'OP c
mempty = (c ~> Unit) -> Op (~>) ('OP Unit) ('OP c)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  mappend :: ('OP c ** 'OP c) ~> 'OP c
mappend = (c ~> (c ** c)) -> Op (~>) ('OP (c ** c)) ('OP c)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

instance (Monoid c) => Comonoid (OP c) where
  counit :: 'OP c ~> Unit
counit = (Unit ~> c) -> Op (~>) ('OP c) ('OP Unit)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Unit ~> c
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  comult :: 'OP c ~> ('OP c ** 'OP c)
comult = ((c ** c) ~> c) -> Op (~>) ('OP c) ('OP (c ** c))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (c ** c) ~> c
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend