module Proarrow.Profunctor.Composition where

import Proarrow.Core (PRO, Profunctor(..), CategoryOf(..), Promonad (..), lmap, rmap)
import Proarrow.Functor (Functor(..))
import Proarrow.Category.Instance.Prof (Prof(..))
import Proarrow.Category.Instance.Nat (Nat(..))
import Proarrow.Profunctor.Representable (Representable(..), withRepCod)
import Proarrow.Profunctor.Corepresentable (Corepresentable(..), withCorepCod)
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))


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

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

instance Profunctor p => Functor ((:.:) p) where
  map :: forall (a :: PRO j k) (b :: PRO j k).
(a ~> b) -> (p :.: a) ~> (p :.: b)
map (Prof a :~> b
n) = ((p :.: a) :~> (p :.: b)) -> Prof (p :.: a) (p :.: b)
forall {j} {k} (p :: PRO j k) (q :: PRO 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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: a b b -> b b b
a :~> b
n a b b
q

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

bimapComp :: (a ~> b) -> (c ~> d) -> a :.: c ~> b :.: d
bimapComp :: forall {i} {j} {k} (a :: PRO i j) (b :: PRO i j) (c :: PRO j k)
       (d :: PRO j k).
(a ~> b) -> (c ~> d) -> (a :.: c) ~> (b :.: d)
bimapComp a ~> b
f c ~> d
g = Nat ((:.:) a) ((:.:) b) -> (:.:) a .~> (:.:) b
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
getNat ((a ~> b) -> (:.:) a ~> (:.:) b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: PRO i j) (b :: PRO i j).
(a ~> b) -> (:.:) a ~> (:.:) b
map a ~> b
f) Prof (a :.: d) (b :.: d)
-> Prof (a :.: c) (a :.: d) -> Prof (a :.: c) (b :.: d)
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: PRO i k) (c :: PRO i k) (a :: PRO i k).
Prof b c -> Prof a b -> Prof a c
. (c ~> d) -> (a :.: c) ~> (a :.: d)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: PRO j k) (b :: PRO j k).
(a ~> b) -> (a :.: a) ~> (a :.: b)
map c ~> d
g ((Ob a, Ob b) => Prof (a :.: c) (b :.: d))
-> Prof a b -> Prof (a :.: c) (b :.: d)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: PRO i j) (b :: PRO i j) r.
((Ob a, Ob b) => r) -> Prof a b -> r
\\ a ~> b
Prof a b
f ((Ob c, Ob d) => Prof (a :.: c) (b :.: d))
-> Prof c d -> Prof (a :.: c) (b :.: d)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: PRO j k) (b :: PRO j k) r.
((Ob a, Ob b) => r) -> Prof a b -> r
\\ c ~> d
Prof c d
g

instance (Representable p, Representable q) => Representable (p :.: q) where
  type (p :.: q) % a = p % (q % a)
  index :: forall (a :: j) (b :: k). (:.:) p q a b -> a ~> ((p :.: q) % b)
index (p a b
p :.: q b b
q) = forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j j) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (q b b -> b ~> (q % b)
forall (a :: j) (b :: k). q a b -> a ~> (q % b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index q b b
q) ((p % b) ~> (p % (q % b))) -> (a ~> (p % b)) -> a ~> (p % (q % b))
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> a ~> (p % b)
forall (a :: j) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index p a b
p
  tabulate :: forall a b. Ob b => (a ~> ((p :.: q) % b)) -> (:.:) p q a b
  tabulate :: forall (a :: j) (b :: k).
Ob b =>
(a ~> ((p :.: q) % b)) -> (:.:) p q a b
tabulate a ~> ((p :.: q) % b)
f = forall {k1} {k2} (p :: PRO k1 k2) (a :: k2) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: PRO j k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepCod @q @b ((a ~> (p % (q % b))) -> p a (q % b)
forall (b :: j) (a :: j). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a ~> (p % (q % b))
a ~> ((p :.: q) % b)
f p a (q % b) -> q (q % b) b -> (:.:) p q a b
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: ((q % b) ~> (q % b)) -> q (q % b) b
forall (b :: k) (a :: j). Ob b => (a ~> (q % b)) -> q a b
forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (q % b) ~> (q % b)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  repMap :: forall (a :: k) (b :: k).
(a ~> b) -> ((p :.: q) % a) ~> ((p :.: q) % b)
repMap a ~> b
f = forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j j) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall {j} {k} (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @q a ~> b
f)

instance (Corepresentable p, Corepresentable q) => Corepresentable (p :.: q) where
  type (p :.: q) %% a = q %% (p %% a)
  coindex :: forall (a :: j) (b :: k). (:.:) p q a b -> ((p :.: q) %% a) ~> b
coindex (p a b
p :.: q b b
q) = q b b -> (q %% b) ~> b
forall (a :: j) (b :: k). q a b -> (q %% a) ~> b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex q b b
q ((q %% b) ~> b)
-> ((q %% (p %% a)) ~> (q %% b)) -> (q %% (p %% a)) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @q (p a b -> (p %% a) ~> b
forall (a :: j) (b :: j). p a b -> (p %% a) ~> b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p a b
p)
  cotabulate :: forall a b. Ob a => (((p :.: q) %% a) ~> b) -> (:.:) p q a b
  cotabulate :: forall (a :: j) (b :: k).
Ob a =>
(((p :.: q) %% a) ~> b) -> (:.:) p q a b
cotabulate ((p :.: q) %% a) ~> b
f = forall {j} {k} (p :: PRO j k) (a :: j) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: PRO j j) (a :: j) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withCorepCod @p @a (((p %% a) ~> (p %% a)) -> p a (p %% a)
forall (a :: j) (b :: j). Ob a => ((p %% a) ~> b) -> p a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (p %% a) ~> (p %% a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id p a (p %% a) -> q (p %% a) b -> (:.:) p q a b
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: ((q %% (p %% a)) ~> b) -> q (p %% a) b
forall (a :: j) (b :: k). Ob a => ((q %% a) ~> b) -> q a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate ((p :.: q) %% a) ~> b
(q %% (p %% a)) ~> b
f)
  corepMap :: forall (a :: j) (b :: j).
(a ~> b) -> ((p :.: q) %% a) ~> ((p :.: q) %% b)
corepMap a ~> b
f = forall {j} {k} (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @q (forall {j} {k} (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: PRO j j) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p a ~> b
f)

instance (MonoidalProfunctor p, MonoidalProfunctor q) => MonoidalProfunctor (p :.: q) where
  lift0 :: (:.:) p q Unit Unit
lift0 = p Unit Unit
forall j k (p :: PRO j k). MonoidalProfunctor p => p Unit Unit
lift0 p Unit Unit -> q Unit Unit -> (:.:) p q Unit Unit
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: q Unit Unit
forall j k (p :: PRO j k). MonoidalProfunctor p => p Unit Unit
lift0
  lift2 :: forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
(:.:) p q x1 x2
-> (:.:) p q y1 y2 -> (:.:) p q (x1 ** y1) (x2 ** y2)
lift2 (p x1 b
p :.: q b x2
q) (p y1 b
r :.: q b y2
s) = p x1 b -> p y1 b -> p (x1 ** y1) (b ** b)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall j k (p :: PRO j k) (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
lift2 p x1 b
p p y1 b
r p (x1 ** y1) (b ** b)
-> q (b ** b) (x2 ** y2) -> (:.:) p q (x1 ** y1) (x2 ** y2)
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: q b x2 -> q b y2 -> q (b ** b) (x2 ** y2)
forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
q x1 x2 -> q y1 y2 -> q (x1 ** y1) (x2 ** y2)
forall j k (p :: PRO j k) (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
lift2 q b x2
q q b y2
s


-- | Horizontal composition
o :: forall {i} {j} {k} (p :: PRO i j) (q :: PRO i j) (r :: PRO j k) (s :: PRO j k)
  . Prof p q -> Prof r s -> Prof (p :.: r) (q :.: s)
Prof p :~> q
pq o :: forall {i} {j} {k} (p :: PRO i j) (q :: PRO i j) (r :: PRO j k)
       (s :: PRO j k).
Prof p q -> Prof r s -> Prof (p :.: r) (q :.: s)
`o` Prof r :~> s
rs = ((p :.: r) :~> (q :.: s)) -> Prof (p :.: r) (q :.: s)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: r b b -> s b b
r :~> s
rs r b b
r