{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.Product where

import Prelude (type (~))

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Category.Enriched.ThinCategory (ThinProfunctor (..))
import Proarrow.Profunctor.Representable (Representable (..))

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 (:**:) :: j1 +-> k1 -> j2 +-> k2 -> (j1, j2) +-> (k1, k2)
data (c :**: d) a b where
  (:**:) :: { forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
(:**:) c d '(a1, a2) '(b1, b2) -> c a1 b1
fstK :: c a1 b1, forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
(:**:) c d '(a1, a2) '(b1, b2) -> d a2 b2
sndK :: d a2 b2 } -> (c :**: d) '(a1, a2) '(b1, b2)

-- | The product of two categories.
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 :: (j1, j2)). Ob a => (:**:) p q a a
id = p (Fst a) (Fst a)
forall (a :: j1). Ob a => p a a
forall {k} (p :: 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 {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q (Snd a) (Snd a)
forall (a :: j2). Ob a => q a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  (p a1 b1
f1 :**: q a2 b2
f2) . :: forall (b :: (j1, j2)) (c :: (j1, j2)) (a :: (j1, j2)).
(:**:) 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 :: j1) (c :: j1) (a :: j1). p b c -> p a b -> p a c
forall {k} (p :: 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 {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
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 :: j2) (c :: j2) (a :: j2). q b c -> q a b -> q a c
forall {k} (p :: 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 :: (j1, j2))
       (d :: (j1, j2)).
(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 :: j1) (d :: j1).
(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 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 {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
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 :: j2) (d :: j2).
(c ~> a) -> (b ~> d) -> q a b -> q 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 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 :: (j1, j2)) 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 :: j1) 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 a1 b1
f ((Ob a2, Ob b2) => r) -> q a2 b2 -> r
forall (a :: k2) (b :: j2) r. ((Ob a, Ob b) => r) -> q 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
\\ q a2 b2
g

instance (DaggerProfunctor p, DaggerProfunctor q) => DaggerProfunctor (p :**: q) where
  dagger :: forall (a :: (j1, j2)) (b :: (j1, j2)).
(:**:) p q a b -> (:**:) p q b a
dagger (p a1 b1
f :**: q a2 b2
g) = p a1 b1 -> p b1 a1
forall (a :: j1) (b :: j1). p a b -> p b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger p a1 b1
f p b1 a1 -> q b2 a2 -> (:**:) p q '(b1, b2) '(a1, a2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q a2 b2 -> q b2 a2
forall (a :: j2) (b :: j2). q a b -> q b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger q a2 b2
g

instance (ThinProfunctor p, ThinProfunctor q) => ThinProfunctor (p :**: q) where
  type HasArrow (p :**: q) '(a1, a2) '(b1, b2) = (HasArrow p a1 b1, HasArrow q a2 b2)
  arr :: forall (a :: (k1, k2)) (b :: (j1, j2)).
(Ob a, Ob b, HasArrow (p :**: q) a b) =>
(:**:) p q a b
arr = p (Fst a) (Fst b)
forall (a :: k1) (b :: j1). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr p (Fst a) (Fst b)
-> q (Snd a) (Snd b) -> (:**:) p q '(Fst a, Snd a) '(Fst b, Snd b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q (Snd a) (Snd b)
forall (a :: k2) (b :: j2). (Ob a, Ob b, HasArrow q a b) => q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
  withArr :: forall (a :: (k1, k2)) (b :: (j1, j2)) r.
(:**:) p q a b -> (HasArrow (p :**: q) a b => r) -> r
withArr (p a1 b1
f :**: q a2 b2
g) HasArrow (p :**: q) a b => r
r = p a1 b1 -> (HasArrow p a1 b1 => r) -> r
forall (a :: k1) (b :: j1) r. p a b -> (HasArrow p a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr p a1 b1
f (q a2 b2 -> (HasArrow q a2 b2 => r) -> r
forall (a :: k2) (b :: j2) r. q a b -> (HasArrow q a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr q a2 b2
g r
HasArrow q a2 b2 => r
HasArrow (p :**: q) a b => r
r)

instance (Representable p, Representable q) => Representable (p :**: q) where
  type (p :**: q) % '(a, b) = '(p % a, q % b)
  index :: forall (a :: (k1, k2)) (b :: (j1, j2)).
(:**:) 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 :: j1). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
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 {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q a2 b2 -> a2 ~> (q % b2)
forall (a :: k2) (b :: j2). q a b -> a ~> (q % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index q a2 b2
q
  tabulate :: forall (b :: (j1, j2)) (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 :: j1) (a :: k1). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(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 {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> (q % Snd b)) -> q a2 (Snd b)
forall (b :: j2) (a :: k2). Ob b => (a ~> (q % b)) -> q a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a2 ~> b2
a2 ~> (q % Snd b)
g
  repMap :: forall (a :: (j1, j2)) (b :: (j1, j2)).
(a ~> b) -> ((p :**: q) % a) ~> ((p :**: q) % b)
repMap (a1 ~> b1
f :**: a2 ~> b2
g) = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j1 +-> k1) (a :: j1) (b :: j1).
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 {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j2 +-> k2) (a :: j2) (b :: j2).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @q a2 ~> b2
g