{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Profunctor.Representable where

import Data.Kind (Constraint)

import Proarrow.Core (PRO, CategoryOf(..), Profunctor(..), Promonad(..))
import Proarrow.Object (obj)

infixl 8 %

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

withRepCod :: forall p a r. (Representable p, Ob a) => (Ob (p % a) => r) -> r
withRepCod :: forall {k} {k} (p :: PRO k k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepCod 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 :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO k k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @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 :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep c ~> a
l b ~> d
r = forall {j} {k} (p :: PRO j k) (b :: k) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: PRO j k) (b :: k) (a :: j).
(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 :: j) (a :: j) (b :: j) (d :: j).
(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 :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j k) (a :: k) (b :: k).
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 :: j) (b :: k). p a b -> a ~> (p % b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
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 :: 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
\\ b ~> d
r