module Proarrow.Profunctor.Coproduct where

import Proarrow.Core (PRO, Profunctor(..), (:~>))

type (:+:) :: PRO j k -> PRO j k -> PRO 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 :: j) (a :: j) (b :: k) (d :: k).
(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 :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> (:+:) p q a b
InjL ((c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(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 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 :: PRO j k) (a :: j) (b :: k) (p :: PRO j k).
q a b -> (:+:) p q a b
InjR ((c ~> a) -> (b ~> d) -> q a b -> q c d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(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 c ~> a
l b ~> d
r q a b
q)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) 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 :: j) (b :: k) 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
r ((Ob a, Ob b) => r) -> q a b -> r
forall (a :: j) (b :: k) 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

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