module Proarrow.Category.Instance.Coproduct where

import Data.Kind (Constraint)

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

type data COPRODUCT j k = L j | R k

type (:++:) :: (j1 +-> k1) -> (j2 +-> k2) -> COPRODUCT j1 j2 +-> COPRODUCT k1 k2
data (:++:) p q a b where
  InjL :: p a b -> (p :++: q) (L a) (L b)
  InjR :: q a b -> (p :++: q) (R a) (R b)

type IsLR :: forall {j} {k}. COPRODUCT j k -> Constraint
class IsLR (a :: COPRODUCT j k) where
  lrId :: (Promonad p, Promonad q) => (p :++: q) a a
instance (Ob a) => IsLR (L a :: COPRODUCT j k) where
  lrId :: forall (p :: PRO j j) (q :: PRO k k).
(Promonad p, Promonad q) =>
(:++:) p q (L a) (L a)
lrId = p a a -> (:++:) p q (L a) (L a)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a :: k1) (b :: j1)
       (q :: j2 +-> k2).
p a b -> (:++:) p q (L a) (L b)
InjL p a a
forall (a :: j). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (Ob a) => IsLR (R a :: COPRODUCT j k) where
  lrId :: forall (p :: PRO j j) (q :: PRO k k).
(Promonad p, Promonad q) =>
(:++:) p q (R a) (R a)
lrId = q a a -> (:++:) p q (R a) (R a)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a :: k2) (b :: j2)
       (p :: j1 +-> k1).
q a b -> (:++:) p q (R a) (R b)
InjR q a a
forall (a :: k). Ob a => q a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (Profunctor p, Profunctor q) => Profunctor (p :++: q) where
  dimap :: forall (c :: COPRODUCT k1 k2) (a :: COPRODUCT k1 k2)
       (b :: COPRODUCT j1 j2) (d :: COPRODUCT j1 j2).
(c ~> a) -> (b ~> d) -> (:++:) p q a b -> (:++:) p q c d
dimap (InjL a ~> b
f) (InjL a ~> b
g) (InjL p a b
p) = p a b -> (:++:) p q (L a) (L b)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a :: k1) (b :: j1)
       (q :: j2 +-> k2).
p a b -> (:++:) p q (L a) (L b)
InjL ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k1) (a :: k1) (b :: j1) (d :: j1).
(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 a ~> b
a ~> a
f a ~> b
b ~> b
g p a b
p)
  dimap (InjR a ~> b
f) (InjR a ~> b
g) (InjR q a b
q) = q a b -> (:++:) p q (R a) (R b)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a :: k2) (b :: j2)
       (p :: j1 +-> k1).
q a b -> (:++:) p q (R a) (R b)
InjR ((a ~> a) -> (b ~> b) -> q a b -> q a b
forall (c :: k2) (a :: k2) (b :: j2) (d :: j2).
(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 a ~> b
a ~> a
f a ~> b
b ~> b
g q a b
q)
  dimap InjL{} InjR{} (:++:) p q a b
p = case (:++:) p q a b
p of
  dimap InjR{} InjL{} (:++:) p q a b
q = case (:++:) p q a b
q of
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) r.
((Ob a, Ob b) => r) -> (:++:) p q a b -> r
\\ InjL p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k1) (b :: j1) 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 a b
p
  (Ob a, Ob b) => r
r \\ InjR q a b
q = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> q a b -> r
forall (a :: k2) (b :: j2) 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 a b
q
instance (Promonad p, Promonad q) => Promonad (p :++: q) where
  id :: forall (a :: COPRODUCT j1 j2). Ob a => (:++:) p q a a
id = (:++:) p q a a
forall {j} {k} (a :: COPRODUCT j k) (p :: PRO j j) (q :: PRO k k).
(IsLR a, Promonad p, Promonad q) =>
(:++:) p q a a
forall (p :: PRO j1 j1) (q :: PRO j2 j2).
(Promonad p, Promonad q) =>
(:++:) p q a a
lrId
  InjL p a b
p . :: forall (b :: COPRODUCT j1 j2) (c :: COPRODUCT j1 j2)
       (a :: COPRODUCT j1 j2).
(:++:) p q b c -> (:++:) p q a b -> (:++:) p q a c
. InjL p a b
q = p a b -> (:++:) p q (L a) (L b)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a :: k1) (b :: j1)
       (q :: j2 +-> k2).
p a b -> (:++:) p q (L a) (L b)
InjL (p a b
p p a b -> p a a -> p a b
forall (b :: j1) (c :: j1) (a :: j1). 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 a a
p a b
q)
  InjR q a b
q . InjR q a b
r = q a b -> (:++:) p q (R a) (R b)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a :: k2) (b :: j2)
       (p :: j1 +-> k1).
q a b -> (:++:) p q (R a) (R b)
InjR (q a b
q q a b -> q a a -> q a b
forall (b :: j2) (c :: j2) (a :: j2). 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 a a
q a b
r)
instance (CategoryOf j, CategoryOf k) => CategoryOf (COPRODUCT j k) where
  type (~>) @(COPRODUCT j k) = (~>) @j :++: (~>) @k
  type Ob (a :: COPRODUCT j k) = IsLR a

instance (DaggerProfunctor p, DaggerProfunctor q) => DaggerProfunctor (p :++: q) where
  dagger :: forall (a :: COPRODUCT j1 j2) (b :: COPRODUCT j1 j2).
(:++:) p q a b -> (:++:) p q b a
dagger = \case
    InjL p a b
f -> p b a -> (:++:) p q (L b) (L a)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a :: k1) (b :: j1)
       (q :: j2 +-> k2).
p a b -> (:++:) p q (L a) (L b)
InjL (p a b -> p b a
forall (a :: j1) (b :: j1). p a b -> p b a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger p a b
f)
    InjR q a b
f -> q b a -> (:++:) p q (R b) (R a)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a :: k2) (b :: j2)
       (p :: j1 +-> k1).
q a b -> (:++:) p q (R a) (R b)
InjR (q a b -> q b a
forall (a :: j2) (b :: j2). q a b -> q b a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger q a b
f)