{-# LANGUAGE
  TypeOperators,
  TypeFamilies,
  GADTs,
  PolyKinds,
  DataKinds,
  Rank2Types,
  PatternSynonyms,
  ScopedTypeVariables,
  UndecidableInstances,
  TypeSynonymInstances,
  FlexibleInstances,
  TupleSections,
  NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.CartesianClosed
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.CartesianClosed where

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Product
import Data.Category.Limit
import Data.Category.Adjunction
import Data.Category.Monoidal as M
import Data.Category.Yoneda
import qualified Data.Category.Unit as U


-- | A category is cartesian closed if it has all products and exponentials for all objects.
class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
  type Exponential k (y :: Kind k) (z :: Kind k) :: Kind k

  apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
  tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
  (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)


data ExpFunctor (k :: Type -> Type -> Type) = ExpFunctor
-- | The exponential as a bifunctor.
instance CartesianClosed k => Functor (ExpFunctor k) where
  type Dom (ExpFunctor k) = Op k :**: k
  type Cod (ExpFunctor k) = k
  type ExpFunctor k :% (y, z) = Exponential k y z

  ExpFunctor k
ExpFunctor % :: forall a b.
ExpFunctor k
-> Dom (ExpFunctor k) a b
-> Cod (ExpFunctor k) (ExpFunctor k :% a) (ExpFunctor k :% b)
% (Op k b1 a1
y :**: k a2 b2
z) = k a2 b2
z forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ k b1 a1
y


flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c))
flip :: forall {k} (k :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianClosed k =>
Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
     (Exponential k b (Exponential k a c))
flip Obj k a
a Obj k b
b Obj k c
c = forall {k} (k :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianClosed k =>
Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
     (Exponential k b (Exponential k a c))
flip Obj k a
a Obj k b
b Obj k c
c -- TODO


-- | Exponentials in @Hask@ are functions.
instance CartesianClosed (->) where
  type Exponential (->) y z = y -> z

  apply :: forall y z.
Obj (->) y
-> Obj (->) z -> BinaryProduct (->) (Exponential (->) y z) y -> z
apply Obj (->) y
_ Obj (->) z
_ (y -> z
f, y
y) = y -> z
f y
y
  tuple :: forall y z.
Obj (->) y
-> Obj (->) z -> z -> Exponential (->) y (BinaryProduct (->) z y)
tuple Obj (->) y
_ Obj (->) z
_ z
z      = (z
z,)
  z1 -> z2
f ^^^ :: forall z1 z2 y2 y1.
(z1 -> z2)
-> (y2 -> y1) -> Exponential (->) y1 z1 -> Exponential (->) y2 z2
^^^ y2 -> y1
h          = \Exponential (->) y1 z1
g -> z1 -> z2
f forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Exponential (->) y1 z1
g forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. y2 -> y1
h


instance CartesianClosed U.Unit where
  type Exponential U.Unit () () = ()
  apply :: forall y z.
Obj Unit y
-> Obj Unit z
-> Unit (BinaryProduct Unit (Exponential Unit y z) y) z
apply Unit y y
U.Unit Unit z z
U.Unit = Unit () ()
U.Unit
  tuple :: forall y z.
Obj Unit y
-> Obj Unit z
-> Unit z (Exponential Unit y (BinaryProduct Unit z y))
tuple Unit y y
U.Unit Unit z z
U.Unit = Unit () ()
U.Unit
  Unit z1 z2
U.Unit ^^^ :: forall z1 z2 y2 y1.
Unit z1 z2
-> Unit y2 y1
-> Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2)
^^^ Unit y2 y1
U.Unit = Unit () ()
U.Unit


-- | Exponentials in @Cat@ are the functor categories.
instance CartesianClosed Cat where
  type Exponential Cat c d = Nat c d

  apply :: forall (y :: * -> * -> *) (z :: * -> * -> *).
Obj Cat y
-> Obj Cat z -> Cat (BinaryProduct Cat (Exponential Cat y z) y) z
apply CatA{} CatA{} = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Apply c1 c2
Apply
  tuple :: forall (y :: * -> * -> *) (z :: * -> * -> *).
Obj Cat y
-> Obj Cat z -> Cat z (Exponential Cat y (BinaryProduct Cat z y))
tuple CatA{} CatA{} = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Tuple c1 c2
Tuple
  CatA ftag
f ^^^ :: forall (z1 :: * -> * -> *) (z2 :: * -> * -> *) (y2 :: * -> * -> *)
       (y1 :: * -> * -> *).
Cat z1 z2
-> Cat y2 y1 -> Cat (Exponential Cat y1 z1) (Exponential Cat y2 z2)
^^^ CatA ftag
h = forall k.
(Functor k, Category (Dom k), Category (Cod k)) =>
k -> Cat (Dom k) (Cod k)
CatA (forall f h. f -> h -> Wrap f h
Wrap ftag
f ftag
h)


type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite
  (   ProductFunctor (Presheaves k)
  :.: Tuple2 (Presheaves k) (Presheaves k) y
  :.: YonedaEmbedding k
  )
pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
pattern $bPshExponential :: forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
$mPshExponential :: forall {r} {k :: * -> * -> *} {y} {z}.
Category k =>
PShExponential k y z
-> (Obj (Presheaves k) y -> Obj (Presheaves k) z -> r)
-> ((# #) -> r)
-> r
PshExponential y z = Hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: YonedaEmbedding)

-- | The category of presheaves on a category @C@ is cartesian closed for any @C@.
instance Category k => CartesianClosed (Presheaves k) where
  type Exponential (Presheaves k) y z = PShExponential k y z

  apply :: forall y z.
Obj (Presheaves k) y
-> Obj (Presheaves k) z
-> Presheaves
     k
     (BinaryProduct (Presheaves k) (Exponential (Presheaves k) y z) y)
     z
apply yn :: Obj (Presheaves k) y
yn@(Nat y
y y
_ forall z. Obj (Op k) z -> Component y y z
_) zn :: Obj (Presheaves k) z
zn@(Nat z
z z
_ forall z. Obj (Op k) z -> Component z z z
_) = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential Obj (Presheaves k) y
yn Obj (Presheaves k) z
zn forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
y) z
z (\(Op k z z
i) (Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y)
  z
n, y :% z
yi) -> (Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y)
  z
n forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k z z
i) (k z z
i, y :% z
yi))
  tuple :: forall y z.
Obj (Presheaves k) y
-> Obj (Presheaves k) z
-> Presheaves
     k
     z
     (Exponential (Presheaves k) y (BinaryProduct (Presheaves k) z y))
tuple Obj (Presheaves k) y
yn zn :: Obj (Presheaves k) z
zn@(Nat z
z z
_ forall z. Obj (Op k) z -> Component z z z
_) = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat z
z (forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential Obj (Presheaves k) y
yn (Obj (Presheaves k) z
zn forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj (Presheaves k) y
yn)) (\(Op k z z
i) z :% z
zi -> forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X k z z
i) z
z (\Obj (Op k) z
_ k z z
j2i -> (z
z forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k z z
j2i) z :% z
zi) forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj (Presheaves k) y
yn)
  Presheaves k z1 z2
zn ^^^ :: forall z1 z2 y2 y1.
Presheaves k z1 z2
-> Presheaves k y2 y1
-> Presheaves
     k
     (Exponential (Presheaves k) y1 z1)
     (Exponential (Presheaves k) y2 z2)
^^^ Presheaves k y2 y1
yn = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Presheaves k y2 y1
yn) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Presheaves k z1 z2
zn)) (forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Presheaves k y2 y1
yn) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Presheaves k z1 z2
zn)) (\(Op k z z
i) Nat (Op k) (->) ((k :-*: z) :*: y1) z1
n -> Presheaves k z1 z2
zn forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Nat (Op k) (->) ((k :-*: z) :*: y1) z1
n forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X k z z
i) forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Presheaves k y2 y1
yn))



-- | The product functor is left adjoint the the exponential functor.
curryAdj :: CartesianClosed k
         => Obj k y
         -> Adjunction k k
              (ProductFunctor k :.: Tuple2 k k y)
              (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj :: forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits (forall (k :: * -> * -> *). ProductFunctor k
ProductFunctor forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c2 a -> Tuple2 c1 c2 a
Tuple2 Obj k y
y) (forall (k :: * -> * -> *). ExpFunctor k
ExpFunctor forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
Tuple1 (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj k y
y)) (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple Obj k y
y) (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply Obj k y
y)

-- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,
--   generalized to any cartesian closed category.
curry :: (CartesianClosed k, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
curry :: forall {k} (k :: k -> k -> *) (x :: k) (y :: k) (z :: k).
(CartesianClosed k, Kind k ~ *) =>
Obj k x
-> Obj k y
-> Obj k z
-> k (BinaryProduct k x y) z
-> k x (Exponential k y z)
curry Obj k x
x Obj k y
y Obj k z
_ = forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct (forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y) Obj k x
x

uncurry :: (CartesianClosed k, Kind k ~ Type) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z
uncurry :: forall {k} (k :: k -> k -> *) (x :: k) (y :: k) (z :: k).
(CartesianClosed k, Kind k ~ *) =>
Obj k x
-> Obj k y
-> Obj k z
-> k x (Exponential k y z)
-> k (BinaryProduct k x y) z
uncurry Obj k x
_ Obj k y
y Obj k z
z = forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct (forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y) Obj k z
z

-- | From every adjunction we get a monad, in this case the State monad.
type State k s a = Exponential k s (BinaryProduct k a s)

stateMonadReturn :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k a (State k s a)
stateMonadReturn :: forall {k} (k :: k -> k -> *) (s :: k) (a :: k).
(CartesianClosed k, Kind k ~ *) =>
Obj k s -> Obj k a -> k a (State k s a)
stateMonadReturn Obj k s
s Obj k a
a = forall f a. MonoidObject f a -> Cod f (Unit f) a
M.unit (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad (forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a

stateMonadJoin :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
stateMonadJoin :: forall {k} (k :: k -> k -> *) (s :: k) (a :: k).
(CartesianClosed k, Kind k ~ *) =>
Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
stateMonadJoin Obj k s
s Obj k a
a = forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
M.multiply (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad (forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a

-- ! From every adjunction we also get a comonad, the Context comonad in this case.
type Context k s a = BinaryProduct k (Exponential k s a) s

contextComonadExtract :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) a
contextComonadExtract :: forall {k} (k :: k -> k -> *) (s :: k) (a :: k).
(CartesianClosed k, Kind k ~ *) =>
Obj k s -> Obj k a -> k (Context k s a) a
contextComonadExtract Obj k s
s Obj k a
a = forall f a. ComonoidObject f a -> Cod f a (Unit f)
M.counit (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad (forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a

contextComonadDuplicate :: (CartesianClosed k, Kind k ~ Type) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
contextComonadDuplicate :: forall {k} (k :: k -> k -> *) (s :: k) (a :: k).
(CartesianClosed k, Kind k ~ *) =>
Obj k s
-> Obj k a -> k (Context k s a) (Context k s (Context k s a))
contextComonadDuplicate Obj k s
s Obj k a
a = forall f a. ComonoidObject f a -> Cod f a (f :% (a, a))
M.comultiply (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad (forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a