module Proarrow.Profunctor.Rift where

import Prelude (type (~))

import Proarrow.Adjunction (Adjunction (..), counitFromRepCounit, unitFromRepUnit)
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, rmap, (//), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Costar (Costar (..))
import Proarrow.Profunctor.Star (Star (..))

-- Note: Ran and Rift are swapped compared to the profunctors package.

type p <| j = Rift (OP j) p

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

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

flipRift :: (Functor j, Profunctor p) => p <| Star j ~> Costar j :.: p
flipRift :: forall {k} {j} {i} (j :: k -> j) (p :: PRO j i).
(Functor j, Profunctor p) =>
(p <| Star j) ~> (Costar j :.: p)
flipRift = ((p <| Star j) :~> (Costar j :.: p))
-> Prof (p <| Star j) (Costar j :.: p)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rift forall (x :: j). Ob x => j x a -> p x b
k) -> (j a ~> j a) -> Costar j a (j a)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar j a ~> j a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Costar j a (j a) -> p (j a) b -> (:.:) (Costar j) p 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
:.: j (j a) a -> p (j a) b
forall (x :: j). Ob x => j x a -> p x b
k ((j a ~> j a) -> Star j (j a) a
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star j a ~> j a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)

flipRiftInv :: (Functor j, Profunctor p) => Costar j :.: p ~> p <| Star j
flipRiftInv :: forall {k} {k2} {j} (j :: k -> k2) (p :: PRO k2 j).
(Functor j, Profunctor p) =>
(Costar j :.: p) ~> (p <| Star j)
flipRiftInv = ((Costar j :.: p) :~> (p <| Star j))
-> Prof (Costar j :.: p) (p <| Star j)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Costar j a ~> b
f :.: p b b
p) -> p b b
p p b b
-> ((Ob b, Ob b) => (<|) p (Star j) a b) -> (<|) p (Star j) 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 :: k2). Ob x => Star j x a -> p x b)
-> (<|) p (Star j) a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Rift ('OP j) p a b
Rift \(Star x ~> j a
g) -> (x ~> b) -> p b b -> p x 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 (j a ~> b
f (j a ~> b) -> (x ~> j a) -> x ~> b
forall (b :: k2) (c :: k2) (a :: k2).
(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
. x ~> j a
g) p b b
p

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 x a -> p x b
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 x c -> p x d) -> Rift ('OP j) p c d
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Rift ('OP j) p a b
Rift ((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) -> 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 :: j +-> i) (b :: 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 {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rift forall (x :: i). Ob x => j x a -> a x b
k) -> (forall (x :: i). Ob x => j x a -> b x b) -> Rift ('OP j) b a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Rift ('OP j) p a b
Rift (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 Rift where
  map :: forall (a :: OPPOSITE (k +-> i)) (b :: OPPOSITE (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 {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rift forall (x :: i). Ob x => j x a -> a x b
k) -> (forall (x :: i). Ob x => b1 x a -> a x b) -> Rift ('OP b1) a a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Rift ('OP j) p a b
Rift (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 (Rift (OP j))) where
  unit :: forall (a :: i +-> k).
Ob a =>
(:.:) (Star (Rift ('OP j))) (Star ((:.:) j)) a a
unit = (a ~> (Star (Rift ('OP j)) % (Star ((:.:) j) % a)))
-> (:.:) (Star (Rift ('OP j))) (Star ((:.:) j)) a a
forall {i} {j} (l :: i +-> j) (r :: j +-> i) (a :: i).
(Representable l, Representable r, Ob a) =>
(a ~> (r % (l % a))) -> (:.:) r l a a
unitFromRepUnit ((a :~> Rift ('OP j) (j :.: a)) -> Prof a (Rift ('OP j) (j :.: 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 a b
p a a b
-> ((Ob a, Ob b) => Rift ('OP j) (j :.: a) a b)
-> Rift ('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)
-> Rift ('OP j) (j :.: a) a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j x a -> p x b) -> Rift ('OP j) p a b
Rift (j x a -> a a b -> (:.:) j a x 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 a b
p))
  counit :: (Star ((:.:) j) :.: Star (Rift ('OP j))) :~> (~>)
counit = (forall (c :: i -> i -> Type).
 Ob c =>
 (Star ((:.:) j) % (Star (Rift ('OP j)) % c)) ~> c)
-> (Star ((:.:) j) :.: Star (Rift ('OP j))) :~> (~>)
forall {j} {k1} (l :: j +-> k1) (r :: k1 +-> j).
(Representable l, Representable r) =>
(forall (c :: k1). Ob c => (l % (r % c)) ~> c)
-> (l :.: r) :~> (~>)
counitFromRepCounit (((j :.: Rift ('OP j) c) :~> c) -> Prof (j :.: Rift ('OP j) c) c
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(j a b
j :.: Rift ('OP j) c b b
r) -> j a b -> Rift ('OP j) c b b -> c a b
forall {i} {k} {j} (j :: PRO i k) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift j a b
j Rift ('OP j) c b b
r)

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

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

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