{-# 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)
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