{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}

module Proarrow.Object.Power where

import Data.Kind (Type)
import Prelude (($), type (~))

import Proarrow.Category.Enriched (Enriched, EnrichedProfunctor (..), HomObj, comp)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (leftUnitorInvWith)
import Proarrow.Core (CategoryOf (..), Ob, Profunctor (..), Promonad (..), (//), type (+->))
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Terminal (TerminalObject, terminate)

-- | Categories powered over Hask.
class (Enriched v k, Closed v) => Powered v k where
  type (a :: k) ^ (n :: v) :: k
  withObPower :: (Ob (a :: k), Ob (n :: v)) => ((Ob (a ^ n)) => r) -> r
  power :: (Ob (a :: k), Ob b) => (n ~> HomObj v a b) -> a ~> (b ^ n)
  unpower :: (Ob (b :: k), Ob n) => a ~> (b ^ n) -> n ~> HomObj v a b

mapBase :: forall {k} {v} (n :: v) (a :: k) b. (Powered v k, Ob n) => a ~> b -> a ^ n ~> b ^ n
mapBase :: forall {k} {v} (n :: v) (a :: k) (b :: k).
(Powered v k, Ob n) =>
(a ~> b) -> (a ^ n) ~> (b ^ n)
mapBase a ~> b
f =
  a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => (a ^ n) ~> (b ^ n)) -> (a ^ n) ~> (b ^ n)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
    forall v k (a :: k) (n :: v) r.
(Powered v k, Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @v @k @a @n
      ( forall v k (a :: k) (b :: k) (n :: v).
(Powered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power @v @k @(a ^ n) @b @n
          (let g :: n ~> HomObj v (a ^ n) a
g = forall v k (b :: k) (n :: v) (a :: k).
(Powered v k, Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower @v @k @a @n (a ^ n) ~> (a ^ n)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id in n ~> HomObj v (a ^ n) a
g (n ~> HomObj v (a ^ n) a)
-> ((Ob n, Ob (HomObj v (a ^ n) a)) => n ~> HomObj v (a ^ n) b)
-> n ~> HomObj v (a ^ n) b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall v (a :: k) (b :: k) (c :: k).
(Enriched v k, Ob a, Ob b, Ob c) =>
(HomObj v b c ** HomObj v a b) ~> HomObj v a c
forall {k} v (a :: k) (b :: k) (c :: k).
(Enriched v k, Ob a, Ob b, Ob c) =>
(HomObj v b c ** HomObj v a b) ~> HomObj v a c
comp @v @(a ^ n) @a @b ((HomObj v a b ** HomObj v (a ^ n) a) ~> HomObj v (a ^ n) b)
-> (n ~> (HomObj v a b ** HomObj v (a ^ n) a))
-> n ~> HomObj v (a ^ n) b
forall (b :: v) (c :: v) (a :: v). (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
. (Unit ~> HomObj v a b)
-> HomObj v (a ^ n) a ~> (HomObj v a b ** HomObj v (a ^ n) a)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
forall v (p :: k +-> k) (a :: k) (b :: k).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
underlying @v a ~> b
f) (HomObj v (a ^ n) a ~> (HomObj v a b ** HomObj v (a ^ n) a))
-> (n ~> HomObj v (a ^ n) a)
-> n ~> (HomObj v a b ** HomObj v (a ^ n) a)
forall (b :: v) (c :: v) (a :: v). (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
. n ~> HomObj v (a ^ n) a
g)
      )

mapPower :: forall {k} {v} (a :: k) (n :: v) m. (Powered v k, Ob a) => (n ~> m) -> a ^ m ~> a ^ n
mapPower :: forall {k} {v} (a :: k) (n :: v) (m :: v).
(Powered v k, Ob a) =>
(n ~> m) -> (a ^ m) ~> (a ^ n)
mapPower n ~> m
f = forall v k (a :: k) (n :: v) r.
(Powered v k, Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @v @k @a @m (forall v k (a :: k) (b :: k) (n :: v).
(Powered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power @v @k @(a ^ m) @a @n (forall v k (b :: k) (n :: v) (a :: k).
(Powered v k, Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower @v @k @a (a ^ m) ~> (a ^ m)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (m ~> HomObj v (a ^ m) a) -> (n ~> m) -> n ~> HomObj v (a ^ m) a
forall (b :: v) (c :: v) (a :: v). (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
. n ~> m
f)) ((Ob n, Ob m) => (a ^ m) ~> (a ^ n))
-> (n ~> m) -> (a ^ m) ~> (a ^ n)
forall (a :: v) (b :: v) r. ((Ob a, Ob b) => r) -> (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
\\ n ~> m
f

instance Powered Type Type where
  type a ^ n = n ~~> a
  withObPower :: forall a n r. (Ob a, Ob n) => (Ob (a ^ n) => r) -> r
withObPower Ob (a ^ n) => r
r = r
Ob (a ^ n) => r
r
  power :: forall a b n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> a ~> (b ^ n)
power n ~> HomObj Type a b
f a
a n
n = n ~> HomObj Type a b
n -> (a -> b)
f n
n a
a
  unpower :: forall b n a.
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj Type a b
unpower a ~> (b ^ n)
f n
n a
a = a ~> (b ^ n)
a -> (n -> b)
f a
a n
n

instance (Enriched v (), Closed v, HomObj v '() '() ~ TerminalObject, Cartesian v) => Powered v () where
  type a ^ n = '()
  withObPower :: forall (a :: ()) (n :: v) r. (Ob a, Ob n) => (Ob (a ^ n) => r) -> r
withObPower Ob (a ^ n) => r
r = r
Ob (a ^ n) => r
r
  power :: forall (a :: ()) (b :: ()) (n :: v).
(Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power n ~> HomObj v a b
_ = a ~> (b ^ n)
Unit '() '()
U.Unit
  unpower :: forall (b :: ()) (n :: v) (a :: ()).
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower a ~> (b ^ n)
Unit a '()
U.Unit = n ~> TerminalObject
n ~> ProObj v (~>) a b
forall (a :: v). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

class (HomObj v '(a1, a2) '(b1, b2) ~ (HomObj v a1 b1 && HomObj v a2 b2)) => HomObjIsProduct v a1 a2 b1 b2
instance (HomObj v '(a1, a2) '(b1, b2) ~ (HomObj v a1 b1 && HomObj v a2 b2)) => HomObjIsProduct v a1 a2 b1 b2
instance
  ( Powered v j
  , Powered v k
  , Enriched v (j, k)
  , forall (a :: (j, k)) (b :: (j, k)) a1 a2 b1 b2
     . (Ob a, a ~ '(a1, a2), Ob b, b ~ '(b1, b2)) => HomObjIsProduct v a1 a2 b1 b2
  , Cartesian v
  )
  => Powered v (j, k)
  where
  type '(a1, a2) ^ n = '(a1 ^ n, a2 ^ n)
  withObPower :: forall (a :: (j, k)) (n :: v) r.
(Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @'(a, b) @n Ob (a ^ n) => r
r = forall v k (a :: k) (n :: v) r.
(Powered v k, Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @v @j @a @n (forall v k (a :: k) (n :: v) r.
(Powered v k, Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @v @k @b @n r
Ob (Snd a ^ n) => r
Ob (a ^ n) => r
r)
  power :: forall (a :: (j, k)) (b :: (j, k)) (n :: v).
(Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power @'(a1, a2) @'(b1, b2) n ~> HomObj v a b
f =
    forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: j +-> j) (a :: j) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(~>) @a1 @b1 ((Ob (ProObj v (~>) (Fst a) (Fst b)) => a ~> (b ^ n))
 -> a ~> (b ^ n))
-> (Ob (ProObj v (~>) (Fst a) (Fst b)) => a ~> (b ^ n))
-> a ~> (b ^ n)
forall a b. (a -> b) -> a -> b
$
      forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: k +-> k) (a :: k) (b :: k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @(~>) @a2 @b2 ((Ob (ProObj v (~>) (Snd a) (Snd b)) => a ~> (b ^ n))
 -> a ~> (b ^ n))
-> (Ob (ProObj v (~>) (Snd a) (Snd b)) => a ~> (b ^ n))
-> a ~> (b ^ n)
forall a b. (a -> b) -> a -> b
$
        forall v k (a :: k) (b :: k) (n :: v).
(Powered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power @v @j @a1 @b1 (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @(HomObj v a1 b1) @(HomObj v a2 b2) ((ProObj v (~>) (Fst a) (Fst b) && ProObj v (~>) (Snd a) (Snd b))
 ~> ProObj v (~>) (Fst a) (Fst b))
-> (n
    ~> (ProObj v (~>) (Fst a) (Fst b)
        && ProObj v (~>) (Snd a) (Snd b)))
-> n ~> ProObj v (~>) (Fst a) (Fst b)
forall (b :: v) (c :: v) (a :: v). (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
. n
~> (ProObj v (~>) (Fst a) (Fst b) && ProObj v (~>) (Snd a) (Snd b))
n ~> HomObj v a b
f)
          (Fst a ~> (Fst b ^ n))
-> (Snd a ~> (Snd b ^ n))
-> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b ^ n, Snd b ^ n)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall v k (a :: k) (b :: k) (n :: v).
(Powered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power @v @k @a2 @b2 (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(HomObj v a1 b1) @(HomObj v a2 b2) ((ProObj v (~>) (Fst a) (Fst b) && ProObj v (~>) (Snd a) (Snd b))
 ~> ProObj v (~>) (Snd a) (Snd b))
-> (n
    ~> (ProObj v (~>) (Fst a) (Fst b)
        && ProObj v (~>) (Snd a) (Snd b)))
-> n ~> ProObj v (~>) (Snd a) (Snd b)
forall (b :: v) (c :: v) (a :: v). (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
. n
~> (ProObj v (~>) (Fst a) (Fst b) && ProObj v (~>) (Snd a) (Snd b))
n ~> HomObj v a b
f)
  unpower :: forall (b :: (j, k)) (n :: v) (a :: (j, k)).
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower @'(b1, b2) @n (a1 ~> b1
f :**: a2 ~> b2
g) = forall v k (b :: k) (n :: v) (a :: k).
(Powered v k, Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower @v @j @b1 @n a1 ~> b1
a1 ~> (Fst b ^ n)
f (n ~> ProObj v (~>) a1 (Fst b))
-> (n ~> ProObj v (~>) a2 (Snd b))
-> n ~> (ProObj v (~>) a1 (Fst b) && ProObj v (~>) a2 (Snd b))
forall (a :: v) (x :: v) (y :: v).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& forall v k (b :: k) (n :: v) (a :: k).
(Powered v k, Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower @v @k @b2 @n a2 ~> b2
a2 ~> (Snd b ^ n)
g ((Ob a1, Ob b1) =>
 n ~> ProObj v ((~>) :**: (~>)) '(a1, a2) '(Fst b, Snd b))
-> (a1 ~> b1)
-> n ~> ProObj v ((~>) :**: (~>)) '(a1, a2) '(Fst b, Snd b)
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (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
\\ a1 ~> b1
f ((Ob a2, Ob b2) =>
 n ~> ProObj v ((~>) :**: (~>)) '(a1, a2) '(Fst b, Snd b))
-> (a2 ~> b2)
-> n ~> ProObj v ((~>) :**: (~>)) '(a1, a2) '(Fst b, Snd b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a2 ~> b2
g

data (p :^: n) a b where
  Power :: (Ob a, Ob b) => {forall {k} {k} (a :: k) (b :: k) n (p :: k -> k -> Type).
(:^:) p n a b -> n -> p a b
unPower :: n -> p a b} -> (p :^: n) a b
instance (Profunctor p) => Profunctor (p :^: n) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> (:^:) p n a b -> (:^:) p n c d
dimap c ~> a
l b ~> d
r (Power n -> p a b
f) = c ~> a
l (c ~> a) -> ((Ob c, Ob a) => (:^:) p n c d) -> (:^:) p n 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 n c d) -> (:^:) p n c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (n -> p c d) -> (:^:) p n c d
forall {k} {k} (a :: k) (b :: k) n (p :: k -> k -> Type).
(Ob a, Ob b) =>
(n -> p a b) -> (:^:) p n a b
Power \n
n -> (c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p 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
l b ~> d
r (n -> p a b
f n
n)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> (:^:) p n a b -> r
\\ Power{} = r
(Ob a, Ob b) => r
r
instance (CategoryOf j, CategoryOf k) => Powered Type (j +-> k) where
  type a ^ n = a :^: n
  withObPower :: forall (a :: j +-> k) n r. (Ob a, Ob n) => (Ob (a ^ n) => r) -> r
withObPower Ob (a ^ n) => r
r = r
Ob (a ^ n) => r
r
  power :: forall (a :: j +-> k) (b :: j +-> k) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> a ~> (b ^ n)
power n ~> HomObj Type a b
f = (a :~> (b :^: n)) -> Prof a (b :^: n)
forall {j} {k} (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) => (:^:) b n a b) -> (:^:) b n a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (n -> b a b) -> (:^:) b n a b
forall {k} {k} (a :: k) (b :: k) n (p :: k -> k -> Type).
(Ob a, Ob b) =>
(n -> p a b) -> (:^:) p n a b
Power \n
n -> Prof a b -> a :~> b
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf (n ~> HomObj Type a b
n -> Prof a b
f n
n) a a b
p
  unpower :: forall (b :: j +-> k) n (a :: j +-> k).
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj Type a b
unpower (Prof a :~> (b :^: n)
f) n
n = (a :~> b) -> Prof a b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> (:^:) b n a b -> n -> b a b
forall {k} {k} (a :: k) (b :: k) n (p :: k -> k -> Type).
(:^:) p n a b -> n -> p a b
unPower (a a b -> (:^:) b n a b
a :~> (b :^: n)
f a a b
p) n
n