{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Representable where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (:~>), type (+->))
import Proarrow.Object (Obj, obj)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), dimapCorep)
import Proarrow.Category.Enriched.ThinCategory (ThinProfunctor (..), Discrete, withEq, Thin)

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

instance Representable (->) where
  type (->) % a = a
  index :: forall a b. (a -> b) -> a ~> ((->) % b)
index a -> b
f = a ~> ((->) % b)
a -> b
f
  tabulate :: forall b a. Ob b => (a ~> ((->) % b)) -> a -> b
tabulate a ~> ((->) % b)
f = a ~> ((->) % b)
a -> b
f
  repMap :: forall a b. (a ~> b) -> ((->) % a) ~> ((->) % b)
repMap a ~> b
f = a ~> b
((->) % a) ~> ((->) % b)
f

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)

withRepOb :: forall p a r. (Representable p, Ob a) => ((Ob (p % a)) => r) -> r
withRepOb :: forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb 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 :: j +-> k) (a :: k) (b :: j) 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 :: 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 :: 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 (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 :: 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r

trivialRep :: forall p a. (Representable p, Ob a) => p (p % a) a
trivialRep :: forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep = ((p % a) ~> (p % a)) -> p (p % a) a
forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (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)

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 :: k) (a :: k) (b :: j) (d :: j).
(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 :: k) (b :: j) 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 :: 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
\\ 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 :: k) (a :: k) (b :: j) (d :: j).
(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 :: k) (b :: j) 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 :: 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
\\ (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
instance (Representable p, Discrete j, Thin k) => ThinProfunctor (RepCostar p :: j +-> k) where
  type HasArrow (RepCostar p) a b = (p % a) ~ b
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (RepCostar p) a b) =>
RepCostar p a b
arr = ((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 b ~> b
(p % a) ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  withArr :: forall (a :: k) (b :: j) r.
RepCostar p a b -> (HasArrow (RepCostar p) a b => r) -> r
withArr (RepCostar (p % a) ~> b
f) HasArrow (RepCostar p) a b => r
r = ((p % a) ~> b) -> (((p % a) ~ b) => r) -> r
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 (p % a) ~> b
f r
((p % a) ~ b) => r
HasArrow (RepCostar p) a b => r
r

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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (q %% b)
q)

-- | A perfectly valid functor definition, but hard to use.
-- So we only use it to easily make representable profunctors with @Rep@.
type FunctorForRep :: forall {j} {k}. (j +-> k) -> Constraint
class (CategoryOf j, CategoryOf k) => FunctorForRep (f :: j +-> k) where
  type f @ (a :: j) :: k
  fmap :: (a ~> b) -> f @ a ~> f @ b

type Rep :: (j +-> k) -> j +-> k
data Rep f a b where
  Rep :: forall f a b. (Ob b) => {forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Rep f a b -> a ~> (f @ b)
unRep :: a ~> f @ b} -> Rep f a b
instance (FunctorForRep f) => Profunctor (Rep f) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Rep f a b -> Rep f c d
dimap = (c ~> a) -> (b ~> d) -> Rep f a b -> Rep f 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 :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Rep f a b -> r
\\ Rep a ~> (f @ b)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (f @ b)) => r
r ((Ob a, Ob (f @ b)) => r) -> (a ~> (f @ b)) -> r
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
\\ a ~> (f @ b)
f
instance (FunctorForRep f) => Representable (Rep f) where
  type Rep f % a = f @ a
  index :: forall (a :: k) (b :: j). Rep f a b -> a ~> (Rep f % b)
index (Rep a ~> (f @ b)
f) = a ~> (f @ b)
a ~> (Rep f % b)
f
  tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (Rep f % b)) -> Rep f a b
tabulate = (a ~> (f @ b)) -> Rep f a b
(a ~> (Rep f % b)) -> Rep f a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep
  repMap :: forall (a :: j) (b :: j). (a ~> b) -> (Rep f % a) ~> (Rep f % b)
repMap = forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @f