module Proarrow.Category.Instance.Graph where

import Prelude (type (~))

import Proarrow.Category.Enriched.Thin (ThinProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, type (+->), lmap, rmap)

type data GRAPH (p :: k +-> j) = GR j k
type family GrJ a where
  GrJ (GR j k) = j
type family GrK a where
  GrK (GR j k) = k

data Graph a b where
  Graph :: (HasArrow p aj ak, HasArrow p bj bk) => aj ~> bj -> ak ~> bk -> Graph (GR aj ak :: GRAPH p) (GR bj bk)
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} (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} (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 elements of the profunctor, these should be equal.
elements :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j) (bk :: k). (ThinProfunctor p) => GR aj ak ~> (GR bj bk :: GRAPH p) -> (p aj bk, p aj bk)
elements :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j)
       (bk :: k).
ThinProfunctor p =>
(GR aj ak ~> GR bj bk) -> (p aj bk, p aj bk)
elements (Graph aj ~> bj
f ak ~> bk
g) = ((aj ~> bj) -> p bj bk -> p aj bk
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 p bj bk
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, (ak ~> bk) -> p aj ak -> p aj bk
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ak ~> bk
ak ~> bk
g p aj ak
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) ((Ob aj, Ob bj) => (p aj bk, p aj bk))
-> (aj ~> bj) -> (p aj bk, 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, p aj bk))
-> (ak ~> bk) -> (p aj 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