{-# OPTIONS_GHC -Wno-orphans #-} module Proarrow.Profunctor.Exponential where import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (//), UN, type (+->)) import Proarrow.Category.Enriched.ThinCategory (ThinProfunctor (..), Discrete, withEq) import Proarrow.Category.Instance.Prof (Prof (..)) import Proarrow.Object.BinaryProduct (PROD (..), Prod (..)) import Proarrow.Profunctor.Product ((:*:) (..)) import Proarrow.Object.Exponential (Closed (..)) import Proarrow.Category.Instance.Constraint ((:=>) (..), reifyExp, type (:-) (..)) data (p :~>: q) a b where Exp :: (Ob a, Ob b) => (forall c d. c ~> a -> b ~> d -> p c d -> q c d) -> (p :~>: q) a b instance (Profunctor p, Profunctor q) => Profunctor (p :~>: q) where dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> (:~>:) p q a b -> (:~>:) p q c d dimap c ~> a l b ~> d r (Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d f) = c ~> a l (c ~> a) -> ((Ob c, Ob a) => (:~>:) p q c d) -> (:~>:) p q c d forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // b ~> d r (b ~> d) -> ((Ob b, Ob d) => (:~>:) p q c d) -> (:~>:) p q c d forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // (forall (c :: k) (d :: j). (c ~> c) -> (d ~> d) -> p c d -> q c d) -> (:~>:) p q c d forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type) (q :: k -> k -> Type). (Ob a, Ob b) => (forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d) -> (:~>:) p q a b Exp \c ~> c ca d ~> d bd p c d p -> (c ~> a) -> (b ~> d) -> p c d -> q c d forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d f (c ~> a l (c ~> a) -> (c ~> c) -> c ~> a forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . c ~> c ca) (d ~> d bd (d ~> d) -> (b ~> d) -> b ~> d forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . b ~> d r) p c d p (Ob a, Ob b) => r r \\ :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> (:~>:) p q a b -> r \\ Exp{} = r (Ob a, Ob b) => r r instance (CategoryOf j, CategoryOf k) => Closed (PROD (j +-> k)) where type p ~~> q = PR (UN PR p :~>: UN PR q) withObExp :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp Ob (a ~~> b) => r r = r Ob (a ~~> b) => r r curry :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry (Prod (Prof (UN 'PR a :*: UN 'PR b) :~> b1 n)) = Prof (UN 'PR a) (UN 'PR b :~>: b1) -> Prod Prof ('PR (UN 'PR a)) ('PR (UN 'PR b :~>: b1)) forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j). p a1 b1 -> Prod p ('PR a1) ('PR b1) Prod ((UN 'PR a :~> (UN 'PR b :~>: b1)) -> Prof (UN 'PR a) (UN 'PR b :~>: b1) forall {j} {k} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \UN 'PR a a b p -> UN 'PR a a b p UN 'PR a a b -> ((Ob a, Ob b) => (:~>:) (UN 'PR b) b1 a b) -> (:~>:) (UN 'PR b) b1 a b forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> UN 'PR b c d -> b1 c d) -> (:~>:) (UN 'PR b) b1 a b forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type) (q :: k -> k -> Type). (Ob a, Ob b) => (forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d) -> (:~>:) p q a b Exp \c ~> a ca b ~> d bd UN 'PR b c d q -> (:*:) (UN 'PR a) (UN 'PR b) c d -> b1 c d (UN 'PR a :*: UN 'PR b) :~> b1 n ((c ~> a) -> (b ~> d) -> UN 'PR a a b -> UN 'PR a c d forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> UN 'PR a a b -> UN 'PR a c d forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap c ~> a ca b ~> d bd UN 'PR a a b p UN 'PR a c d -> UN 'PR b c d -> (:*:) (UN 'PR a) (UN 'PR b) c d forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k). p a b -> q a b -> (:*:) p q a b :*: UN 'PR b c d q)) apply :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b apply = Prof ((UN 'PR a :~>: UN 'PR b) :*: UN 'PR a) (UN 'PR b) -> Prod Prof ('PR ((UN 'PR a :~>: UN 'PR b) :*: UN 'PR a)) ('PR (UN 'PR b)) forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j). p a1 b1 -> Prod p ('PR a1) ('PR b1) Prod ((((UN 'PR a :~>: UN 'PR b) :*: UN 'PR a) :~> UN 'PR b) -> Prof ((UN 'PR a :~>: UN 'PR b) :*: UN 'PR a) (UN 'PR b) forall {j} {k} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> UN 'PR a c d -> UN 'PR b c d f :*: UN 'PR a a b q) -> (a ~> a) -> (b ~> b) -> UN 'PR a a b -> UN 'PR b a b forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> UN 'PR a c d -> UN 'PR b c d f a ~> a forall (a :: k). Ob a => a ~> a forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a id b ~> b forall (a :: j). Ob a => a ~> a forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a id UN 'PR a a b q ((Ob a, Ob b) => UN 'PR b a b) -> UN 'PR a a b -> UN 'PR b a b forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> UN 'PR a a b -> r forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r. Profunctor p => ((Ob a, Ob b) => r) -> p a b -> r \\ UN 'PR a a b q) Prod (Prof a1 :~> b1 m) ^^^ :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (x :: PROD (j +-> k)) (y :: PROD (j +-> k)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) ^^^ Prod (Prof a1 :~> b1 n) = Prof (b1 :~>: a1) (a1 :~>: b1) -> Prod Prof ('PR (b1 :~>: a1)) ('PR (a1 :~>: b1)) forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j). p a1 b1 -> Prod p ('PR a1) ('PR b1) Prod (((b1 :~>: a1) :~> (a1 :~>: b1)) -> Prof (b1 :~>: a1) (a1 :~>: b1) forall {j} {k} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d f) -> (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> a1 c d -> b1 c d) -> (:~>:) a1 b1 a b forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type) (q :: k -> k -> Type). (Ob a, Ob b) => (forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d) -> (:~>:) p q a b Exp \c ~> a ca b ~> d bd a1 c d p -> a1 c d -> b1 c d a1 :~> b1 m ((c ~> a) -> (b ~> d) -> b1 c d -> a1 c d forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d f c ~> a ca b ~> d bd (a1 c d -> b1 c d a1 :~> b1 n a1 c d p))) instance (ThinProfunctor p, ThinProfunctor q, Discrete j, Discrete k) => ThinProfunctor (p :~>: q :: j +-> k) where type HasArrow (p :~>: q) a b = (HasArrow p a b :=> HasArrow q a b) arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (p :~>: q) a b) => (:~>:) p q a b arr @a @b = (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d) -> (:~>:) p q a b forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type) (q :: k -> k -> Type). (Ob a, Ob b) => (forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d) -> (:~>:) p q a b Exp \c ~> a ca b ~> d bd p c d p -> (c ~> a) -> ((c ~ a) => q c d) -> q c d forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r forall {k} (p :: k +-> k) (a :: k) (b :: k) r. DiscreteProfunctor p => p a b -> ((a ~ b) => r) -> r withEq c ~> a ca ((b ~> d) -> ((b ~ d) => q c d) -> q c d forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r forall {k} (p :: k +-> k) (a :: k) (b :: k) r. DiscreteProfunctor p => p a b -> ((a ~ b) => r) -> r withEq b ~> d bd (p c d -> (HasArrow p c d => q c d) -> q c d forall (a :: k) (b :: j) r. p a b -> (HasArrow p a b => r) -> r forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r. ThinProfunctor p => p a b -> (HasArrow p a b => r) -> r withArr p c d p (('CNSTRNT (HasArrow p a b) :- 'CNSTRNT (HasArrow q a b)) -> forall r. HasArrow p a b => (HasArrow q a b => r) -> r forall (a :: Constraint) (b :: Constraint). ('CNSTRNT a :- 'CNSTRNT b) -> forall r. a => (b => r) -> r unEntails (forall (b :: Constraint) (c :: Constraint). (b :=> c) => 'CNSTRNT b :- 'CNSTRNT c entails @(HasArrow p a b) @(HasArrow q a b)) q c d HasArrow q a b => q c d forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow q a b) => q a b forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (ThinProfunctor p, Ob a, Ob b, HasArrow p a b) => p a b arr))) withArr :: forall (a :: k) (b :: j) r. (:~>:) p q a b -> (HasArrow (p :~>: q) a b => r) -> r withArr @a @b (Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d f) = ('CNSTRNT (HasArrow p a b) :- 'CNSTRNT (HasArrow q a b)) -> ((HasArrow p a b :=> HasArrow q a b) => r) -> r forall (b :: Constraint) (c :: Constraint) r. ('CNSTRNT b :- 'CNSTRNT c) -> ((b :=> c) => r) -> r reifyExp (forall (a1 :: Constraint) (b1 :: Constraint). (forall r. a1 => (b1 => r) -> r) -> 'CNSTRNT a1 :- 'CNSTRNT b1 Entails @(HasArrow p a b) @(HasArrow q a b) (q a b -> (HasArrow q a b => r) -> r forall (a :: k) (b :: j) r. q a b -> (HasArrow q a b => r) -> r forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r. ThinProfunctor p => p a b -> (HasArrow p a b => r) -> r withArr ((a ~> a) -> (b ~> b) -> p a b -> q a b forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d f a ~> a forall (a :: k). Ob a => a ~> a forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a id b ~> b forall (a :: j). Ob a => a ~> a forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a id p a b forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow p a b) => p a b forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (ThinProfunctor p, Ob a, Ob b, HasArrow p a b) => p a b arr)))