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