-- | Profunctor composition ':.:', the coend @exists b. (p a b, q b c)@ with the coend hidden in the
-- existential of the constructor. This is the horizontal composition of profunctors; 'Promonad's are the
-- monoids with respect to it.
module Proarrow.Profunctor.Instance.Composition where

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (Profunctor (..), Promonad (..), lmap, rmap, (:~>), type (+->))
import Proarrow.Functor (Functor (..), FunctorForRep (..))

type (:.:) :: (j +-> k) -> (i +-> j) -> (i +-> k)
data (p :.: q) a c where
  (:.:) :: forall b a c p q. ~(p a b) -> ~(q b c) -> (p :.: q) a c

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

instance (Profunctor p) => Functor ((:.:) p) where
  map :: forall (a :: i +-> j) (b :: i +-> j).
(a ~> b) -> (p :.: a) ~> (p :.: b)
map (Prof a :~> b
n) = ((p :.: a) :~> (p :.: b)) -> Prof (p :.: a) (p :.: b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(p a b
p :.: a b b
q) -> p a b
p p a b -> b b b -> (:.:) p b a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: a b b -> b b b
a :~> b
n a b b
q

instance (FunctorForRep p, FunctorForRep q) => FunctorForRep (p :.: q) where
  type (p :.: q) @ b = p @ (q @ b)
  fmap :: forall (a :: j) (b :: j).
(a ~> b) -> ((p :.: q) @ a) ~> ((p :.: q) @ b)
fmap = forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @p (((q @ a) ~> (q @ b)) -> (p @ (q @ a)) ~> (p @ (q @ b)))
-> ((a ~> b) -> (q @ a) ~> (q @ b))
-> (a ~> b)
-> (p @ (q @ a)) ~> (p @ (q @ b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: j +-> j) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @q

-- The 'Proarrow.Category.Enriched.Thin.ThinProfunctor' instance for composition lives in
-- "Proarrow.Category.Enriched.Thin.Composition": in general it needs an existential over the
-- middle objects, which constraints can't express directly, so it either substitutes a
-- representable leg or, when both legs are decidable and the middle category enumerable,
-- searches the middle objects at the type level.

-- | Horizontal composition
o
  :: forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j) (s :: i +-> j)
   . p :~> q
  -> r :~> s
  -> p :.: r :~> q :.: s
p :~> q
pq o :: forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j)
       (s :: i +-> j).
(p :~> q) -> (r :~> s) -> (p :.: r) :~> (q :.: s)
`o` r :~> s
rs = \(p a b
p :.: r b b
r) -> p a b -> q a b
p :~> q
pq p a b
p q a b -> s b b -> (:.:) q s a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: r b b -> s b b
r :~> s
rs r b b
r

-- | @p :.: q@ is a `Promonad` if @p@ and @q@ are and if there's a distributive law between @p@ and @q@.
compComp :: (Promonad p, Promonad q) => q :.: p :~> p :.: q -> (p :.: q) b c -> (p :.: q) a b -> (p :.: q) a c
compComp :: forall {i} (p :: CAT i) (q :: CAT i) (b :: i) (c :: i) (a :: i).
(Promonad p, Promonad q) =>
((q :.: p) :~> (p :.: q))
-> (:.:) p q b c -> (:.:) p q a b -> (:.:) p q a c
compComp (q :.: p) :~> (p :.: q)
dist (p b b
p1 :.: q b c
q1) (p a b
p2 :.: q b b
q2) = case (:.:) q p b b -> (:.:) p q b b
(q :.: p) :~> (p :.: q)
dist (q b b
q2 q b b -> p b b -> (:.:) q p b b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
p1) of p b b
p3 :.: q b b
q3 -> (p b b
p3 p b b -> p a b -> p a b
forall (b :: i) (c :: i) (a :: i). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
p2) p a b -> q b c -> (:.:) p q a c
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (q b c
q1 q b c -> q b b -> q b c
forall (b :: i) (c :: i) (a :: i). q b c -> q a b -> q a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. q b b
q3)