{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators, FlexibleContexts #-}
-------------------------------------------------------------------------------------------
-- |
-- Module     : Control.Category.Cartesian.Closed
-- Copyright  : 2008 Edward Kmett
-- License    : BSD
--
-- Maintainer : Edward Kmett <ekmett@gmail.com>
-- Stability  : experimental
-- Portability: non-portable (class-associated types)
--
-------------------------------------------------------------------------------------------
module Control.Category.Cartesian.Closed
    (
    -- * Cartesian Closed Category
      CCC(..)
    , unitCCC, counitCCC
    -- * Co-(Cartesian Closed Category)
    , CoCCC(..)
    , unitCoCCC, counitCoCCC
    ) where

import Prelude ()
import qualified Prelude

import Control.Category
import Control.Category.Braided
import Control.Category.Cartesian

-- * Closed Cartesian Category

-- | A 'CCC' has full-fledged monoidal finite products and exponentials

-- Ideally you also want an instance for @'Bifunctor' ('Exp' hom) ('Dual' hom) hom hom@.
-- or at least @'Functor' ('Exp' hom a) hom hom@, which cannot be expressed in the constraints here.

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 = ((a, b) -> c) -> a -> b -> c
(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
(a -> b -> c) -> (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
 #-}

-- * Free @'Adjunction' (Product (<=) a) (Exp (<=) a) (<=) (<=)@
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 a b c. k (Product k a b) c -> k a (Exp k b c)
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 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

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 a b. k (Product k (Exp k a b) a) b
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 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 (Exp k b a)) (Product k (Exp k b 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

-- * A Co-(Closed Cartesian Category)

-- | A Co-CCC has full-fledged comonoidal finite coproducts and coexponentials

-- You probably also want an instance for @'Bifunctor' ('coexp' hom) ('Dual' hom) hom hom@.

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
 #-}

-- * Free @'Adjunction' ('Coexp' (<=) a) ('Sum' (<=) a) (<=) (<=)@
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 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 (Coexp k b a) b)
forall b a. k b (Sum k (Coexp k a b) a)
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 c a b. k c (Sum k a b) -> k (Coexp k b c) 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