module Control.Category.Cartesian
(
PreCartesian(..)
, bimapProduct, braidProduct, associateProduct, disassociateProduct
, PreCoCartesian(..)
, bimapSum, braidSum, associateSum, disassociateSum
, Cartesian
, CoCartesian
) where
import Control.Category.Associative
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 ( Associative k (Product k)
, Disassociative k (Product k)
, Symmetric k (Product k)
, Braided k (Product k)
) => PreCartesian 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 PreCartesian (->) where
type Product (->) = (,)
fst = Prelude.fst
snd = Prelude.snd
diag a = (a,a)
(f &&& g) a = (f a, g a)
class ( Monoidal k (Product k)
, PreCartesian k
) => Cartesian k
instance ( Monoidal k (Product k)
, PreCartesian k
) => Cartesian k
bimapProduct :: (PreCartesian k, (<*>) ~ Product k) => (a `k` c) -> (b `k` d) -> (a <*> b) `k` (c <*> d)
bimapProduct f g = (f . fst) &&& (g . snd)
braidProduct :: (PreCartesian k) => Product k a b `k` Product k b a
braidProduct = snd &&& fst
associateProduct :: (PreCartesian k) => Product k (Product k a b) c `k` Product k a (Product k b c)
associateProduct = (fst . fst) &&& first snd
disassociateProduct:: (PreCartesian 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 ( Associative k (Sum k)
, Disassociative k (Sum k)
, Symmetric k (Product k)
, Braided k (Sum k)
) => PreCoCartesian 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
(|||) :: (a `k` c) -> (b `k` c) -> Sum k a b `k` c
codiag = id ||| id
f ||| g = codiag . bimap f g
instance PreCoCartesian (->) 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 :: (PreCoCartesian k, Sum k ~ (+)) => (a `k` c) -> (b `k` d) -> (a + b) `k` (c + d)
bimapSum f g = (inl . f) ||| (inr . g)
braidSum :: (PreCoCartesian k, (+) ~ Sum k) => (a + b) `k` (b + a)
braidSum = inr ||| inl
associateSum :: (PreCoCartesian 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 :: (PreCoCartesian k) => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
disassociateSum = (inl . inl) ||| first inr
class
( Comonoidal k (Sum k)
, PreCoCartesian k
) => CoCartesian k
instance
( Comonoidal k (Sum k)
, PreCoCartesian k
) => CoCartesian k