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