module Proarrow.Profunctor.Coproduct where

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Core (Profunctor (..), type (+->))
import Proarrow.Category.Monoidal.Action (Strong (..))

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 x y -> r) -> (q x y -> r) -> (p :+: q) x y -> r
coproduct :: forall {k} {j} (p :: k -> j -> Type) (x :: k) (y :: j) r
       (q :: k -> j -> Type).
(p x y -> r) -> (q x y -> r) -> (:+:) p q x y -> r
coproduct p x y -> r
l q x y -> r
_ (InjL p x y
p) = p x y -> r
l p x y
p
coproduct p x y -> r
_ q x y -> r
r (InjR q x y
q) = q x y -> r
r q x y
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)

instance (Strong m p, Strong m q) => Strong m (p :+: q) where
  act :: forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> (:+:) p q x y -> (:+:) p q (Act a x) (Act b y)
act a ~> b
f (InjL p x y
p) = p (Act a x) (Act b y) -> (:+:) p q (Act a x) (Act b y)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL ((a ~> b) -> p x y -> p (Act a x) (Act b y)
forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f p x y
p)
  act a ~> b
f (InjR q x y
q) = q (Act a x) (Act b y) -> (:+:) p q (Act a x) (Act b y)
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR ((a ~> b) -> q x y -> q (Act a x) (Act b y)
forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> q x y -> q (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f q x y
q)