{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Copower 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 copowered over Hask.
class (CategoryOf k) => Copowered k where
  type (n :: Type) *. (a :: k) :: k
  withObCopower :: (Ob (a :: k)) => ((Ob (n *. a)) => r) -> r
  copower :: (Ob (a :: k), Ob b) => (n -> a ~> b) -> (n *. a) ~> b
  uncopower :: (Ob (a :: k)) => (n *. a) ~> b -> n -> a ~> b

mapCobase :: forall k a b n. (Copowered k) => (a :: k) ~> b -> n *. a ~> n *. b
mapCobase :: forall k (a :: k) (b :: k) n.
Copowered k =>
(a ~> b) -> (n *. a) ~> (n *. b)
mapCobase a ~> b
f = a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => (n *. a) ~> (n *. b)) -> (n *. 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 k (a :: k) n r.
(Copowered k, Ob a) =>
(Ob (n *. a) => r) -> r
withObCopower @k @b @n (forall k (a :: k) (b :: k) n.
(Copowered k, Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower @k @a @(n *. b) @n (\n
n -> ((n *. b) ~> (n *. b)) -> n -> b ~> (n *. b)
forall (a :: k) n (b :: k). Ob a => ((n *. a) ~> b) -> n -> a ~> b
forall k (a :: k) n (b :: k).
(Copowered k, Ob a) =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (n *. b) ~> (n *. b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id n
n (b ~> (n *. b)) -> (a ~> b) -> 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 ~> b
f))

mapCopower :: forall k a n m. (Copowered k, Ob (a :: k)) => (n -> m) -> n *. a ~> m *. a
mapCopower :: forall k (a :: k) n m.
(Copowered k, Ob a) =>
(n -> m) -> (n *. a) ~> (m *. a)
mapCopower n -> m
f = forall k (a :: k) n r.
(Copowered k, Ob a) =>
(Ob (n *. a) => r) -> r
withObCopower @k @a @m (forall k (a :: k) (b :: k) n.
(Copowered k, Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower @k @a @(m *. a) @n (\n
m -> ((m *. a) ~> (m *. a)) -> m -> a ~> (m *. a)
forall (a :: k) n (b :: k). Ob a => ((n *. a) ~> b) -> n -> a ~> b
forall k (a :: k) n (b :: k).
(Copowered k, Ob a) =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (m *. a) ~> (m *. a)
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
m)))

instance Copowered Type where
  type n *. a = (n, a)
  withObCopower :: forall a n r. Ob a => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall a b n. (Ob a, Ob b) => (n -> a ~> b) -> (n *. a) ~> b
copower n -> a ~> b
f = \(n
n, a
a) -> n -> a ~> b
f n
n a
a
  uncopower :: forall a n b. Ob a => ((n *. a) ~> b) -> n -> a ~> b
uncopower (n *. a) ~> b
f n
n a
a = (n *. a) ~> b
(n, a) -> b
f (n
n, a
a)

instance Copowered () where
  type n *. a = '()
  withObCopower :: forall (a :: ()) n r. Ob a => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall (a :: ()) (b :: ()) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower n -> a ~> b
_ = (n *. a) ~> b
Unit '() '()
Unit
  uncopower :: forall (a :: ()) n (b :: ()).
Ob a =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (n *. a) ~> b
Unit '() b
Unit n
_ = a ~> b
Unit '() '()
Unit

instance (Copowered j, Copowered k) => Copowered (j, k) where
  type (n :: Type) *. '(a, b) = '(n *. a, n *. b)
  withObCopower :: forall (a :: (j, k)) n r. Ob a => (Ob (n *. a) => r) -> r
withObCopower @'(a, b) @n Ob (n *. a) => r
r = forall k (a :: k) n r.
(Copowered k, Ob a) =>
(Ob (n *. a) => r) -> r
withObCopower @j @a @n (forall k (a :: k) n r.
(Copowered k, Ob a) =>
(Ob (n *. a) => r) -> r
withObCopower @k @b @n r
Ob (n *. Snd a) => r
Ob (n *. a) => r
r)
  copower :: forall (a :: (j, k)) (b :: (j, k)) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower n -> a ~> b
f = forall k (a :: k) (b :: k) n.
(Copowered k, Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower @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)) ((n *. Fst a) ~> Fst b)
-> ((n *. Snd a) ~> Snd b)
-> (:**:) (~>) (~>) '(n *. Fst a, n *. Snd a) '(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)
:**: forall k (a :: k) (b :: k) n.
(Copowered k, Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower @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))
  uncopower :: forall (a :: (j, k)) n (b :: (j, k)).
Ob a =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (a1 ~> b1
f :**: a2 ~> b2
g) n
n = ((n *. Fst a) ~> b1) -> n -> Fst a ~> b1
forall (a :: j) n (b :: j). Ob a => ((n *. a) ~> b) -> n -> a ~> b
forall k (a :: k) n (b :: k).
(Copowered k, Ob a) =>
((n *. a) ~> b) -> n -> a ~> b
uncopower a1 ~> b1
(n *. Fst a) ~> b1
f n
n (Fst a ~> b1)
-> (Snd a ~> b2) -> (:**:) (~>) (~>) '(Fst a, Snd a) '(b1, b2)
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)
:**: ((n *. Snd a) ~> b2) -> n -> Snd a ~> b2
forall (a :: k) n (b :: k). Ob a => ((n *. a) ~> b) -> n -> a ~> b
forall k (a :: k) n (b :: k).
(Copowered k, Ob a) =>
((n *. a) ~> b) -> n -> a ~> b
uncopower a2 ~> b2
(n *. Snd a) ~> b2
g n
n

data (n :*.: p) a b where
  Copower :: n -> p a b -> (n :*.: p) a b
instance (Profunctor p) => Profunctor (n :*.: p) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> (:*.:) n p a b -> (:*.:) n p c d
dimap c ~> a
l b ~> d
r (Copower n
n p a b
p) = n -> p c d -> (:*.:) n p c d
forall {k} {k} n (p :: k -> k -> Type) (a :: k) (b :: k).
n -> p a b -> (:*.:) n p a b
Copower 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 p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> (:*.:) n p a b -> r
\\ Copower n
_ p a b
p = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p
instance (CategoryOf j, CategoryOf k) => Copowered (j +-> k) where
  type n *. a = n :*.: a
  withObCopower :: forall (a :: j +-> k) n r. Ob a => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall (a :: j +-> k) (b :: j +-> k) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower n -> a ~> b
f = ((n :*.: a) :~> b) -> Prof (n :*.: a) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Copower n
n a a b
p) -> 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
  uncopower :: forall (a :: j +-> k) n (b :: j +-> k).
Ob a =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (Prof (n :*.: a) :~> b
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 -> (:*.:) n a a b -> b a b
(n :*.: a) :~> b
f (n -> a a b -> (:*.:) n a a b
forall {k} {k} n (p :: k -> k -> Type) (a :: k) (b :: k).
n -> p a b -> (:*.:) n p a b
Copower n
n a a b
p)