{-# LANGUAGE DerivingStrategies #-}
module Proarrow.Profunctor.Ran where

import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), (//), rmap)
import Proarrow.Functor (Functor(..))
import Proarrow.Category.Instance.Prof (Prof(..))
import Proarrow.Category.Instance.Nat (Nat(..))
import Proarrow.Category.Opposite (OPPOSITE(..), Op(..))
import Proarrow.Adjunction (Adjunction (..), unitFromStarUnit, counitFromStarCounit)
import Proarrow.Profunctor.Composition ((:.:)(..))
import Proarrow.Profunctor.Star (Star(..))

type j |> p = Ran (OP j) p

type Ran :: OPPOSITE (PRO i j) -> PRO i k -> PRO j k
data Ran j p a b where
  Ran :: (Ob a, Ob b) => { forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO i j) (p :: PRO i k).
Ran ('OP j) p a b -> forall (x :: i). Ob x => j x a -> p x b
getRan :: forall x. Ob x => j x a -> p x b } -> Ran (OP j) p a b

runRan :: Profunctor j => j x a -> Ran (OP j) p a b -> p x b
runRan :: forall {i} {j} {k} (j :: PRO i j) (x :: i) (a :: j) (p :: PRO i k)
       (b :: k).
Profunctor j =>
j x a -> Ran ('OP j) p a b -> p x b
runRan j x a
j (Ran forall (x :: i). Ob x => j x a -> p x b
k) = j x a -> p x b
forall (x :: i). Ob x => j x a -> p x b
k j x a
j x a
j ((Ob x, Ob a) => p x b) -> j x a -> p x b
forall (a :: i) (b :: j) r. ((Ob a, Ob b) => r) -> j 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
\\ j x a
j

instance (Profunctor p, Profunctor j) => Profunctor (Ran (OP j) p) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Ran ('OP j) p a b -> Ran ('OP j) p c d
dimap c ~> a
l b ~> d
r (Ran forall (x :: i). Ob x => j x a -> p x b
k) = c ~> a
l (c ~> a)
-> ((Ob c, Ob a) => Ran ('OP j) p c d) -> Ran ('OP j) p c d
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> d
r (b ~> d)
-> ((Ob b, Ob d) => Ran ('OP j) p c d) -> Ran ('OP j) p c d
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: i). Ob x => j x c -> p x d) -> Ran ('OP j) p c d
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO i j) (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Ran ('OP j) p a b
Ran ((b ~> d) -> p x b -> p x 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 (p x b -> p x d) -> (j x c -> p x b) -> j x c -> p x d
forall b c a. (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
. j x a -> p x b
j x a -> p x b
forall (x :: i). Ob x => j x a -> p x b
k (j x a -> p x b) -> (j x c -> j x a) -> j x c -> p x b
forall b c a. (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
. (c ~> a) -> j x c -> j x a
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap c ~> a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> Ran ('OP j) p a b -> r
\\ Ran{} = r
(Ob a, Ob b) => r
r

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

instance Functor Ran where
  map :: forall (a :: OPPOSITE (PRO i j)) (b :: OPPOSITE (PRO i j)).
(a ~> b) -> Ran a ~> Ran b
map (Op (Prof b1 :~> a1
n)) = (Ran ('OP a1) .~> Ran ('OP b1))
-> Nat (Ran ('OP a1)) (Ran ('OP b1))
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((Ran ('OP a1) a :~> Ran ('OP b1) a)
-> Prof (Ran ('OP a1) a) (Ran ('OP b1) a)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Ran forall (x :: i). Ob x => j x a -> a x b
k) -> (forall (x :: i). Ob x => b1 x a -> a x b) -> Ran ('OP b1) a a b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO i j) (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Ran ('OP j) p a b
Ran (a1 x a -> a x b
j x a -> a x b
forall (x :: i). Ob x => j x a -> a x b
k (a1 x a -> a x b) -> (b1 x a -> a1 x a) -> b1 x a -> a x b
forall b c a. (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
. b1 x a -> a1 x a
b1 :~> a1
n))

instance Profunctor j => Adjunction (Star ((:.:) j)) (Star (Ran (OP j))) where
  unit :: forall (a :: PRO j k).
Ob a =>
(:.:) (Star (Ran ('OP j))) (Star ((:.:) j)) a a
unit = (a ~> Ran ('OP j) (j :.: a))
-> (:.:) (Star (Ran ('OP j))) (Star ((:.:) j)) a a
forall {k} {k2} (l :: k -> k2) (r :: k2 -> k) (a :: k).
(Functor l, Ob a) =>
(a ~> r (l a)) -> (:.:) (Star r) (Star l) a a
unitFromStarUnit ((a :~> Ran ('OP j) (j :.: a)) -> Prof a (Ran ('OP j) (j :.: 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 a b
p a a b
-> ((Ob a, Ob b) => Ran ('OP j) (j :.: a) a b)
-> Ran ('OP j) (j :.: a) a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: i). Ob x => j x a -> (:.:) j a x b)
-> Ran ('OP j) (j :.: a) a b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO i j) (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Ran ('OP j) p a b
Ran (j x a -> a a b -> (:.:) j a x 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 a b
p))
  counit :: (Star ((:.:) j) :.: Star (Ran ('OP j))) :~> (~>)
counit = (forall (c :: i -> k -> Type). Ob c => (j :.: Ran ('OP j) c) ~> c)
-> (:.:) (Star ((:.:) j)) (Star (Ran ('OP j))) a b -> a ~> b
forall {j} {k} (l :: j -> k) (r :: k -> j) (a :: k) (b :: k).
Functor l =>
(forall (c :: k). Ob c => l (r c) ~> c)
-> (:.:) (Star l) (Star r) a b -> a ~> b
counitFromStarCounit (((j :.: Ran ('OP j) c) :~> c) -> Prof (j :.: Ran ('OP j) c) c
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(j a b
j :.: Ran ('OP j) c b b
r) -> j a b -> Ran ('OP j) c b b -> c a b
forall {i} {j} {k} (j :: PRO i j) (x :: i) (a :: j) (p :: PRO i k)
       (b :: k).
Profunctor j =>
j x a -> Ran ('OP j) p a b -> p x b
runRan j a b
j Ran ('OP j) c b b
r)

ranCompose :: (Profunctor i, Profunctor j, Profunctor p) => Ran (OP i) (Ran (OP j) p) ~> Ran (OP (j :.: i)) p
ranCompose :: forall {j} {j} {i} {k} (i :: PRO j j) (j :: PRO i j)
       (p :: PRO i k).
(Profunctor i, Profunctor j, Profunctor p) =>
Ran ('OP i) (Ran ('OP j) p) ~> Ran ('OP (j :.: i)) p
ranCompose = (Ran ('OP i) (Ran ('OP j) p) :~> Ran ('OP (j :.: i)) p)
-> Prof (Ran ('OP i) (Ran ('OP j) p)) (Ran ('OP (j :.: i)) p)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \Ran ('OP i) (Ran ('OP j) p) a b
k -> Ran ('OP i) (Ran ('OP j) p) a b
k Ran ('OP i) (Ran ('OP j) p) a b
-> ((Ob a, Ob b) => Ran ('OP (j :.: i)) p a b)
-> Ran ('OP (j :.: i)) p a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: i). Ob x => (:.:) j i x a -> p x b)
-> Ran ('OP (j :.: i)) p a b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO i j) (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Ran ('OP j) p a b
Ran \(j x b
j :.: i b a
i) -> j x b -> Ran ('OP j) p b b -> p x b
forall {i} {j} {k} (j :: PRO i j) (x :: i) (a :: j) (p :: PRO i k)
       (b :: k).
Profunctor j =>
j x a -> Ran ('OP j) p a b -> p x b
runRan j x b
j (i b a -> Ran ('OP i) (Ran ('OP j) p) a b -> Ran ('OP j) p b b
forall {i} {j} {k} (j :: PRO i j) (x :: i) (a :: j) (p :: PRO i k)
       (b :: k).
Profunctor j =>
j x a -> Ran ('OP j) p a b -> p x b
runRan i b a
i Ran ('OP i) (Ran ('OP j) p) a b
k)

ranComposeInv :: (Profunctor i, Profunctor j, Profunctor p) => Ran (OP (j :.: i)) p ~> Ran (OP i) (Ran (OP j) p)
ranComposeInv :: forall {j} {j} {i} {k} (i :: PRO j j) (j :: PRO i j)
       (p :: PRO i k).
(Profunctor i, Profunctor j, Profunctor p) =>
Ran ('OP (j :.: i)) p ~> Ran ('OP i) (Ran ('OP j) p)
ranComposeInv = (Ran ('OP (j :.: i)) p :~> Ran ('OP i) (Ran ('OP j) p))
-> Prof (Ran ('OP (j :.: i)) p) (Ran ('OP i) (Ran ('OP j) p))
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \Ran ('OP (j :.: i)) p a b
k -> Ran ('OP (j :.: i)) p a b
k Ran ('OP (j :.: i)) p a b
-> ((Ob a, Ob b) => Ran ('OP i) (Ran ('OP j) p) a b)
-> Ran ('OP i) (Ran ('OP j) p) a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: j). Ob x => i x a -> Ran ('OP j) p x b)
-> Ran ('OP i) (Ran ('OP j) p) a b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO i j) (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Ran ('OP j) p a b
Ran \i x a
i -> (forall (x :: i). Ob x => j x x -> p x b) -> Ran ('OP j) p x b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO i j) (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Ran ('OP j) p a b
Ran \j x x
j -> (:.:) j i x a -> Ran ('OP (j :.: i)) p a b -> p x b
forall {i} {j} {k} (j :: PRO i j) (x :: i) (a :: j) (p :: PRO i k)
       (b :: k).
Profunctor j =>
j x a -> Ran ('OP j) p a b -> p x b
runRan (j x x
j j x x -> i x a -> (:.:) j i x a
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
:.: i x a
i) Ran ('OP (j :.: i)) p a b
k