{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Corepresentable where

import Data.Kind (Constraint)

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Object (obj)

infixl 8 %%

type Corepresentable :: forall {j} {k}. (j +-> k) -> Constraint
class (Profunctor p) => Corepresentable (p :: j +-> k) where
  type p %% (a :: k) :: j
  coindex :: p a b -> p %% a ~> b
  cotabulate :: (Ob a) => (p %% a ~> b) -> p a b
  corepMap :: (a ~> b) -> p %% a ~> p %% b

withCorepObj :: forall p a r. (Corepresentable p, Ob a) => ((Ob (p %% a)) => r) -> r
withCorepObj :: forall {k} {k} (p :: k +-> k) (a :: k) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withCorepObj 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 :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: k +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

dimapCorep :: forall p a b c d. (Corepresentable p) => (c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep :: 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 c ~> a
l b ~> d
r = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate @p (((p %% c) ~> d) -> p c d)
-> (p a b -> (p %% c) ~> 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
. ((p %% c) ~> (p %% a))
-> (b ~> d) -> ((p %% a) ~> b) -> (p %% c) ~> 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 (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p c ~> a
l) b ~> d
r (((p %% a) ~> b) -> (p %% c) ~> d)
-> (p a b -> (p %% a) ~> b) -> 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
. p a b -> (p %% a) ~> b
forall (a :: k) (b :: j). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex ((Ob c, Ob a) => p a b -> p c d) -> (c ~> a) -> 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
\\ c ~> a
l

type Corep :: (j +-> k) -> (j +-> k)
data Corep p a b where
  Corep :: Ob a => { forall {k} {k} (a :: k) (p :: k +-> k) (b :: k).
Corep p a b -> (p %% a) ~> b
getCorep :: p %% a ~> b } -> Corep p a b
instance (Corepresentable p) => Profunctor (Corep p) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Corep p a b -> Corep p c d
dimap c ~> a
f b ~> d
g (Corep (p %% a) ~> b
h) = ((p %% c) ~> d) -> Corep p c d
forall {k} {k} (a :: k) (p :: k +-> k) (b :: k).
Ob a =>
((p %% a) ~> b) -> Corep p a b
Corep (b ~> d
g (b ~> d) -> ((p %% c) ~> b) -> (p %% c) ~> d
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
. (p %% a) ~> b
h ((p %% a) ~> b) -> ((p %% c) ~> (p %% a)) -> (p %% c) ~> 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
. 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 c ~> a
f) ((Ob c, Ob a) => Corep p c d) -> (c ~> a) -> Corep 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
\\ c ~> a
f
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> Corep p a b -> r
\\ Corep (p %% a) ~> b
f = r
(Ob (p %% a), Ob b) => r
(Ob 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 (Corepresentable p) => Corepresentable (Corep p) where
  type Corep p %% a = p %% a
  coindex :: forall (a :: k) (b :: j). Corep p a b -> (Corep p %% a) ~> b
coindex (Corep (p %% a) ~> b
f) = (p %% a) ~> b
(Corep p %% a) ~> b
f
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((Corep p %% a) ~> b) -> Corep p a b
cotabulate = ((p %% a) ~> b) -> Corep p a b
((Corep p %% a) ~> b) -> Corep p a b
forall {k} {k} (a :: k) (p :: k +-> k) (b :: k).
Ob a =>
((p %% a) ~> b) -> Corep p a b
Corep
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Corep p %% a) ~> (Corep p %% b)
corepMap = forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p