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