{-# 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