module Control.Category.Cartesian
(
Cartesian(..)
, bimapProduct, braidProduct, associateProduct, disassociateProduct
, CoCartesian(..)
, bimapSum, braidSum, associateSum, disassociateSum
) where
import Control.Category.Braided
import Control.Category.Monoidal
import Prelude hiding (Functor, map, (.), id, fst, snd, curry, uncurry)
import qualified Prelude (fst,snd)
import Control.Categorical.Bifunctor
import Control.Category
infixr 3 &&&
infixr 2 |||
class (Symmetric k (Product k), Monoidal k (Product k)) => Cartesian k where
type Product k :: * -> * -> *
fst :: Product k a b `k` a
snd :: Product k a b `k` b
diag :: a `k` Product k a a
(&&&) :: (a `k` b) -> (a `k` c) -> a `k` Product k b c
diag = id &&& id
f &&& g = bimap f g . diag
instance Cartesian (->) where
type Product (->) = (,)
fst = Prelude.fst
snd = Prelude.snd
diag a = (a,a)
(f &&& g) a = (f a, g a)
bimapProduct :: Cartesian k => k a c -> k b d -> Product k a b `k` Product k c d
bimapProduct f g = (f . fst) &&& (g . snd)
braidProduct :: Cartesian k => k (Product k a b) (Product k b a)
braidProduct = snd &&& fst
associateProduct :: Cartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)
associateProduct = (fst . fst) &&& first snd
disassociateProduct:: Cartesian k => Product k a (Product k b c) `k` Product k (Product k a b) c
disassociateProduct= braid . second braid . associateProduct . first braid . braid
class (Monoidal k (Sum k), Symmetric k (Sum k)) => CoCartesian k where
type Sum k :: * -> * -> *
inl :: a `k` Sum k a b
inr :: b `k` Sum k a b
codiag :: Sum k a a `k` a
(|||) :: k a c -> k b c -> Sum k a b `k` c
codiag = id ||| id
f ||| g = codiag . bimap f g
instance CoCartesian (->) where
type Sum (->) = Either
inl = Left
inr = Right
codiag (Left a) = a
codiag (Right a) = a
(f ||| _) (Left a) = f a
(_ ||| g) (Right a) = g a
bimapSum :: CoCartesian k => k a c -> k b d -> Sum k a b `k` Sum k c d
bimapSum f g = (inl . f) ||| (inr . g)
braidSum :: CoCartesian k => Sum k a b `k` Sum k b a
braidSum = inr ||| inl
associateSum :: CoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)
associateSum = braid . first braid . disassociateSum . second braid . braid
disassociateSum :: CoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
disassociateSum = (inl . inl) ||| first inr