module Proarrow.Category.Instance.Graph where

import Prelude (type (~))

import Proarrow.Category.Enriched.Thin (ThinProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, lmap, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Profunctor.Direpresentable (Direp)
import Proarrow.Profunctor.Identity (Id)
import Proarrow.Profunctor.Representable (Rep)

type data GRAPH (p :: k +-> j) = GR j k
data family GrJ :: GRAPH (p :: k +-> j) +-> j
instance (ThinProfunctor p) => FunctorForRep (GrJ :: GRAPH (p :: k +-> j) +-> j) where
  type (GrJ :: GRAPH (p :: k +-> j) +-> j) @ GR x y = x
  fmap :: forall (a :: GRAPH p) (b :: GRAPH p).
(a ~> b) -> (GrJ @ a) ~> (GrJ @ b)
fmap (Graph aj ~> bj
l ak ~> bk
_) = aj ~> bj
(GrJ @ a) ~> (GrJ @ b)
l
data family GrK :: GRAPH (p :: k +-> j) +-> k
instance (ThinProfunctor p) => FunctorForRep (GrK :: GRAPH (p :: k +-> j) +-> k) where
  type (GrK :: GRAPH (p :: k +-> j) +-> k) @ GR x y = y
  fmap :: forall (a :: GRAPH p) (b :: GRAPH p).
(a ~> b) -> (GrK @ a) ~> (GrK @ b)
fmap (Graph aj ~> bj
_ ak ~> bk
r) = ak ~> bk
(GrK @ a) ~> (GrK @ 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 = ((GrJ @ a) ~> (GrJ @ a))
-> ((GrK @ a) ~> (GrK @ a))
-> Graph (GR (GrJ @ a) (GrK @ a)) (GR (GrJ @ a) (GrK @ 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 (GrJ @ a) ~> (GrJ @ a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (GrK @ a) ~> (GrK @ 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 (GrJ @ ab) (GrK @ ab), Ob (GrJ @ ab), Ob (GrK @ ab), HasArrow p (GrJ @ ab) (GrK @ 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) => 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 => 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 => r) -> r
forall (p :: k +-> j) (a :: j) (b :: k) r.
ThinProfunctor p =>
p a b -> (HasArrow p a 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)

-- | 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)