module Proarrow.Profunctor.Composition where

import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, rmap, type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), withCorepObj)
import Proarrow.Profunctor.Representable (Representable (..), withRepObj)

type (:.:) :: (j +-> k) -> (i +-> j) -> (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 {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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 :: 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 {k} {j} (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} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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 :: j +-> k) (b :: j +-> k).
(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 {k} {j} (p :: j +-> k) (q :: 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 {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
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 {j} {k} {i} (a :: j +-> k) (b :: j +-> k) (c :: i +-> j)
       (d :: i +-> j).
(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
unNat ((a ~> b) -> (:.:) a ~> (:.:) b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: j +-> k) (b :: j +-> k).
(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 :: i +-> k) (c :: i +-> k) (a :: 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 :: i +-> j) (b :: i +-> j).
(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 :: j +-> k) (b :: j +-> k) 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 :: i +-> j) (b :: i +-> j) 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 :: k) (b :: j). (:.:) p q a b -> a ~> ((p :.: q) % b)
index (p a b
p :.: q b b
q) = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (q b b -> b ~> (q % b)
forall (a :: j) (b :: j). q a b -> a ~> (q % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
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 :: 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
. p a b -> a ~> (p % b)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
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 :: k) (b :: j).
Ob b =>
(a ~> ((p :.: q) % b)) -> (:.:) p q a b
tabulate a ~> ((p :.: q) % b)
f = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> j) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepObj @q @b ((a ~> (p % (q % b))) -> p a (q % b)
forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(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 {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((q % b) ~> (q % b)) -> q (q % b) b
forall (b :: j) (a :: j). Ob b => (a ~> (q % b)) -> q a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(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 :: j) (b :: j).
(a ~> b) -> ((p :.: q) % a) ~> ((p :.: q) % b)
repMap a ~> b
f = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> j) (a :: j) (b :: j).
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 :: k) (b :: j). (:.:) 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 :: j). q a b -> (q %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
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 :: 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
. forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> j) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @q (p a b -> (p %% a) ~> b
forall (a :: k) (b :: j). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
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 :: k) (b :: j).
Ob a =>
(((p :.: q) %% a) ~> b) -> (:.:) p q a b
cotabulate ((p :.: q) %% a) ~> b
f = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> k) (a :: k) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withCorepObj @p @a (((p %% a) ~> (p %% a)) -> p a (p %% a)
forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(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 {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((q %% (p %% a)) ~> b) -> q (p %% a) b
forall (a :: j) (b :: j). Ob a => ((q %% a) ~> b) -> q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (q %% (p %% a)) ~> b
((p :.: q) %% a) ~> b
f)
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> ((p :.: q) %% a) ~> ((p :.: q) %% b)
corepMap a ~> b
f = forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> j) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @q (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p a ~> b
f)

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

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