{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators, FlexibleContexts #-}
module Control.Category.Cartesian.Closed
(
CCC(..)
, unitCCC, counitCCC
, CoCCC(..)
, unitCoCCC, counitCoCCC
) where
import Prelude ()
import qualified Prelude
import Control.Category
import Control.Category.Braided
import Control.Category.Cartesian
class Cartesian k => CCC k where
type Exp k :: * -> * -> *
apply :: Product k (Exp k a b) a `k` b
curry :: Product k a b `k` c -> a `k` Exp k b c
uncurry :: a `k` Exp k b c -> Product k a b `k` c
instance CCC (->) where
type Exp (->) = (->)
apply :: forall a b. Product (->) (Exp (->) a b) a -> b
apply (a -> b
f,a
a) = a -> b
f a
a
curry :: forall a b c. (Product (->) a b -> c) -> a -> Exp (->) b c
curry = (Product (->) a b -> c) -> a -> Exp (->) b c
forall a b c. ((a, b) -> c) -> a -> b -> c
Prelude.curry
uncurry :: forall a b c. (a -> Exp (->) b c) -> Product (->) a b -> c
uncurry = (a -> Exp (->) b c) -> Product (->) a b -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
Prelude.uncurry
{-# RULES
"curry apply" curry apply = id
-- "curry . uncurry" curry . uncurry = id
-- "uncurry . curry" uncurry . curry = id
#-}
unitCCC :: CCC k => a `k` Exp k b (Product k b a)
unitCCC :: forall (k :: * -> * -> *) a b.
CCC k =>
k a (Exp k b (Product k b a))
unitCCC = k (Product k a b) (Product k b a) -> k a (Exp k b (Product k b a))
forall (k :: * -> * -> *) a b c.
CCC k =>
k (Product k a b) c -> k a (Exp k b c)
curry 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
counitCCC :: CCC k => Product k b (Exp k b a) `k` a
counitCCC :: forall (k :: * -> * -> *) b a.
CCC k =>
k (Product k b (Exp k b a)) a
counitCCC = k (Product k (Exp k b a) b) a
forall (k :: * -> * -> *) a b.
CCC k =>
k (Product k (Exp k a b) a) b
apply k (Product k (Exp k b a) b) a
-> k (Product k b (Exp k b a)) (Product k (Exp k b a) b)
-> k (Product k b (Exp k b a)) a
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 (Exp k b a)) (Product k (Exp k b a) b)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Braided k p =>
k (p a b) (p b a)
braid
class CoCartesian k => CoCCC k where
type Coexp k :: * -> * -> *
coapply :: b `k` Sum k (Coexp k a b) a
cocurry :: c `k` Sum k a b -> Coexp k b c `k` a
uncocurry :: Coexp k b c `k` a -> c `k` Sum k a b
{-# RULES
"cocurry coapply" cocurry coapply = id
-- "cocurry . uncocurry" cocurry . uncocurry = id
-- "uncocurry . cocurry" uncocurry . cocurry = id
#-}
unitCoCCC :: CoCCC k => a `k` Sum k b (Coexp k b a)
unitCoCCC :: forall (k :: * -> * -> *) a b.
CoCCC k =>
k a (Sum k b (Coexp k b a))
unitCoCCC = k (Sum k (Coexp k b a) b) (Sum k b (Coexp k b a))
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Symmetric k p =>
k (p a b) (p b a)
swap k (Sum k (Coexp k b a) b) (Sum k b (Coexp k b a))
-> k a (Sum k (Coexp k b a) b) -> k a (Sum k b (Coexp k b a))
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 (Coexp k b a) b)
forall (k :: * -> * -> *) b a.
CoCCC k =>
k b (Sum k (Coexp k a b) a)
coapply
counitCoCCC :: CoCCC k => Coexp k b (Sum k b a) `k` a
counitCoCCC :: forall (k :: * -> * -> *) b a.
CoCCC k =>
k (Coexp k b (Sum k b a)) a
counitCoCCC = k (Sum k b a) (Sum k a b) -> k (Coexp k b (Sum k b a)) a
forall (k :: * -> * -> *) c a b.
CoCCC k =>
k c (Sum k a b) -> k (Coexp k b c) a
cocurry k (Sum k b a) (Sum k a b)
forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
Symmetric k p =>
k (p a b) (p b a)
swap