{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Representable where

import Data.Kind (Constraint)

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->), (:~>))
import Proarrow.Object (Obj, obj)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), dimapCorep)

infixl 8 %

type Representable :: forall {j} {k}. j +-> k -> Constraint
class (Profunctor p) => Representable (p :: j +-> k) where
  type p % (a :: j) :: k
  index :: p a b -> a ~> p % b
  tabulate :: (Ob b) => (a ~> p % b) -> p a b
  repMap :: (a ~> b) -> p % a ~> p % b

repObj :: forall p a. (Representable p, Ob a) => Obj (p % a)
repObj :: forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

withRepObj :: forall p a r. (Representable p, Ob a) => ((Ob (p % a)) => r) -> r
withRepObj :: forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepObj Ob (p % a) => r
r = r
Ob (p % a) => r
(Ob (p % a), Ob (p % a)) => r
r ((Ob (p % a), Ob (p % a)) => r) -> ((p % a) ~> (p % a)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj @p @a

dimapRep :: forall p a b c d. (Representable p) => (c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep c ~> a
l b ~> d
r = forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p ((c ~> (p % d)) -> p c d)
-> (p a b -> c ~> (p % d)) -> p a b -> p c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> a) -> ((p % b) ~> (p % d)) -> (a ~> (p % b)) -> c ~> (p % d)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p b ~> d
r) ((a ~> (p % b)) -> c ~> (p % d))
-> (p a b -> a ~> (p % b)) -> p a b -> c ~> (p % d)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> a ~> (p % b)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((Ob b, Ob d) => p a b -> p c d) -> (b ~> d) -> p a b -> p c d
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r

type RepStar :: (j +-> k) -> (j +-> k)
data RepStar p a b where
  RepStar :: (Ob b) => {forall {j} {k} (b :: j) (a :: k) (p :: j +-> k).
RepStar p a b -> a ~> (p % b)
unRepStar :: a ~> p % b} -> RepStar p a b
instance (Representable p) => Profunctor (RepStar p) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> RepStar p a b -> RepStar p c d
dimap = (c ~> a) -> (b ~> d) -> RepStar p a b -> RepStar p c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> RepStar p a b -> r
\\ RepStar a ~> (p % b)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (p % b)) => r
r ((Ob a, Ob (p % b)) => r) -> (a ~> (p % b)) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (p % b)
f
instance (Representable p) => Representable (RepStar p) where
  type RepStar p % a = p % a
  index :: forall (a :: k) (b :: j). RepStar p a b -> a ~> (RepStar p % b)
index (RepStar a ~> (p % b)
f) = a ~> (p % b)
a ~> (RepStar p % b)
f
  tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (RepStar p % b)) -> RepStar p a b
tabulate = (a ~> (p % b)) -> RepStar p a b
(a ~> (RepStar p % b)) -> RepStar p a b
forall {j} {k} (b :: j) (a :: k) (p :: j +-> k).
Ob b =>
(a ~> (p % b)) -> RepStar p a b
RepStar
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (RepStar p % a) ~> (RepStar p % b)
repMap = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p

type CorepStar :: (k +-> j) -> (j +-> k)
data CorepStar p a b where
  CorepStar :: (Ob b) => {forall {k} {j} (b :: k) (a :: j) (p :: j +-> k).
CorepStar p a b -> a ~> (p %% b)
unCorepStar :: a ~> p %% b} -> CorepStar p a b
instance (Corepresentable p) => Profunctor (CorepStar p) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CorepStar p a b -> CorepStar p c d
dimap = (c ~> a) -> (b ~> d) -> CorepStar p a b -> CorepStar p c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> CorepStar p a b -> r
\\ CorepStar a ~> (p %% b)
f = r
(Ob a, Ob (p %% b)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (p %% b)) => r) -> (a ~> (p %% b)) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (p %% b)
f
instance (Corepresentable p) => Representable (CorepStar p) where
  type CorepStar p % a = p %% a
  index :: forall (a :: k) (b :: j). CorepStar p a b -> a ~> (CorepStar p % b)
index (CorepStar a ~> (p %% b)
f) = a ~> (p %% b)
a ~> (CorepStar p % b)
f
  tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (CorepStar p % b)) -> CorepStar p a b
tabulate = (a ~> (p %% b)) -> CorepStar p a b
(a ~> (CorepStar p % b)) -> CorepStar p a b
forall {k} {j} (b :: k) (a :: j) (p :: j +-> k).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (CorepStar p % a) ~> (CorepStar p % b)
repMap = forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: k +-> j) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p

type RepCostar :: (k +-> j) -> (j +-> k)
data RepCostar p a b where
  RepCostar :: (Ob a) => {forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
RepCostar p a b -> (p % a) ~> b
unRepCostar :: p % a ~> b} -> RepCostar p a b
instance (Representable p) => Profunctor (RepCostar p) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> RepCostar p a b -> RepCostar p c d
dimap = (c ~> a) -> (b ~> d) -> RepCostar p a b -> RepCostar p c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> RepCostar p a b -> r
\\ RepCostar (p % a) ~> b
f = r
(Ob a, Ob b) => r
(Ob (p % a), Ob b) => r
r ((Ob (p % a), Ob b) => r) -> ((p % a) ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (p % a) ~> b
f
instance (Representable p) => Corepresentable (RepCostar p) where
  type RepCostar p %% a = p % a
  coindex :: forall (a :: k) (b :: j).
RepCostar p a b -> (RepCostar p %% a) ~> b
coindex (RepCostar (p % a) ~> b
f) = (RepCostar p %% a) ~> b
(p % a) ~> b
f
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((RepCostar p %% a) ~> b) -> RepCostar p a b
cotabulate = ((RepCostar p %% a) ~> b) -> RepCostar p a b
((p % a) ~> b) -> RepCostar p a b
forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (RepCostar p %% a) ~> (RepCostar p %% b)
corepMap = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> j) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p

flipRep :: forall p q. (Representable p, Corepresentable q) => RepCostar p :~> q -> CorepStar q :~> p
flipRep :: forall {k1} {k} (p :: k1 +-> k) (q :: k +-> k1).
(Representable p, Corepresentable q) =>
(RepCostar p :~> q) -> CorepStar q :~> p
flipRep RepCostar p :~> q
n (CorepStar @b a ~> (q %% b)
q) = forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: k1 +-> k) (b :: k1) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: k +-> k1) (a :: k1) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @q @b (RepCostar p b (p % b) -> q b (p % b)
RepCostar p :~> q
n (((p % b) ~> (p % b)) -> RepCostar p b (p % b)
forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k1 +-> k) (a :: k1) (b :: k1).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall (a :: k1). (CategoryOf k1, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)))) ((q %% b) ~> (p % b)) -> (a ~> (q %% b)) -> a ~> (p % b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (q %% b)
q)