{-# 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 (f,a) = f a
curry = Prelude.curry
uncurry = 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 = curry braid
counitCCC :: CCC k => Product k b (Exp k b a) `k` a
counitCCC = apply . 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 = swap . coapply
counitCoCCC :: CoCCC k => Coexp k b (Sum k b a) `k` a
counitCoCCC = cocurry swap