{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Power where

import Data.Kind (Type)

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Core (CategoryOf (..), Ob, Profunctor (..), Promonad (..), (//), type (+->))

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

mapBase :: forall k a b n. (Powered k) => (a :: k) ~> b -> a ^ n ~> b ^ n
mapBase :: forall k (a :: k) (b :: k) n.
Powered k =>
(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 k (a :: k) n r. (Powered k, Ob a) => (Ob (a ^ n) => r) -> r
withObPower @k @a @n (forall k (a :: k) (b :: k) n.
(Powered k, Ob a, Ob b) =>
(n -> a ~> b) -> a ~> (b ^ n)
power @k @(a ^ n) @b @n (\n
n -> a ~> b
f (a ~> b) -> ((a ^ n) ~> a) -> (a ^ n) ~> b
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
. ((a ^ n) ~> (a ^ n)) -> n -> (a ^ n) ~> a
forall (b :: k) (a :: k) n. Ob b => (a ~> (b ^ n)) -> n -> a ~> b
forall k (b :: k) (a :: k) n.
(Powered k, Ob b) =>
(a ~> (b ^ n)) -> n -> a ~> b
unpower (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 n
n))

mapPower :: forall k a n m. (Powered k, Ob (a :: k)) => (n -> m) -> a ^ m ~> a ^ n
mapPower :: forall k (a :: k) n m.
(Powered k, Ob a) =>
(n -> m) -> (a ^ m) ~> (a ^ n)
mapPower n -> m
f = forall k (a :: k) n r. (Powered k, Ob a) => (Ob (a ^ n) => r) -> r
withObPower @k @a @m (forall k (a :: k) (b :: k) n.
(Powered k, Ob a, Ob b) =>
(n -> a ~> b) -> a ~> (b ^ n)
power @k @(a ^ m) @a @n (\n
n -> ((a ^ m) ~> (a ^ m)) -> m -> (a ^ m) ~> a
forall (b :: k) (a :: k) n. Ob b => (a ~> (b ^ n)) -> n -> a ~> b
forall k (b :: k) (a :: k) n.
(Powered k, Ob b) =>
(a ~> (b ^ n)) -> n -> a ~> b
unpower (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 (n -> m
f n
n)))

instance Powered Type where
  type a ^ n = n -> a
  withObPower :: forall a n r. Ob a => (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 -> a ~> b) -> a ~> (b ^ n)
power n -> a ~> b
f a
a n
n = n -> a ~> b
f n
n a
a
  unpower :: forall b a n. Ob b => (a ~> (b ^ n)) -> n -> a ~> b
unpower a ~> (b ^ n)
f n
n a
a = a ~> (b ^ n)
a -> (n -> b)
f a
a n
n

instance Powered () where
  type a ^ n = '()
  withObPower :: forall (a :: ()) n r. Ob a => (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 -> a ~> b) -> a ~> (b ^ n)
power n -> a ~> b
_ = a ~> (b ^ n)
Unit '() '()
Unit
  unpower :: forall (b :: ()) (a :: ()) n. Ob b => (a ~> (b ^ n)) -> n -> a ~> b
unpower a ~> (b ^ n)
Unit a '()
Unit n
_ = a ~> b
Unit '() '()
Unit

instance (Powered j, Powered k) => Powered (j, k) where
  type '(a, b) ^ n = '(a ^ n, b ^ n)
  withObPower :: forall (a :: (j, k)) n r. Ob a => (Ob (a ^ n) => r) -> r
withObPower @'(a, b) @n Ob (a ^ n) => r
r = forall k (a :: k) n r. (Powered k, Ob a) => (Ob (a ^ n) => r) -> r
withObPower @j @a @n (forall k (a :: k) n r. (Powered k, Ob a) => (Ob (a ^ n) => r) -> r
withObPower @k @b @n r
Ob (Snd a ^ n) => r
Ob (a ^ n) => r
r)
  power :: forall (a :: (j, k)) (b :: (j, k)) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> a ~> (b ^ n)
power n -> a ~> b
f = forall k (a :: k) (b :: k) n.
(Powered k, Ob a, Ob b) =>
(n -> a ~> b) -> a ~> (b ^ n)
power @j (\n
n -> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b, Snd b) -> Fst a ~> Fst b
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
(:**:) c d '(a1, a2) '(b1, b2) -> c a1 b1
fstK (n -> a ~> b
f n
n)) (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 k (a :: k) (b :: k) n.
(Powered k, Ob a, Ob b) =>
(n -> a ~> b) -> a ~> (b ^ n)
power @k (\n
n -> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b, Snd b) -> Snd a ~> Snd b
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
(:**:) c d '(a1, a2) '(b1, b2) -> d a2 b2
sndK (n -> a ~> b
f n
n))
  unpower :: forall (b :: (j, k)) (a :: (j, k)) n.
Ob b =>
(a ~> (b ^ n)) -> n -> a ~> b
unpower (a1 ~> b1
f :**: a2 ~> b2
g) n
n = (a1 ~> (Fst b ^ n)) -> n -> a1 ~> Fst b
forall (b :: j) (a :: j) n. Ob b => (a ~> (b ^ n)) -> n -> a ~> b
forall k (b :: k) (a :: k) n.
(Powered k, Ob b) =>
(a ~> (b ^ n)) -> n -> a ~> b
unpower a1 ~> b1
a1 ~> (Fst b ^ n)
f n
n (a1 ~> Fst b)
-> (a2 ~> Snd b) -> (:**:) (~>) (~>) '(a1, a2) '(Fst b, Snd b)
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)
:**: (a2 ~> (Snd b ^ n)) -> n -> a2 ~> Snd b
forall (b :: k) (a :: k) n. Ob b => (a ~> (b ^ n)) -> n -> a ~> b
forall k (b :: k) (a :: k) n.
(Powered k, Ob b) =>
(a ~> (b ^ n)) -> n -> a ~> b
unpower a2 ~> b2
a2 ~> (Snd b ^ n)
g n
n

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 (j +-> k) where
  type a ^ n = a :^: n
  withObPower :: forall (a :: j +-> k) n r. Ob a => (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 -> a ~> b) -> a ~> (b ^ n)
power n -> 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 -> a ~> b
f n
n) a a b
p
  unpower :: forall (b :: j +-> k) (a :: j +-> k) n.
Ob b =>
(a ~> (b ^ n)) -> n -> 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