module Proarrow.Profunctor.Coproduct where

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Core (Profunctor (..), (:~>), type (+->))

type (:+:) :: (j +-> k) -> (j +-> k) -> (j +-> k)
data (p :+: q) a b where
  InjL :: p a b -> (p :+: q) a b
  InjR :: q a b -> (p :+: q) a b

instance (Profunctor p, Profunctor q) => Profunctor (p :+: q) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> (:+:) p q a b -> (:+:) p q c d
dimap c ~> a
l b ~> d
r (InjL p a b
p) = p c d -> (:+:) p q c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL ((c ~> a) -> (b ~> d) -> p a b -> p c d
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 c ~> a
l b ~> d
r p a b
p)
  dimap c ~> a
l b ~> d
r (InjR q a b
q) = q c d -> (:+:) p q c d
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR ((c ~> a) -> (b ~> d) -> q a b -> q c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(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 c ~> a
l b ~> d
r q a b
q)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> (:+:) p q a b -> r
\\ InjL p a b
p = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
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 b
p
  (Ob a, Ob b) => r
r \\ InjR q a b
q = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> q a b -> r
forall (a :: k) (b :: j) 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

coproduct :: (p :~> r) -> (q :~> r) -> p :+: q :~> r
coproduct :: forall {k} {k1} (p :: k -> k1 -> Type) (r :: k -> k1 -> Type)
       (q :: k -> k1 -> Type).
(p :~> r) -> (q :~> r) -> (p :+: q) :~> r
coproduct p :~> r
l q :~> r
_ (InjL p a b
p) = p a b -> r a b
p :~> r
l p a b
p
coproduct p :~> r
_ q :~> r
r (InjR q a b
q) = q a b -> r a b
q :~> r
r q a b
q

instance (DaggerProfunctor p, DaggerProfunctor q) => DaggerProfunctor (p :+: q) where
  dagger :: forall (a :: k) (b :: k). (:+:) p q a b -> (:+:) p q b a
dagger (InjL p a b
p) = p b a -> (:+:) p q b a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL (p a b -> p b a
forall (a :: k) (b :: k). 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
p)
  dagger (InjR q a b
q) = q b a -> (:+:) p q b a
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR (q a b -> q b a
forall (a :: k) (b :: k). 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
q)