module Proarrow.Category.Instance.Graph where

import Prelude (type (~))

import Proarrow.Category.Enriched.Thin (CodiscreteProfunctor, ThinProfunctor (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, lmap, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Optic (Iso', iso)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Direp (Direp)
import Proarrow.Profunctor.Instance.Identity (Id)
import Proarrow.Profunctor.Representable (Rep (..))

type data GRAPH (p :: k +-> j) = GR j k

data family ProjJ :: forall (p :: k +-> j) -> GRAPH p +-> j
instance (ThinProfunctor p) => FunctorForRep (ProjJ p) where
  type (ProjJ p) @ GR x y = x
  fmap :: forall (a :: GRAPH p) (b :: GRAPH p).
(a ~> b) -> (ProjJ p @ a) ~> (ProjJ p @ b)
fmap (Graph aj ~> bj
l ak ~> bk
_) = aj ~> bj
(ProjJ p @ a) ~> (ProjJ p @ b)
l

data family ProjK :: forall (p :: k +-> j) -> GRAPH p +-> k
instance (ThinProfunctor p) => FunctorForRep (ProjK p) where
  type (ProjK p) @ GR x y = y
  fmap :: forall (a :: GRAPH p) (b :: GRAPH p).
(a ~> b) -> (ProjK p @ a) ~> (ProjK p @ b)
fmap (Graph aj ~> bj
_ ak ~> bk
r) = ak ~> bk
(ProjK p @ a) ~> (ProjK p @ b)
r

data Graph a b where
  Graph
    :: forall {p} aj ak bj bk
     . (HasArrow p aj ak, HasArrow p bj bk) => aj ~> bj -> ak ~> bk -> Graph (GR aj ak :: GRAPH p) (GR bj bk :: GRAPH p)
instance (ThinProfunctor p) => Profunctor (Graph :: CAT (GRAPH p)) where
  dimap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p) (d :: GRAPH p).
(c ~> a) -> (b ~> d) -> Graph a b -> Graph c d
dimap = (c ~> a) -> (b ~> d) -> Graph a b -> Graph c d
Graph c a -> Graph b d -> Graph a b -> Graph c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: GRAPH p) (b :: GRAPH p) r.
((Ob a, Ob b) => r) -> Graph a b -> r
\\ Graph aj ~> bj
f ak ~> bk
g = r
(Ob aj, Ob bj) => r
(Ob a, Ob b) => r
r ((Ob aj, Ob bj) => r) -> (aj ~> bj) -> 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
\\ aj ~> bj
f ((Ob ak, Ob bk) => r) -> (ak ~> bk) -> 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
\\ ak ~> bk
g
instance (ThinProfunctor p) => Promonad (Graph :: CAT (GRAPH p)) where
  id :: forall (a :: GRAPH p). Ob a => Graph a a
id = ((ProjJ p @ a) ~> (ProjJ p @ a))
-> ((ProjK p @ a) ~> (ProjK p @ a))
-> Graph
     (GR (ProjJ p @ a) (ProjK p @ a)) (GR (ProjJ p @ a) (ProjK p @ a))
forall {k} {k} {p :: k +-> k} (aj :: k) (ak :: k) (bj :: k)
       (bk :: k).
(HasArrow p aj ak, HasArrow p bj bk) =>
(aj ~> bj) -> (ak ~> bk) -> Graph (GR aj ak) (GR bj bk)
Graph (ProjJ p @ a) ~> (ProjJ p @ a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (ProjK p @ a) ~> (ProjK p @ a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  Graph aj ~> bj
f1 ak ~> bk
g1 . :: forall (b :: GRAPH p) (c :: GRAPH p) (a :: GRAPH p).
Graph b c -> Graph a b -> Graph a c
. Graph aj ~> bj
f2 ak ~> bk
g2 = (aj ~> bj) -> (ak ~> bk) -> Graph (GR aj ak) (GR bj bk)
forall {k} {k} {p :: k +-> k} (aj :: k) (ak :: k) (bj :: k)
       (bk :: k).
(HasArrow p aj ak, HasArrow p bj bk) =>
(aj ~> bj) -> (ak ~> bk) -> Graph (GR aj ak) (GR bj bk)
Graph (aj ~> bj
f1 (aj ~> bj) -> (aj ~> aj) -> aj ~> bj
forall (b :: j) (c :: j) (a :: j). (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
. aj ~> aj
aj ~> bj
f2) (ak ~> bk
g1 (ak ~> bk) -> (ak ~> ak) -> ak ~> bk
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
. ak ~> ak
ak ~> bk
g2)

-- | The graph of a thin profunctor. Doing this for any profunctor would need dependent types.
instance (ThinProfunctor p) => CategoryOf (GRAPH p) where
  type (~>) = Graph
  type
    Ob @(GRAPH p) ab =
      (ab ~ GR (ProjJ p @ ab) (ProjK p @ ab), Ob (ProjJ p @ ab), Ob (ProjK p @ ab), HasArrow p (ProjJ p @ ab) (ProjK p @ ab))

-- | A morphism gives two equal ways to compute the "diagonal", which is an element of the profunctor.
diagonalElement
  :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j) (bk :: k) r
   . (ThinProfunctor p) => GR aj ak ~> (GR bj bk :: GRAPH p) -> ((HasArrow p aj bk, Ob aj, Ob bk) => r) -> r
diagonalElement :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j)
       (bk :: k) r.
ThinProfunctor p =>
(GR aj ak ~> GR bj bk)
-> ((HasArrow p aj bk, Ob aj, Ob bk) => r) -> r
diagonalElement (Graph aj ~> bj
f ak ~> bk
g) = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (p :: k +-> j) (a :: j) (b :: k) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr @p @aj @bk ((aj ~> bj) -> p bj bk -> p aj bk
forall (c :: j) (a :: j) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap aj ~> bj
aj ~> bj
f (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: k +-> j) (a :: j) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @p @bj @bk) ((Ob aj, Ob bj) => p aj bk) -> (aj ~> bj) -> p aj bk
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
\\ aj ~> bj
aj ~> bj
f ((Ob ak, Ob bk) => p aj bk) -> (ak ~> bk) -> p aj bk
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
\\ ak ~> bk
ak ~> bk
g)

graphUniv :: forall {j} {k} (p :: k +-> j). (ThinProfunctor p) => Iso' p (Rep (ProjJ p) :.: Corep (ProjK p))
graphUniv :: forall {j} {k} (p :: k +-> j).
ThinProfunctor p =>
Iso' p (Rep (ProjJ p) :.: Corep (ProjK p))
graphUniv =
  (p ~> (Rep (ProjJ p) :.: Corep (ProjK p)))
-> ((Rep (ProjJ p) :.: Corep (ProjK p)) ~> p)
-> Iso
     p
     p
     (Rep (ProjJ p) :.: Corep (ProjK p))
     (Rep (ProjJ p) :.: Corep (ProjK p))
forall {j} {k} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso
    ((p :~> (Rep (ProjJ p) :.: Corep (ProjK p)))
-> Prof p (Rep (ProjJ p) :.: Corep (ProjK p))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \ @a @b p a b
p -> p a b
-> ((HasArrow p a b, Ob a, Ob b) =>
    (:.:) (Rep (ProjJ p)) (Corep (ProjK p)) a b)
-> (:.:) (Rep (ProjJ p)) (Corep (ProjK p)) a b
forall (a :: j) (b :: k) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr p a b
p (forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall (b :: GRAPH p) (f :: GRAPH p +-> j) (a :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @(GR a b) a ~> a
a ~> (ProjJ p @ GR a b)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Rep (ProjJ p) a (GR a b)
-> Corep (ProjK p) (GR a b) b
-> (:.:) (Rep (ProjJ p)) (Corep (ProjK p)) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((ProjK p @ GR a b) ~> b) -> Corep (ProjK p) (GR a b) b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep b ~> b
(ProjK p @ GR a b) ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))
    (((Rep (ProjJ p) :.: Corep (ProjK p)) :~> p)
-> Prof (Rep (ProjJ p) :.: Corep (ProjK p)) p
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rep a ~> (ProjJ p @ b)
l :.: Corep (ProjK p @ b) ~> b
r) -> (a ~> (ProjJ p @ b))
-> ((ProjK p @ b) ~> b) -> p (ProjJ p @ b) (ProjK p @ b) -> p a b
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p 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 a ~> (ProjJ p @ b)
l (ProjK p @ b) ~> b
r p (ProjJ p @ b) (ProjK p @ b)
forall (a :: j) (b :: k). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr)

data family ProdAsGraph :: (j, k) +-> GRAPH (p :: k +-> j)
instance (CategoryOf j, CategoryOf k, CodiscreteProfunctor p) => FunctorForRep (ProdAsGraph :: (j, k) +-> GRAPH (p :: k +-> j)) where
  type ProdAsGraph @ '(a, b) = GR a b
  fmap :: forall (a :: (j, k)) (b :: (j, k)).
(a ~> b) -> (ProdAsGraph @ a) ~> (ProdAsGraph @ b)
fmap (a1 ~> b1
l :**: a2 ~> b2
r) = (a1 ~> b1) -> (a2 ~> b2) -> Graph (GR a1 a2) (GR b1 b2)
forall {k} {k} {p :: k +-> k} (aj :: k) (ak :: k) (bj :: k)
       (bk :: k).
(HasArrow p aj ak, HasArrow p bj bk) =>
(aj ~> bj) -> (ak ~> bk) -> Graph (GR aj ak) (GR bj bk)
Graph a1 ~> b1
l a2 ~> b2
r ((Ob a1, Ob b1) => Graph (GR a1 a2) (GR b1 b2))
-> (a1 ~> b1) -> Graph (GR a1 a2) (GR b1 b2)
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
\\ a1 ~> b1
l ((Ob a2, Ob b2) => Graph (GR a1 a2) (GR b1 b2))
-> (a2 ~> b2) -> Graph (GR a1 a2) (GR b1 b2)
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
\\ a2 ~> b2
r

-- | The arrow category is the graph of the hom-functor. Here we require the category to be thin.
type ARROW k = GRAPH (Id :: CAT k)

-- | The category of elements of a functor.
type ELEMENTS f = GRAPH (Rep f)

-- | The comma category f/g is the graph of @C(f(-), g(=))@.
type f `COMMA` g = GRAPH (Direp f g)