{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Instance.Product where

import Proarrow.Core (CAT, CategoryOf(..), Promonad(..), Profunctor(..))
import Proarrow.Profunctor.Representable (Representable(..))
import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal, swap')

type Fst :: (a, b) -> a
type family Fst a where Fst '(a, b) = a
type Snd :: (a, b) -> b
type family Snd a where Snd '(a, b) = b

type (:**:) :: CAT k1 -> CAT k2 -> CAT (k1, k2)
data (c :**: d) a b where
  (:**:) :: c a1 b1 -> d a2 b2 -> (c :**: d) '(a1, a2) '(b1, b2)

instance (CategoryOf k1, CategoryOf k2) => CategoryOf (k1, k2) where
  type (~>) = (~>) :**: (~>)
  type Ob a = (a ~ '(Fst a, Snd a), Ob (Fst a), Ob (Snd a))


-- | The product promonad of promonads `p` and `q`.
instance (Promonad p, Promonad q) => Promonad (p :**: q) where
  id :: forall (a :: (k1, k2)). Ob a => (:**:) p q a a
id = p (Fst a) (Fst a)
forall (a :: k1). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id p (Fst a) (Fst a)
-> q (Snd a) (Snd a) -> (:**:) p q '(Fst a, Snd a) '(Fst a, Snd a)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q (Snd a) (Snd a)
forall (a :: k2). Ob a => q a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  (p a1 b1
f1 :**: q a2 b2
f2) . :: forall (b :: (k1, k2)) (c :: (k1, k2)) (a :: (k1, k2)).
(:**:) p q b c -> (:**:) p q a b -> (:**:) p q a c
. (p a1 b1
g1 :**: q a2 b2
g2) = (p a1 b1
f1 p a1 b1 -> p a1 a1 -> p a1 b1
forall (b :: k1) (c :: k1) (a :: k1). p b c -> p a b -> p a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a1 a1
p a1 b1
g1) p a1 b1 -> q a2 b2 -> (:**:) p q '(a1, a2) '(b1, b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (q a2 b2
f2 q a2 b2 -> q a2 a2 -> q a2 b2
forall (b :: k2) (c :: k2) (a :: k2). q b c -> q a b -> q a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. q a2 a2
q a2 b2
g2)

instance (Profunctor p, Profunctor q) => Profunctor (p :**: q) where
  dimap :: forall (c :: (k1, k2)) (a :: (k1, k2)) (b :: (k1, k2))
       (d :: (k1, k2)).
(c ~> a) -> (b ~> d) -> (:**:) p q a b -> (:**:) p q c d
dimap (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) (p a1 b1
f1 :**: q a2 b2
f2) = (a1 ~> a1) -> (b1 ~> b1) -> p a1 b1 -> p a1 b1
forall (c :: k1) (a :: k1) (b :: k1) (d :: k1).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a1 ~> b1
a1 ~> a1
l1 a1 ~> b1
b1 ~> b1
r1 p a1 b1
f1 p a1 b1 -> q a2 b2 -> (:**:) p q '(a1, a2) '(b1, b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> a2) -> (b2 ~> b2) -> q a2 b2 -> q a2 b2
forall (c :: k2) (a :: k2) (b :: k2) (d :: k2).
(c ~> a) -> (b ~> d) -> q a b -> q c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a2 ~> b2
a2 ~> a2
l2 a2 ~> b2
b2 ~> b2
r2 q a2 b2
f2
  (Ob a, Ob b) => r
r \\ :: forall (a :: (k1, k2)) (b :: (k1, k2)) r.
((Ob a, Ob b) => r) -> (:**:) p q a b -> r
\\ (p a1 b1
f :**: q a2 b2
g) = r
(Ob a1, Ob b1) => r
(Ob a, Ob b) => r
r ((Ob a1, Ob b1) => r) -> p a1 b1 -> r
forall (a :: k1) (b :: k1) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a1 b1
f ((Ob a2, Ob b2) => r) -> q a2 b2 -> r
forall (a :: k2) (b :: k2) r. ((Ob a, Ob b) => r) -> q a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q a2 b2
g

instance (Representable p, Representable q) => Representable (p :**: q) where
  type (p :**: q) % '(a, b) = '(p % a, q % b)
  index :: forall (a :: (k1, k2)) (b :: (k1, k2)).
(:**:) p q a b -> a ~> ((p :**: q) % b)
index (p a1 b1
p :**: q a2 b2
q) = p a1 b1 -> a1 ~> (p % b1)
forall (a :: k1) (b :: k1). p a b -> a ~> (p % b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index p a1 b1
p (a1 ~> (p % b1))
-> (a2 ~> (q % b2)) -> (:**:) (~>) (~>) '(a1, a2) '(p % b1, q % b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q a2 b2 -> a2 ~> (q % b2)
forall (a :: k2) (b :: k2). q a b -> a ~> (q % b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index q a2 b2
q
  tabulate :: forall (b :: (k1, k2)) (a :: (k1, k2)).
Ob b =>
(a ~> ((p :**: q) % b)) -> (:**:) p q a b
tabulate (a1 ~> b1
f :**: a2 ~> b2
g) = (a1 ~> (p % Fst b)) -> p a1 (Fst b)
forall (b :: k1) (a :: k1). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a1 ~> b1
a1 ~> (p % Fst b)
f p a1 (Fst b)
-> q a2 (Snd b) -> (:**:) p q '(a1, a2) '(Fst b, Snd b)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> (q % Snd b)) -> q a2 (Snd b)
forall (b :: k2) (a :: k2). Ob b => (a ~> (q % b)) -> q a b
forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a2 ~> b2
a2 ~> (q % Snd b)
g
  repMap :: forall (a :: (k1, k2)) (b :: (k1, k2)).
(a ~> b) -> ((p :**: q) % a) ~> ((p :**: q) % b)
repMap (a1 ~> b1
f :**: a2 ~> b2
g) = forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO k1 k1) (a :: k1) (b :: k1).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a1 ~> b1
f ((p % a1) ~> (p % b1))
-> ((q % a2) ~> (q % b2))
-> (:**:) (~>) (~>) '(p % a1, q % a2) '(p % b1, q % b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO k2 k2) (a :: k2) (b :: k2).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @q a2 ~> b2
g


instance (Monoidal j, Monoidal k) => Monoidal (j, k) where
  type Unit = '(Unit, Unit)
  type '(a1, a2) ** '(b1, b2) = '(a1 ** b1, a2 ** b2)
  (a1 ~> b1
f1 :**: a2 ~> b2
f2) par :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)) (d :: (j, k)).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (a1 ~> b1
g1 :**: a2 ~> b2
g2) = (a1 ~> b1
f1 (a1 ~> b1) -> (a1 ~> b1) -> (a1 ** a1) ~> (b1 ** b1)
forall (a :: j) (b :: j) (c :: j) (d :: j).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` a1 ~> b1
g1) ((a1 ** a1) ~> (b1 ** b1))
-> ((a2 ** a2) ~> (b2 ** b2))
-> (:**:) (~>) (~>) '(a1 ** a1, a2 ** a2) '(b1 ** b1, b2 ** b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2
f2 (a2 ~> b2) -> (a2 ~> b2) -> (a2 ** a2) ~> (b2 ** b2)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` a2 ~> b2
g2)
  leftUnitor :: forall (a :: (j, k)). Obj a -> (Unit ** a) ~> a
leftUnitor (a1 ~> b1
a1 :**: a2 ~> b2
a2) = Obj b1 -> (Unit ** b1) ~> b1
forall (a :: j). Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor a1 ~> b1
Obj b1
a1 ((Unit ** b1) ~> b1)
-> ((Unit ** b2) ~> b2)
-> (:**:) (~>) (~>) '(Unit ** b1, Unit ** b2) '(b1, b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2 -> (Unit ** b2) ~> b2
forall (a :: k). Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor a2 ~> b2
Obj b2
a2
  leftUnitorInv :: forall (a :: (j, k)). Obj a -> a ~> (Unit ** a)
leftUnitorInv (a1 ~> b1
a1 :**: a2 ~> b2
a2) = Obj b1 -> b1 ~> (Unit ** b1)
forall (a :: j). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv a1 ~> b1
Obj b1
a1 (b1 ~> (Unit ** b1))
-> (b2 ~> (Unit ** b2))
-> (:**:) (~>) (~>) '(b1, b2) '(Unit ** b1, Unit ** b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2 -> b2 ~> (Unit ** b2)
forall (a :: k). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv a2 ~> b2
Obj b2
a2
  rightUnitor :: forall (a :: (j, k)). Obj a -> (a ** Unit) ~> a
rightUnitor (a1 ~> b1
a1 :**: a2 ~> b2
a2) = Obj b1 -> (b1 ** Unit) ~> b1
forall (a :: j). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
rightUnitor a1 ~> b1
Obj b1
a1 ((b1 ** Unit) ~> b1)
-> ((b2 ** Unit) ~> b2)
-> (:**:) (~>) (~>) '(b1 ** Unit, b2 ** Unit) '(b1, b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2 -> (b2 ** Unit) ~> b2
forall (a :: k). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
rightUnitor a2 ~> b2
Obj b2
a2
  rightUnitorInv :: forall (a :: (j, k)). Obj a -> a ~> (a ** Unit)
rightUnitorInv (a1 ~> b1
a1 :**: a2 ~> b2
a2) = Obj b1 -> b1 ~> (b1 ** Unit)
forall (a :: j). Obj a -> a ~> (a ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
rightUnitorInv a1 ~> b1
Obj b1
a1 (b1 ~> (b1 ** Unit))
-> (b2 ~> (b2 ** Unit))
-> (:**:) (~>) (~>) '(b1, b2) '(b1 ** Unit, b2 ** Unit)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2 -> b2 ~> (b2 ** Unit)
forall (a :: k). Obj a -> a ~> (a ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
rightUnitorInv a2 ~> b2
Obj b2
a2
  associator :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator (a1 ~> b1
a1 :**: a2 ~> b2
a2) (a1 ~> b1
b1 :**: a2 ~> b2
b2) (a1 ~> b1
c1 :**: a2 ~> b2
c2) = Obj b1
-> Obj b1 -> Obj b1 -> ((b1 ** b1) ** b1) ~> (b1 ** (b1 ** b1))
forall (a :: j) (b :: j) (c :: j).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator a1 ~> b1
Obj b1
a1 a1 ~> b1
Obj b1
b1 a1 ~> b1
Obj b1
c1 (((b1 ** b1) ** b1) ~> (b1 ** (b1 ** b1)))
-> (((b2 ** b2) ** b2) ~> (b2 ** (b2 ** b2)))
-> (:**:)
     (~>)
     (~>)
     '((b1 ** b1) ** b1, (b2 ** b2) ** b2)
     '(b1 ** (b1 ** b1), b2 ** (b2 ** b2))
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2
-> Obj b2 -> Obj b2 -> ((b2 ** b2) ** b2) ~> (b2 ** (b2 ** b2))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator a2 ~> b2
Obj b2
a2 a2 ~> b2
Obj b2
b2 a2 ~> b2
Obj b2
c2
  associatorInv :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv (a1 ~> b1
a1 :**: a2 ~> b2
a2) (a1 ~> b1
b1 :**: a2 ~> b2
b2) (a1 ~> b1
c1 :**: a2 ~> b2
c2) = Obj b1
-> Obj b1 -> Obj b1 -> (b1 ** (b1 ** b1)) ~> ((b1 ** b1) ** b1)
forall (a :: j) (b :: j) (c :: j).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv a1 ~> b1
Obj b1
a1 a1 ~> b1
Obj b1
b1 a1 ~> b1
Obj b1
c1 ((b1 ** (b1 ** b1)) ~> ((b1 ** b1) ** b1))
-> ((b2 ** (b2 ** b2)) ~> ((b2 ** b2) ** b2))
-> (:**:)
     (~>)
     (~>)
     '(b1 ** (b1 ** b1), b2 ** (b2 ** b2))
     '((b1 ** b1) ** b1, (b2 ** b2) ** b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2
-> Obj b2 -> Obj b2 -> (b2 ** (b2 ** b2)) ~> ((b2 ** b2) ** b2)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv a2 ~> b2
Obj b2
a2 a2 ~> b2
Obj b2
b2 a2 ~> b2
Obj b2
c2

instance (SymMonoidal j, SymMonoidal k) => SymMonoidal (j, k) where
  swap' :: forall (a :: (j, k)) (b :: (j, k)).
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' (a1 ~> b1
a1 :**: a2 ~> b2
a2) (a1 ~> b1
b1 :**: a2 ~> b2
b2) = Obj b1 -> Obj b1 -> (b1 ** b1) ~> (b1 ** b1)
forall (a :: j) (b :: j). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' a1 ~> b1
Obj b1
a1 a1 ~> b1
Obj b1
b1 ((b1 ** b1) ~> (b1 ** b1))
-> ((b2 ** b2) ~> (b2 ** b2))
-> (:**:) (~>) (~>) '(b1 ** b1, b2 ** b2) '(b1 ** b1, b2 ** b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2 -> Obj b2 -> (b2 ** b2) ~> (b2 ** b2)
forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' a2 ~> b2
Obj b2
a2 a2 ~> b2
Obj b2
b2