{-# LANGUAGE DefaultSignatures #-}
module Control.Category.Monoidal where

import Control.Category (Category, (>>>))
import qualified Control.Arrow as A

class SymmetricProduct k => MonoidalProduct k where
  {-# MINIMAL first' | second' #-}
  (***) :: (al `k` bl) -> (ar `k` br) -> ((al, ar) `k` (bl, br))
  k al bl
l *** k ar br
r = k al bl -> k (al, ar) (bl, ar)
forall (k :: * -> * -> *) a b c.
MonoidalProduct k =>
k a b -> k (a, c) (b, c)
first' k al bl
l k (al, ar) (bl, ar) -> k (bl, ar) (bl, br) -> k (al, ar) (bl, br)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k ar br -> k (bl, ar) (bl, br)
forall (k :: * -> * -> *) a b c.
MonoidalProduct k =>
k a b -> k (c, a) (c, b)
second' k ar br
r
  first' :: (a `k` b) -> ((a, c) `k` (b, c))
  first' k a b
f = k (a, c) (c, a)
forall (k :: * -> * -> *) l r.
SymmetricProduct k =>
k (l, r) (r, l)
swap k (a, c) (c, a) -> k (c, a) (b, c) -> k (a, c) (b, c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k a b -> k (c, a) (c, b)
forall (k :: * -> * -> *) a b c.
MonoidalProduct k =>
k a b -> k (c, a) (c, b)
second' k a b
f k (c, a) (c, b) -> k (c, b) (b, c) -> k (c, a) (b, c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k (c, b) (b, c)
forall (k :: * -> * -> *) l r.
SymmetricProduct k =>
k (l, r) (r, l)
swap
  second' :: (a `k` b) -> ((c, a) `k` (c, b))
  second' k a b
f = k (c, a) (a, c)
forall (k :: * -> * -> *) l r.
SymmetricProduct k =>
k (l, r) (r, l)
swap k (c, a) (a, c) -> k (a, c) (c, b) -> k (c, a) (c, b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k a b -> k (a, c) (b, c)
forall (k :: * -> * -> *) a b c.
MonoidalProduct k =>
k a b -> k (a, c) (b, c)
first' k a b
f k (a, c) (b, c) -> k (b, c) (c, b) -> k (a, c) (c, b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k (b, c) (c, b)
forall (k :: * -> * -> *) l r.
SymmetricProduct k =>
k (l, r) (r, l)
swap

instance MonoidalProduct (->) where
  *** :: (al -> bl) -> (ar -> br) -> (al, ar) -> (bl, br)
(***) = (al -> bl) -> (ar -> br) -> (al, ar) -> (bl, br)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
(A.***)
  first' :: (a -> b) -> (a, c) -> (b, c)
first' = (a -> b) -> (a, c) -> (b, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
A.first
  second' :: (a -> b) -> (c, a) -> (c, b)
second' = (a -> b) -> (c, a) -> (c, b)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
A.second

class SymmetricSum k => MonoidalSum k where
  {-# MINIMAL left | right #-}
  (+++) :: (al `k` bl) -> (ar `k` br) -> ((Either al ar) `k` (Either bl br))
  k al bl
l +++ k ar br
r = k al bl -> k (Either al ar) (Either bl ar)
forall (k :: * -> * -> *) a b c.
MonoidalSum k =>
k a b -> k (Either a c) (Either b c)
left k al bl
l k (Either al ar) (Either bl ar)
-> k (Either bl ar) (Either bl br)
-> k (Either al ar) (Either bl br)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k ar br -> k (Either bl ar) (Either bl br)
forall (k :: * -> * -> *) a b c.
MonoidalSum k =>
k a b -> k (Either c a) (Either c b)
right k ar br
r
  left :: (a `k` b) -> ((Either a c) `k` (Either b c))
  left k a b
f = k (Either a c) (Either c a)
forall (k :: * -> * -> *) l r.
SymmetricSum k =>
k (Either l r) (Either r l)
swapE k (Either a c) (Either c a)
-> k (Either c a) (Either b c) -> k (Either a c) (Either b c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k a b -> k (Either c a) (Either c b)
forall (k :: * -> * -> *) a b c.
MonoidalSum k =>
k a b -> k (Either c a) (Either c b)
right k a b
f k (Either c a) (Either c b)
-> k (Either c b) (Either b c) -> k (Either c a) (Either b c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k (Either c b) (Either b c)
forall (k :: * -> * -> *) l r.
SymmetricSum k =>
k (Either l r) (Either r l)
swapE
  right :: (a `k` b) -> ((Either c a) `k` (Either c b))
  right k a b
f = k (Either c a) (Either a c)
forall (k :: * -> * -> *) l r.
SymmetricSum k =>
k (Either l r) (Either r l)
swapE k (Either c a) (Either a c)
-> k (Either a c) (Either c b) -> k (Either c a) (Either c b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k a b -> k (Either a c) (Either b c)
forall (k :: * -> * -> *) a b c.
MonoidalSum k =>
k a b -> k (Either a c) (Either b c)
left k a b
f k (Either a c) (Either b c)
-> k (Either b c) (Either c b) -> k (Either a c) (Either c b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> k (Either b c) (Either c b)
forall (k :: * -> * -> *) l r.
SymmetricSum k =>
k (Either l r) (Either r l)
swapE

instance MonoidalSum (->) where
  al -> bl
l +++ :: (al -> bl) -> (ar -> br) -> Either al ar -> Either bl br
+++ ar -> br
r = al -> bl
l (al -> bl) -> (ar -> br) -> Either al ar -> Either bl br
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
A.+++ ar -> br
r
  left :: (a -> b) -> Either a c -> Either b c
left = (a -> b) -> Either a c -> Either b c
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
A.left
  right :: (a -> b) -> Either c a -> Either c b
right = (a -> b) -> Either c a -> Either c b
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
A.right

class Category k => SymmetricProduct k where
  swap :: (l, r) `k` (r, l)
  reassoc :: (a, (b, c)) `k` ((a, b), c)

class Category k => SymmetricSum k where
  swapE :: (Either l r) `k` (Either r l)
  reassocE :: (Either a (Either b c)) `k` Either (Either a b) c

instance SymmetricProduct (->) where
  swap :: (l, r) -> (r, l)
swap (l
a, r
b) = (r
b, l
a)
  reassoc :: (a, (b, c)) -> ((a, b), c)
reassoc (a
a, (b
b, c
c)) = ((a
a, b
b), c
c)

instance SymmetricSum (->) where
  swapE :: Either l r -> Either r l
swapE (Left l
a) = l -> Either r l
forall a b. b -> Either a b
Right l
a
  swapE (Right r
a) = r -> Either r l
forall a b. a -> Either a b
Left r
a
  reassocE :: Either a (Either b c) -> Either (Either a b) c
reassocE (Left a
a) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (a -> Either a b
forall a b. a -> Either a b
Left a
a)
  reassocE (Right (Left b
b)) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (b -> Either a b
forall a b. b -> Either a b
Right b
b)
  reassocE (Right (Right c
c)) = c -> Either (Either a b) c
forall a b. b -> Either a b
Right c
c

class CategoryPlus k => CategoryZero k where
  zeroC :: k a b

class Category k => CategoryPlus k where
  (<+>) :: k a b -> k a b -> k a b