module Proarrow.Category.Instance.Coproduct where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Representable (Representable (..))

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
  lrCase :: (forall b. (a ~ L b, Ob b) => r) -> (forall b. (a ~ R b, Ob b) => r) -> r
instance (Ob a) => IsLR (L a :: COPRODUCT j k) where
  lrCase :: forall r.
(forall (b :: j). (L a ~ L b, Ob b) => r)
-> (forall (b :: k). (L a ~ R b, Ob b) => r) -> r
lrCase forall (b :: j). (L a ~ L b, Ob b) => r
l forall (b :: k). (L a ~ R b, Ob b) => r
_ = r
forall (b :: j). (L a ~ L b, Ob b) => r
l
instance (Ob a) => IsLR (R a :: COPRODUCT j k) where
  lrCase :: forall r.
(forall (b :: j). (R a ~ L b, Ob b) => r)
-> (forall (b :: k). (R a ~ R b, Ob b) => r) -> r
lrCase forall (b :: j). (R a ~ L b, Ob b) => r
_ forall (b :: k). (R a ~ R b, Ob b) => r
r = r
forall (b :: k). (R a ~ R b, Ob b) => r
r

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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q a b
q

-- | The coproduct of two promonads.
instance (Promonad p, Promonad q) => Promonad (p :++: q) where
  id :: forall (a :: COPRODUCT j1 j2). Ob a => (:++:) p q a a
id @a = forall {j} {k} (a :: COPRODUCT j k) r.
IsLR a =>
(forall (b :: j). (a ~ L b, Ob b) => r)
-> (forall (b :: k). (a ~ R b, Ob b) => r) -> r
forall (a :: COPRODUCT j1 j2) r.
IsLR a =>
(forall (b :: j1). (a ~ L b, Ob b) => r)
-> (forall (b :: j2). (a ~ R b, Ob b) => r) -> r
lrCase @a (p b b -> (:++:) p q (L b) (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 b b
forall (a :: j1). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) (q b b -> (:++:) p q (R b) (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 b b
forall (a :: j2). Ob a => q a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  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 :: 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 :: 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)

-- | The coproduct of two categories.
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 (Representable p, Representable q) => Representable (p :++: q) where
  type (p :++: q) % L a = L (p % a)
  type (p :++: q) % R a = R (q % a)
  index :: forall (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2).
(:++:) p q a b -> a ~> ((p :++: q) % b)
index (InjL p a b
p) = (a ~> (p % b)) -> (:++:) (~>) (~>) (L a) (L (p % 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 -> a ~> (p % b)
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 a b
p)
  index (InjR q a b
q) = (a ~> (q % b)) -> (:++:) (~>) (~>) (R a) (R (q % 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 -> a ~> (q % b)
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 a b
q)
  repUniv :: forall (a :: COPRODUCT j1 j2).
Ob a =>
(:++:) p q ((p :++: q) % a) a
repUniv @a = forall {j} {k} (a :: COPRODUCT j k) r.
IsLR a =>
(forall (b :: j). (a ~ L b, Ob b) => r)
-> (forall (b :: k). (a ~ R b, Ob b) => r) -> r
forall (a :: COPRODUCT j1 j2) r.
IsLR a =>
(forall (b :: j1). (a ~ L b, Ob b) => r)
-> (forall (b :: j2). (a ~ R b, Ob b) => r) -> r
lrCase @a (p (p % b) b -> (:++:) p q (L (p % b)) (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 (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: j1 +-> k1) (a :: j1).
(Representable p, Ob a) =>
p (p % a) a
repUniv @p)) (q (q % b) b -> (:++:) p q (R (q % b)) (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 (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: j2 +-> k2) (a :: j2).
(Representable p, Ob a) =>
p (p % a) a
repUniv @q))

instance (Corepresentable p, Corepresentable q) => Corepresentable (p :++: q) where
  type (p :++: q) %% L a = L (p %% a)
  type (p :++: q) %% R a = R (q %% a)
  coindex :: forall (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2).
(:++:) p q a b -> ((p :++: q) %% a) ~> b
coindex (InjL p a b
f) = ((p %% a) ~> b) -> (:++:) (~>) (~>) (L (p %% 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 %% a) ~> b
forall (a :: k1) (b :: j1). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p a b
f)
  coindex (InjR q a b
f) = ((q %% a) ~> b) -> (:++:) (~>) (~>) (R (q %% 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 %% a) ~> b
forall (a :: k2) (b :: j2). q a b -> (q %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex q a b
f)
  corepUniv :: forall (a :: COPRODUCT k1 k2).
Ob a =>
(:++:) p q a ((p :++: q) %% a)
corepUniv @a = forall {j} {k} (a :: COPRODUCT j k) r.
IsLR a =>
(forall (b :: j). (a ~ L b, Ob b) => r)
-> (forall (b :: k). (a ~ R b, Ob b) => r) -> r
forall (a :: COPRODUCT k1 k2) r.
IsLR a =>
(forall (b :: k1). (a ~ L b, Ob b) => r)
-> (forall (b :: k2). (a ~ R b, Ob b) => r) -> r
lrCase @a (p b (p %% b) -> (:++:) p q (L b) (L (p %% 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 (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j1 +-> k1) (a :: k1).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv @p)) (q b (q %% b) -> (:++:) p q (R b) (R (q %% 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 (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j2 +-> k2) (a :: k2).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv @q))

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 k (p :: k +-> k) (a :: k) (b :: k).
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 k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger q a b
f)

data family Lft :: j +-> COPRODUCT j k
instance (CategoryOf j, CategoryOf k) => FunctorForRep (Lft :: j +-> COPRODUCT j k) where
  type Lft @ a = L a
  fmap :: forall (a :: j) (b :: j). (a ~> b) -> (Lft @ a) ~> (Lft @ b)
fmap = (a ~> b) -> (Lft @ a) ~> (Lft @ b)
(a ~> b) -> (:++:) (~>) (~>) (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

data family Rgt :: k +-> COPRODUCT j k
instance (CategoryOf j, CategoryOf k) => FunctorForRep (Rgt :: k +-> COPRODUCT j k) where
  type Rgt @ a = R a
  fmap :: forall (a :: k) (b :: k). (a ~> b) -> (Rgt @ a) ~> (Rgt @ b)
fmap = (a ~> b) -> (Rgt @ a) ~> (Rgt @ b)
(a ~> b) -> (:++:) (~>) (~>) (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

data family Codiag :: COPRODUCT k k +-> k
instance (CategoryOf k) => FunctorForRep (Codiag :: COPRODUCT k k +-> k) where
  type Codiag @ L a = a
  type Codiag @ R a = a
  fmap :: forall (a :: COPRODUCT k k) (b :: COPRODUCT k k).
(a ~> b) -> (Codiag @ a) ~> (Codiag @ b)
fmap = \case
    InjL a ~> b
f -> a ~> b
(Codiag @ a) ~> (Codiag @ b)
f
    InjR a ~> b
g -> a ~> b
(Codiag @ a) ~> (Codiag @ b)
g