{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Cartesian monoidal categories ('Cartesian': tensor = product, with 'CopyDiscard' as
-- superclass by Fox's theorem) and cartesian closed ones ('CCC', 'BiCCC'). Lives above
-- "Proarrow.Category.Monoidal.CopyDiscard" rather than with the products, because the superclass
-- points that way.
module Proarrow.Category.Monoidal.Cartesian where

import Prelude (type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal)
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Colimit.BinaryCoproduct (HasCoproducts)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts, PROD (..), Prod (..), diag)
import Proarrow.Limit.Terminal (HasTerminalObject (..), Semicartesian)
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..))
import Proarrow.Profunctor.Representable (RepCostar (..), Representable (..), withObRep)

class (a ** b ~ a && b) => TensorIsProduct a b
instance (a ** b ~ a && b) => TensorIsProduct a b

-- | A cartesian monoidal category: the tensor is the product and the unit the terminal object.
-- By Fox's theorem this is exactly a 'CopyDiscard' category whose 'copy' and 'discard' are
-- natural, so 'CopyDiscard' is a superclass: every cartesian category supplies its diagonals as
-- comonoids, and anything asking only for copying and discarding (prisms, for instance) accepts
-- a cartesian category directly. The law relating the two is @copy = id &&& id@ and
-- @discard = terminate@.
class
  (HasProducts k, SymMonoidal k, Semicartesian k, CopyDiscard k, forall (a :: k) (b :: k). TensorIsProduct a b) =>
  Cartesian k

instance
  (HasProducts k, SymMonoidal k, Semicartesian k, CopyDiscard k, forall (a :: k) (b :: k). TensorIsProduct a b)
  => Cartesian k

-- | In a category with products every object is a comonoid via the diagonal and the terminal
-- map -- the natural comonoid structure that makes 'PROD' 'CopyDiscard' and 'Cartesian'.
instance (HasProducts k, Ob a) => Comonoid (PR (a :: k)) where
  counit :: 'PR a ~> Unit
counit = (a ~> TerminalObject) -> Prod (~>) ('PR a) ('PR TerminalObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  comult :: 'PR a ~> ('PR a ** 'PR a)
comult = (a ~> (a && a)) -> Prod (~>) ('PR a) ('PR (a && a))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag

instance (HasProducts k, Ob a) => CocommutativeComonoid (PR (a :: k))

-- | A category with products, viewed through 'PROD' as a monoidal category, is cartesian.
instance (HasProducts k) => CopyDiscard (PROD k)

-- | In a cartesian category the tensor /is/ the product ('TensorIsProduct'), but GHC only applies
-- that equation at the top of a type, never under another type family such as @('||')@, and
-- using the quantified form of it directly sends the solver in circles. These two identities take
-- the equation as an ordinary given -- discharged at the call site from the quantified superclass
-- of 'Cartesian' -- and let it be applied exactly where a product-typed leg meets tensor-typed
-- plumbing.
tensorToProduct :: forall {k} (a :: k) b. (HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) => (a ** b) ~> (a && b)
tensorToProduct :: forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a ** b) ~> (a && b)
tensorToProduct = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b (a && b) ~> (a && b)
Ob (a && b) => (a && b) ~> (a && b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

productToTensor :: forall {k} (a :: k) b. (HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) => (a && b) ~> (a ** b)
productToTensor :: forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
productToTensor = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b (a && b) ~> (a && b)
Ob (a && b) => (a && b) ~> (a && b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | Every functor between cartesian categories is oplax monoidal, @f (a && b) ~> f a && f b@ by the
-- projections and @f Unit ~> Unit@ by terminality. On the 'RepCostar' of its representable profunctor
-- this is 'Proarrow.Category.Monoidal.OplaxMonoidal'.
instance (Representable p, Cartesian j, Cartesian k) => MonoidalProfunctor (RepCostar (p :: j +-> k)) where
  one :: RepCostar p Unit Unit
one = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @Unit (((p % TerminalObject) ~> TerminalObject)
-> RepCostar p TerminalObject TerminalObject
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (p % TerminalObject) ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)
  RepCostar @a (p % x1) ~> x2
f ** :: forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
RepCostar p x1 x2
-> RepCostar p y1 y2 -> RepCostar p (x1 ** y1) (x2 ** y2)
** RepCostar @b (p % y1) ~> y2
g = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @j @a @b (((p % (x1 ** y1)) ~> (x2 ** y2))
-> RepCostar p (x1 ** y1) (x2 ** y2)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j) (a' :: k)
       (b' :: k).
(Representable p, Cartesian k, Cartesian j, TensorIsProduct a b,
 TensorIsProduct a' b', Ob a, Ob b) =>
((p % a) ~> a') -> ((p % b) ~> b') -> (p % (a ** b)) ~> (a' ** b')
forall (p :: j +-> k) (a :: j) (b :: j) (a' :: k) (b' :: k).
(Representable p, Cartesian k, Cartesian j, TensorIsProduct a b,
 TensorIsProduct a' b', Ob a, Ob b) =>
((p % a) ~> a') -> ((p % b) ~> b') -> (p % (a ** b)) ~> (a' ** b')
unparRepCartesian @p @a @b (p % x1) ~> x2
f (p % y1) ~> y2
g))

unparRepCartesian
  :: forall {j} {k} p (a :: j) b a' b'
   . ( Representable (p :: j +-> k)
     , Cartesian k
     , Cartesian j
     , TensorIsProduct a b
     , TensorIsProduct a' b'
     , Ob a
     , Ob b
     )
  => (p % a ~> a') -> (p % b ~> b') -> p % (a ** b) ~> (a' ** b')
unparRepCartesian :: forall {j} {k} (p :: j +-> k) (a :: j) (b :: j) (a' :: k)
       (b' :: k).
(Representable p, Cartesian k, Cartesian j, TensorIsProduct a b,
 TensorIsProduct a' b', Ob a, Ob b) =>
((p % a) ~> a') -> ((p % b) ~> b') -> (p % (a ** b)) ~> (a' ** b')
unparRepCartesian (p % a) ~> a'
f (p % b) ~> b'
g = (p % a) ~> a'
f ((p % a) ~> a')
-> ((p % (a && b)) ~> (p % a)) -> (p % (a && b)) ~> a'
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @j @a @b) ((p % (a && b)) ~> a')
-> ((p % (a && b)) ~> b') -> (p % (a && b)) ~> (a' && b')
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& (p % b) ~> b'
g ((p % b) ~> b')
-> ((p % (a && b)) ~> (p % b)) -> (p % (a && b)) ~> b'
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @j @a @b)

class (Cartesian k, Closed k) => CCC k
instance (Cartesian k, Closed k) => CCC k

class (CCC k, HasCoproducts k) => BiCCC k
instance (CCC k, HasCoproducts k) => BiCCC k

ap
  :: forall {j} {k} y a x p
   . (Closed j, Cartesian k, MonoidalProfunctor (p :: j +-> k), Ob y)
  => p a (x ~~> y)
  -> p a x
  -> p a y
ap :: forall {j} {k} (y :: j) (a :: k) (x :: j) (p :: j +-> k).
(Closed j, Cartesian k, MonoidalProfunctor p, Ob y) =>
p a (x ~~> y) -> p a x -> p a y
ap p a (x ~~> y)
pf p a x
px = (a ~> (a && a))
-> (((x ~~> y) ** x) ~> y) -> p (a && a) ((x ~~> y) ** x) -> p a y
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @j @x @y) (p a (x ~~> y)
pf p a (x ~~> y) -> p a x -> p (a ** a) ((x ~~> y) ** x)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** p a x
px) ((Ob a, Ob x) => p a y) -> p a x -> p a y
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a x
px