{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
-------------------------------------------------------------------------------------------
-- |
-- Module    : Control.Category.Cartesian
-- Copyright : 2008-2010 Edward Kmett
-- License   : BSD
--
-- Maintainer  : Edward Kmett <ekmett@gmail.com>
-- Stability   : experimental
-- Portability : non-portable (class-associated types)
--
-------------------------------------------------------------------------------------------
module Control.Category.Cartesian
    (
    -- * (Co)Cartesian categories
      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 |||

{- |
Minimum definition:

> fst, snd, diag
> fst, snd, (&&&)
-}
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 = k a a
forall a. k a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id k a a -> k a a -> k a (Product k a a)
forall a b c. k a b -> k a c -> k a (Product k b c)
forall (k :: * -> * -> *) a b c.
Cartesian k =>
k a b -> k a c -> k a (Product k b c)
&&& k a a
forall a. k a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
    k a b
f &&& k a c
g = k a b -> k a c -> k (Product k a a) (Product k b c)
forall a b c d. k a b -> k c d -> k (Product k a c) (Product k b d)
forall (p :: * -> * -> *) (r :: * -> * -> *) (s :: * -> * -> *)
       (t :: * -> * -> *) a b c d.
Bifunctor p r s t =>
r a b -> s c d -> t (p a c) (p b d)
bimap k a b
f k a c
g k (Product k a a) (Product k b c)
-> k a (Product k a a) -> k a (Product k b c)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k a (Product k a a)
forall a. k a (Product k a a)
forall (k :: * -> * -> *) a. Cartesian k => k a (Product k a a)
diag

{-- RULES
"fst . diag"      fst . diag = id
"snd . diag"    snd . diag = id
"fst . f &&& g" forall f g. fst . (f &&& g) = f
"snd . f &&& g" forall f g. snd . (f &&& g) = g
 --}

instance Cartesian (->) where
    type Product (->) = (,)
    fst :: forall a b. Product (->) a b -> a
fst = (a, b) -> a
Product (->) a b -> a
forall a b. (a, b) -> a
Prelude.fst
    snd :: forall a b. Product (->) a b -> b
snd = (a, b) -> b
Product (->) a b -> b
forall a b. (a, b) -> b
Prelude.snd
    diag :: forall a. a -> Product (->) a a
diag a
a = (a
a,a
a)
    (a -> b
f &&& :: forall a b c. (a -> b) -> (a -> c) -> a -> Product (->) b c
&&& a -> c
g) a
a = (a -> b
f a
a, a -> c
g a
a)

-- | free construction of 'Bifunctor' for the product 'Bifunctor' @Product k@ if @(&&&)@ is known
bimapProduct :: Cartesian k => k a c -> k b d -> Product k a b `k` Product k c d
bimapProduct :: forall (k :: * -> * -> *) a c b d.
Cartesian k =>
k a c -> k b d -> k (Product k a b) (Product k c d)
bimapProduct k a c
f k b d
g = (k a c
f k a c -> k (Product k a b) a -> k (Product k a b) c
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Product k a b) a
forall a b. k (Product k a b) a
forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
fst) k (Product k a b) c
-> k (Product k a b) d -> k (Product k a b) (Product k c d)
forall a b c. k a b -> k a c -> k a (Product k b c)
forall (k :: * -> * -> *) a b c.
Cartesian k =>
k a b -> k a c -> k a (Product k b c)
&&& (k b d
g k b d -> k (Product k a b) b -> k (Product k a b) d
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Product k a b) b
forall a b. k (Product k a b) b
forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) b
snd)

-- | free construction of 'Braided' for the product 'Bifunctor' @Product k@
braidProduct :: Cartesian k => k (Product k a b) (Product k b a)
braidProduct :: forall (k :: * -> * -> *) a b.
Cartesian k =>
k (Product k a b) (Product k b a)
braidProduct = k (Product k a b) b
forall a b. k (Product k a b) b
forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) b
snd k (Product k a b) b
-> k (Product k a b) a -> k (Product k a b) (Product k b a)
forall a b c. k a b -> k a c -> k a (Product k b c)
forall (k :: * -> * -> *) a b c.
Cartesian k =>
k a b -> k a c -> k a (Product k b c)
&&& k (Product k a b) a
forall a b. k (Product k a b) a
forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
fst

-- | free construction of 'Associative' for the product 'Bifunctor' @Product k@
associateProduct :: Cartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)
associateProduct :: forall (k :: * -> * -> *) a b c.
Cartesian k =>
k (Product k (Product k a b) c) (Product k a (Product k b c))
associateProduct = (k (Product k a b) a
forall a b. k (Product k a b) a
forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
fst k (Product k a b) a
-> k (Product k (Product k a b) c) (Product k a b)
-> k (Product k (Product k a b) c) a
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Product k (Product k a b) c) (Product k a b)
forall a b. k (Product k a b) a
forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
fst) k (Product k (Product k a b) c) a
-> k (Product k (Product k a b) c) (Product k b c)
-> k (Product k (Product k a b) c) (Product k a (Product k b c))
forall a b c. k a b -> k a c -> k a (Product k b c)
forall (k :: * -> * -> *) a b c.
Cartesian k =>
k a b -> k a c -> k a (Product k b c)
&&& k (Product k a b) b
-> k (Product k (Product k a b) c) (Product k b c)
forall a b c. k a b -> k (Product k a c) (Product k b c)
forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
       c.
PFunctor p r t =>
r a b -> t (p a c) (p b c)
first k (Product k a b) b
forall a b. k (Product k a b) b
forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) b
snd

-- | free construction of 'Disassociative' for the product 'Bifunctor' @Product k@
disassociateProduct:: Cartesian k => Product k a (Product k b c) `k` Product k (Product k a b) c
disassociateProduct :: forall (k :: * -> * -> *) a b c.
Cartesian k =>
k (Product k a (Product k b c)) (Product k (Product k a b) c)
disassociateProduct= k (Product k c (Product k a b)) (Product k (Product k a b) c)
forall a b. k (Product k a b) (Product k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid k (Product k c (Product k a b)) (Product k (Product k a b) c)
-> k (Product k a (Product k b c)) (Product k c (Product k a b))
-> k (Product k a (Product k b c)) (Product k (Product k a b) c)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Product k b a) (Product k a b)
-> k (Product k c (Product k b a)) (Product k c (Product k a b))
forall a b c. k a b -> k (Product k c a) (Product k c b)
forall (q :: * -> * -> *) (s :: * -> * -> *) (t :: * -> * -> *) a b
       c.
QFunctor q s t =>
s a b -> t (q c a) (q c b)
second k (Product k b a) (Product k a b)
forall a b. k (Product k a b) (Product k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid k (Product k c (Product k b a)) (Product k c (Product k a b))
-> k (Product k a (Product k b c)) (Product k c (Product k b a))
-> k (Product k a (Product k b c)) (Product k c (Product k a b))
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Product k (Product k c b) a) (Product k c (Product k b a))
forall (k :: * -> * -> *) a b c.
Cartesian k =>
k (Product k (Product k a b) c) (Product k a (Product k b c))
associateProduct k (Product k (Product k c b) a) (Product k c (Product k b a))
-> k (Product k a (Product k b c)) (Product k (Product k c b) a)
-> k (Product k a (Product k b c)) (Product k c (Product k b a))
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Product k b c) (Product k c b)
-> k (Product k (Product k b c) a) (Product k (Product k c b) a)
forall a b c. k a b -> k (Product k a c) (Product k b c)
forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
       c.
PFunctor p r t =>
r a b -> t (p a c) (p b c)
first k (Product k b c) (Product k c b)
forall a b. k (Product k a b) (Product k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid k (Product k (Product k b c) a) (Product k (Product k c b) a)
-> k (Product k a (Product k b c)) (Product k (Product k b c) a)
-> k (Product k a (Product k b c)) (Product k (Product k c b) a)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Product k a (Product k b c)) (Product k (Product k b c) a)
forall a b. k (Product k a b) (Product k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid

-- * Co-Cartesian categories

-- a category that has finite coproducts, weakened the same way as PreCartesian above was weakened
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 = k a a
forall a. k a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id k a a -> k a a -> k (Sum k a a) a
forall a c b. k a c -> k b c -> k (Sum k a b) c
forall (k :: * -> * -> *) a c b.
CoCartesian k =>
k a c -> k b c -> k (Sum k a b) c
||| k a a
forall a. k a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
    k a c
f ||| k b c
g = k (Sum k c c) c
forall a. k (Sum k a a) a
forall (k :: * -> * -> *) a. CoCartesian k => k (Sum k a a) a
codiag k (Sum k c c) c -> k (Sum k a b) (Sum k c c) -> k (Sum k a b) c
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k a c -> k b c -> k (Sum k a b) (Sum k c c)
forall a b c d. k a b -> k c d -> k (Sum k a c) (Sum k b d)
forall (p :: * -> * -> *) (r :: * -> * -> *) (s :: * -> * -> *)
       (t :: * -> * -> *) a b c d.
Bifunctor p r s t =>
r a b -> s c d -> t (p a c) (p b d)
bimap k a c
f k b c
g

{-- RULES
"codiag . inl"  codiag . inl = id
"codiag . inr"    codiag . inr = id
"(f ||| g) . inl" forall f g. (f ||| g) . inl = f
"(f ||| g) . inr" forall f g. (f ||| g) . inr = g
 --}

instance CoCartesian (->) where
    type Sum (->) = Either
    inl :: forall a b. a -> Sum (->) a b
inl = a -> Either a b
a -> Sum (->) a b
forall a b. a -> Either a b
Left
    inr :: forall b a. b -> Sum (->) a b
inr = b -> Either a b
b -> Sum (->) a b
forall a b. b -> Either a b
Right
    codiag :: forall a. Sum (->) a a -> a
codiag (Left a
a) = a
a
    codiag (Right a
a) = a
a
    (a -> c
f ||| :: forall a c b. (a -> c) -> (b -> c) -> Sum (->) a b -> c
||| b -> c
_) (Left a
a) = a -> c
f a
a
    (a -> c
_ ||| b -> c
g) (Right b
a) = b -> c
g b
a

-- | free construction of 'Bifunctor' for the coproduct 'Bifunctor' @Sum k@ if @(|||)@ is known
bimapSum :: CoCartesian k => k a c -> k b d -> Sum k a b `k` Sum k c d
bimapSum :: forall (k :: * -> * -> *) a c b d.
CoCartesian k =>
k a c -> k b d -> k (Sum k a b) (Sum k c d)
bimapSum k a c
f k b d
g = (k c (Sum k c d)
forall a b. k a (Sum k a b)
forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
inl k c (Sum k c d) -> k a c -> k a (Sum k c d)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k a c
f) k a (Sum k c d) -> k b (Sum k c d) -> k (Sum k a b) (Sum k c d)
forall a c b. k a c -> k b c -> k (Sum k a b) c
forall (k :: * -> * -> *) a c b.
CoCartesian k =>
k a c -> k b c -> k (Sum k a b) c
||| (k d (Sum k c d)
forall b a. k b (Sum k a b)
forall (k :: * -> * -> *) b a. CoCartesian k => k b (Sum k a b)
inr k d (Sum k c d) -> k b d -> k b (Sum k c d)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k b d
g)

-- | free construction of 'Braided' for the coproduct 'Bifunctor' @Sum k@
braidSum :: CoCartesian k => Sum k a b `k` Sum k b a
braidSum :: forall (k :: * -> * -> *) a b.
CoCartesian k =>
k (Sum k a b) (Sum k b a)
braidSum = k a (Sum k b a)
forall b a. k b (Sum k a b)
forall (k :: * -> * -> *) b a. CoCartesian k => k b (Sum k a b)
inr k a (Sum k b a) -> k b (Sum k b a) -> k (Sum k a b) (Sum k b a)
forall a c b. k a c -> k b c -> k (Sum k a b) c
forall (k :: * -> * -> *) a c b.
CoCartesian k =>
k a c -> k b c -> k (Sum k a b) c
||| k b (Sum k b a)
forall a b. k a (Sum k a b)
forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
inl

-- | free construction of 'Associative' for the coproduct 'Bifunctor' @Sum k@
associateSum :: CoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)
associateSum :: forall (k :: * -> * -> *) a b c.
CoCartesian k =>
k (Sum k (Sum k a b) c) (Sum k a (Sum k b c))
associateSum = k (Sum k (Sum k b c) a) (Sum k a (Sum k b c))
forall a b. k (Sum k a b) (Sum k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid k (Sum k (Sum k b c) a) (Sum k a (Sum k b c))
-> k (Sum k (Sum k a b) c) (Sum k (Sum k b c) a)
-> k (Sum k (Sum k a b) c) (Sum k a (Sum k b c))
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Sum k c b) (Sum k b c)
-> k (Sum k (Sum k c b) a) (Sum k (Sum k b c) a)
forall a b c. k a b -> k (Sum k a c) (Sum k b c)
forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
       c.
PFunctor p r t =>
r a b -> t (p a c) (p b c)
first k (Sum k c b) (Sum k b c)
forall a b. k (Sum k a b) (Sum k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid k (Sum k (Sum k c b) a) (Sum k (Sum k b c) a)
-> k (Sum k (Sum k a b) c) (Sum k (Sum k c b) a)
-> k (Sum k (Sum k a b) c) (Sum k (Sum k b c) a)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Sum k c (Sum k b a)) (Sum k (Sum k c b) a)
forall (k :: * -> * -> *) a b c.
CoCartesian k =>
k (Sum k a (Sum k b c)) (Sum k (Sum k a b) c)
disassociateSum k (Sum k c (Sum k b a)) (Sum k (Sum k c b) a)
-> k (Sum k (Sum k a b) c) (Sum k c (Sum k b a))
-> k (Sum k (Sum k a b) c) (Sum k (Sum k c b) a)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Sum k a b) (Sum k b a)
-> k (Sum k c (Sum k a b)) (Sum k c (Sum k b a))
forall a b c. k a b -> k (Sum k c a) (Sum k c b)
forall (q :: * -> * -> *) (s :: * -> * -> *) (t :: * -> * -> *) a b
       c.
QFunctor q s t =>
s a b -> t (q c a) (q c b)
second k (Sum k a b) (Sum k b a)
forall a b. k (Sum k a b) (Sum k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid k (Sum k c (Sum k a b)) (Sum k c (Sum k b a))
-> k (Sum k (Sum k a b) c) (Sum k c (Sum k a b))
-> k (Sum k (Sum k a b) c) (Sum k c (Sum k b a))
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k (Sum k (Sum k a b) c) (Sum k c (Sum k a b))
forall a b. k (Sum k a b) (Sum k b a)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid

-- | free construction of 'Disassociative' for the coproduct 'Bifunctor' @Sum k@
disassociateSum :: CoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
disassociateSum :: forall (k :: * -> * -> *) a b c.
CoCartesian k =>
k (Sum k a (Sum k b c)) (Sum k (Sum k a b) c)
disassociateSum = (k (Sum k a b) (Sum k (Sum k a b) c)
forall a b. k a (Sum k a b)
forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
inl k (Sum k a b) (Sum k (Sum k a b) c)
-> k a (Sum k a b) -> k a (Sum k (Sum k a b) c)
forall b c a. k b c -> k a b -> k a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. k a (Sum k a b)
forall a b. k a (Sum k a b)
forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
inl) k a (Sum k (Sum k a b) c)
-> k (Sum k b c) (Sum k (Sum k a b) c)
-> k (Sum k a (Sum k b c)) (Sum k (Sum k a b) c)
forall a c b. k a c -> k b c -> k (Sum k a b) c
forall (k :: * -> * -> *) a c b.
CoCartesian k =>
k a c -> k b c -> k (Sum k a b) c
||| k b (Sum k a b) -> k (Sum k b c) (Sum k (Sum k a b) c)
forall a b c. k a b -> k (Sum k a c) (Sum k b c)
forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
       c.
PFunctor p r t =>
r a b -> t (p a c) (p b c)
first k b (Sum k a b)
forall b a. k b (Sum k a b)
forall (k :: * -> * -> *) b a. CoCartesian k => k b (Sum k a b)
inr