module Proarrow.Profunctor.Rift where

import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), (//), lmap)
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 p <| j = Rift (OP j) p

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

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

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

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

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

newtype Precompose j p a b = Precompose { forall {j} {k} {i} (j :: PRO j k) (p :: PRO i j) (a :: i) (b :: k).
Precompose j p a b -> (:.:) p j a b
getPrecompose :: (p :.: j) a b }
instance (Profunctor j, Profunctor p) => Profunctor (Precompose j p) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Precompose j p a b -> Precompose j p c d
dimap c ~> a
l b ~> d
r (Precompose (:.:) p j a b
pj) = (:.:) p j c d -> Precompose j p c d
forall {j} {k} {i} (j :: PRO j k) (p :: PRO i j) (a :: i) (b :: k).
(:.:) p j a b -> Precompose j p a b
Precompose ((c ~> a) -> (b ~> d) -> (:.:) p j a b -> (:.:) p j c d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (:.:) p j a b -> (:.:) p j 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 j a b
pj)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> Precompose j p a b -> r
\\ Precompose (:.:) p j a b
pj = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (:.:) p j a b -> r
forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> (:.:) p 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
\\ (:.:) p j a b
pj
instance Profunctor j => Functor (Precompose j) where
  map :: forall (a :: PRO i j) (b :: PRO i j).
(a ~> b) -> Precompose j a ~> Precompose j b
map a ~> b
f = a ~> b
Prof a b
f Prof a b
-> ((Ob a, Ob b) => Prof (Precompose j a) (Precompose j b))
-> Prof (Precompose j a) (Precompose j b)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Precompose j a :~> Precompose j b)
-> Prof (Precompose j a) (Precompose j b)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Precompose (:.:) a j a b
pj) -> (:.:) b j a b -> Precompose j b a b
forall {j} {k} {i} (j :: PRO j k) (p :: PRO i j) (a :: i) (b :: k).
(:.:) p j a b -> Precompose j p a b
Precompose (Prof (a :.: j) (b :.: j) -> (a :.: j) :~> (b :.: j)
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
getProf (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)) (:.:) a j a b
pj)

instance Profunctor j => Adjunction (Star (Precompose j)) (Star (Rift (OP j))) where
  unit :: forall (a :: PRO i k).
Ob a =>
(:.:) (Star (Rift ('OP j))) (Star (Precompose j)) a a
unit = (a ~> Rift ('OP j) (Precompose j a))
-> (:.:) (Star (Rift ('OP j))) (Star (Precompose 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 :~> Rift ('OP j) (Precompose j a))
-> Prof a (Rift ('OP j) (Precompose 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) => Rift ('OP j) (Precompose j a) a b)
-> Rift ('OP j) (Precompose 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 b x -> Precompose j a a x)
-> Rift ('OP j) (Precompose j a) a b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO k i) (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j b x -> p a x) -> Rift ('OP j) p a b
Rift \j b x
j -> (:.:) a j a x -> Precompose j a a x
forall {j} {k} {i} (j :: PRO j k) (p :: PRO i j) (a :: i) (b :: k).
(:.:) p j a b -> Precompose j p a b
Precompose (a a b
p a a b -> j b x -> (:.:) a j a x
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
:.: j b x
j))
  counit :: (Star (Precompose j) :.: Star (Rift ('OP j))) :~> (~>)
counit = (forall (c :: i -> i -> Type).
 Ob c =>
 Precompose j (Rift ('OP j) c) ~> c)
-> (:.:) (Star (Precompose j)) (Star (Rift ('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 ((Precompose j (Rift ('OP j) c) :~> c)
-> Prof (Precompose j (Rift ('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 \(Precompose (Rift ('OP j) c a b
r :.: j b b
j)) -> j b b -> Rift ('OP j) c a b -> c a b
forall {k} {i} {j} (j :: PRO k i) (b :: k) (x :: i) (p :: PRO j i)
       (a :: j).
Profunctor j =>
j b x -> Rift ('OP j) p a b -> p a x
runRift j b b
j Rift ('OP j) c a b
r)

riftCompose :: (Profunctor i, Profunctor j, Profunctor p) => Rift (OP i) (Rift (OP j) p) ~> Rift (OP (i :.: j)) p
riftCompose :: forall {k} {j} {i} {j} (i :: PRO k j) (j :: PRO j i)
       (p :: PRO j i).
(Profunctor i, Profunctor j, Profunctor p) =>
Rift ('OP i) (Rift ('OP j) p) ~> Rift ('OP (i :.: j)) p
riftCompose = (Rift ('OP i) (Rift ('OP j) p) :~> Rift ('OP (i :.: j)) p)
-> Prof (Rift ('OP i) (Rift ('OP j) p)) (Rift ('OP (i :.: j)) p)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \Rift ('OP i) (Rift ('OP j) p) a b
k -> Rift ('OP i) (Rift ('OP j) p) a b
k Rift ('OP i) (Rift ('OP j) p) a b
-> ((Ob a, Ob b) => Rift ('OP (i :.: j)) p a b)
-> Rift ('OP (i :.: 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 :: i). Ob x => (:.:) i j b x -> p a x)
-> Rift ('OP (i :.: j)) p a b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO k i) (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j b x -> p a x) -> Rift ('OP j) p a b
Rift \(i b b
i :.: j b x
j) -> j b x -> Rift ('OP j) p a b -> p a x
forall {k} {i} {j} (j :: PRO k i) (b :: k) (x :: i) (p :: PRO j i)
       (a :: j).
Profunctor j =>
j b x -> Rift ('OP j) p a b -> p a x
runRift j b x
j (i b b -> Rift ('OP i) (Rift ('OP j) p) a b -> Rift ('OP j) p a b
forall {k} {i} {j} (j :: PRO k i) (b :: k) (x :: i) (p :: PRO j i)
       (a :: j).
Profunctor j =>
j b x -> Rift ('OP j) p a b -> p a x
runRift i b b
i Rift ('OP i) (Rift ('OP j) p) a b
k)

riftComposeInv :: (Profunctor i, Profunctor j, Profunctor p) => Rift (OP (i :.: j)) p ~> Rift (OP i) (Rift (OP j) p)
riftComposeInv :: forall {k} {k} {i} {j} (i :: PRO k k) (j :: PRO k i)
       (p :: PRO j i).
(Profunctor i, Profunctor j, Profunctor p) =>
Rift ('OP (i :.: j)) p ~> Rift ('OP i) (Rift ('OP j) p)
riftComposeInv = (Rift ('OP (i :.: j)) p :~> Rift ('OP i) (Rift ('OP j) p))
-> Prof (Rift ('OP (i :.: j)) p) (Rift ('OP i) (Rift ('OP j) p))
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \Rift ('OP (i :.: j)) p a b
k -> Rift ('OP (i :.: j)) p a b
k Rift ('OP (i :.: j)) p a b
-> ((Ob a, Ob b) => Rift ('OP i) (Rift ('OP j) p) a b)
-> Rift ('OP i) (Rift ('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 :: k). Ob x => i b x -> Rift ('OP j) p a x)
-> Rift ('OP i) (Rift ('OP j) p) a b
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO k i) (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j b x -> p a x) -> Rift ('OP j) p a b
Rift \i b x
i -> (forall (x :: i). Ob x => j x x -> p a x) -> Rift ('OP j) p a x
forall {j} {k} {i} (a :: j) (b :: k) (j :: PRO k i) (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j b x -> p a x) -> Rift ('OP j) p a b
Rift \j x x
j -> (:.:) i j b x -> Rift ('OP (i :.: j)) p a b -> p a x
forall {k} {i} {j} (j :: PRO k i) (b :: k) (x :: i) (p :: PRO j i)
       (a :: j).
Profunctor j =>
j b x -> Rift ('OP j) p a b -> p a x
runRift (i b x
i i b x -> j x x -> (:.:) i j b x
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
:.: j x x
j) Rift ('OP (i :.: j)) p a b
k