{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Corepresentable where

import Data.Kind (Constraint)

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->), Iso, iso)
import Proarrow.Object (obj, Obj)
import Proarrow.Functor (FunctorForRep (..))

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

instance Corepresentable (->) where
  type (->) %% a = a
  coindex :: forall a b. (a -> b) -> ((->) %% a) ~> b
coindex a -> b
f = ((->) %% a) ~> b
a -> b
f
  cotabulate :: forall a b. Ob a => (((->) %% a) ~> b) -> a -> b
cotabulate ((->) %% a) ~> b
f = ((->) %% a) ~> b
a -> b
f
  corepMap :: forall a b. (a ~> b) -> ((->) %% a) ~> ((->) %% b)
corepMap a ~> b
f = a ~> b
((->) %% a) ~> ((->) %% b)
f

corepObj :: forall p a. (Corepresentable p, Ob a) => Obj (p %% a)
corepObj :: forall {k} {k} (p :: k +-> k) (a :: k).
(Corepresentable p, Ob a) =>
Obj (p %% a)
corepObj = 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)

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

trivialCorep :: forall p a. (Corepresentable p, Ob a) => p a (p %% a)
trivialCorep :: forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep = ((p %% a) ~> (p %% a)) -> p a (p %% a)
forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (forall {k} {k} (p :: k +-> k) (a :: k).
(Corepresentable p, Ob a) =>
Obj (p %% a)
forall (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
Obj (p %% a)
corepObj @p @a)

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

corep :: forall f a b a' b'. Ob a => Iso (f @ a ~> b) (f @ a' ~> b') (Corep f a b) (Corep f a' b')
corep :: forall {j} {k} (f :: j +-> k) (a :: j) (b :: k) (a' :: j)
       (b' :: k).
Ob a =>
Iso ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b')
corep = (((f @ a) ~> b) ~> Corep f a b)
-> (Corep f a' b' ~> ((f @ a') ~> b'))
-> Iso
     ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b')
forall {k1} {k2} (s :: k1) (a :: k1) (b :: k2) (t :: k2).
(s ~> a) -> (b ~> t) -> Iso s t a b
iso ((f @ a) ~> b) ~> Corep f a b
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (f :: j +-> k) (a :: j) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep Corep f a' b' ~> ((f @ a') ~> b')
Corep f a' b' -> (f @ a') ~> b'
forall {j} {k} (f :: j +-> k) (a :: j) (b :: k).
Corep f a b -> (f @ a) ~> b
unCorep

type Comonad w = (Promonad w, Corepresentable w)

extract :: forall w a. (Comonad w, Ob a) => w %% a ~> a
extract :: forall {k} (w :: k +-> k) (a :: k).
(Comonad w, Ob a) =>
(w %% a) ~> a
extract = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: k +-> k) (a :: k) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @w w a a
forall (a :: k). Ob a => w a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

extend :: forall w a b. (Comonad w, Ob a) => (w %% a ~> b) -> (w %% a ~> w %% b)
extend :: forall {j} (w :: j +-> j) (a :: j) (b :: j).
(Comonad w, Ob a) =>
((w %% a) ~> b) -> (w %% a) ~> (w %% b)
extend (w %% a) ~> b
f = w a (w %% b) -> (w %% a) ~> (w %% b)
forall (a :: j) (b :: j). w a b -> (w %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex ((w b (w %% b)
(Ob (w %% a), Ob b) => w b (w %% b)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep ((Ob (w %% a), Ob b) => w b (w %% b))
-> ((w %% a) ~> b) -> w b (w %% b)
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
\\ (w %% a) ~> b
f) w b (w %% b) -> w a b -> w a (w %% b)
forall (b :: j) (c :: j) (a :: j). w b c -> w a b -> w a c
forall {k} (p :: 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 :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (p :: j +-> j) (a :: j) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate @w @a (w %% a) ~> b
f)