Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Graph

Synopsis

data GRAPH (p :: k +-> j) = GR j k
data family GrJ :: GRAPH p +-> j
data family GrK :: GRAPH p +-> k
data Graph (a :: GRAPH p) (b :: GRAPH p) where
- Graph :: forall {k} {k1} {p :: k +-> k1} (aj :: k1) (ak :: k) (bj :: k1) (bk :: k). (HasArrow p aj ak, HasArrow p bj bk) => (aj ~> bj) -> (ak ~> bk) -> Graph ('GR aj ak :: GRAPH p) ('GR bj bk :: GRAPH p)
diagonalElement :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j) (bk :: k) r. ThinProfunctor p => (('GR aj ak :: GRAPH p) ~> ('GR bj bk :: GRAPH p)) -> (HasArrow p aj bk => r) -> r
type ARROW k = GRAPH (Id :: k -> k -> Type)
type ELEMENTS (f :: k +-> j) = GRAPH (Rep f)
type COMMA (f :: j +-> k) (g :: k1 +-> k) = GRAPH (Direp f g)

Documentation

data GRAPH (p :: k +-> j) Source Github #

Constructors

GR j k

Instances

Instances details

ThinProfunctor p => CategoryOf (GRAPH p) Source Github #

The graph of a thin profunctor. Doing this for any profunctor would need dependent types.

Instance details

Defined in Proarrow.Category.Instance.Graph

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Graph type (~>) = Graph :: GRAPH p -> GRAPH p -> Type

ThinProfunctor p => FunctorForRep (GrJ :: GRAPH p +-> j) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> ((GrJ :: GRAPH p +-> j) @ a) ~> ((GrJ :: GRAPH p +-> j) @ b) Source Github #

ThinProfunctor p => FunctorForRep (GrK :: GRAPH p +-> k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> ((GrK :: GRAPH p +-> k) @ a) ~> ((GrK :: GRAPH p +-> k) @ b) Source Github #

ThinProfunctor p => Promonad (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

id :: forall (a :: GRAPH p). Ob a => Graph a a Source Github #

(.) :: forall (b :: GRAPH p) (c :: GRAPH p) (a :: GRAPH p). Graph b c -> Graph a b -> Graph a c Source Github #

ThinProfunctor p => Profunctor (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

dimap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p) (d :: GRAPH p). (c ~> a) -> (b ~> d) -> Graph a b -> Graph c d Source Github #

lmap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p). (c ~> a) -> Graph a b -> Graph c b Source Github #

rmap :: forall (b :: GRAPH p) (d :: GRAPH p) (a :: GRAPH p). (b ~> d) -> Graph a b -> Graph a d Source Github #

(\\) :: forall (a :: GRAPH p) (b :: GRAPH p) r. ((Ob a, Ob b) => r) -> Graph a b -> r Source Github #

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type (~>) = Graph :: GRAPH p -> GRAPH p -> Type

type Ob (ab :: GRAPH p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type Ob (ab :: GRAPH p) = (ab ~ ('GR ((GrJ :: GRAPH p +-> j) @ ab) ((GrK :: GRAPH p +-> k) @ ab) :: GRAPH p), Ob ((GrJ :: GRAPH p +-> j) @ ab), Ob ((GrK :: GRAPH p +-> k) @ ab), HasArrow p ((GrJ :: GRAPH p +-> j) @ ab) ((GrK :: GRAPH p +-> k) @ ab))

type (GrJ :: GRAPH p +-> j) @ ('GR x y :: GRAPH p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type (GrJ :: GRAPH p +-> j) @ ('GR x y :: GRAPH p) = x

type (GrK :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type (GrK :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) = y

data family GrJ :: GRAPH p +-> j Source Github #

Instances

Instances details

ThinProfunctor p => FunctorForRep (GrJ :: GRAPH p +-> j) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> ((GrJ :: GRAPH p +-> j) @ a) ~> ((GrJ :: GRAPH p +-> j) @ b) Source Github #
type (GrJ :: GRAPH p +-> j) @ ('GR x y :: GRAPH p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph type (GrJ :: GRAPH p +-> j) @ ('GR x y :: GRAPH p) = x

data family GrK :: GRAPH p +-> k Source Github #

Instances

Instances details

ThinProfunctor p => FunctorForRep (GrK :: GRAPH p +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> ((GrK :: GRAPH p +-> k) @ a) ~> ((GrK :: GRAPH p +-> k) @ b) Source Github #
type (GrK :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph type (GrK :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) = y

data Graph (a :: GRAPH p) (b :: GRAPH p) where Source Github #

Constructors

Graph :: forall {k} {k1} {p :: k +-> k1} (aj :: k1) (ak :: k) (bj :: k1) (bk :: k). (HasArrow p aj ak, HasArrow p bj bk) => (aj ~> bj) -> (ak ~> bk) -> Graph ('GR aj ak :: GRAPH p) ('GR bj bk :: GRAPH p)

Instances

Instances details

ThinProfunctor p => Promonad (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods id :: forall (a :: GRAPH p). Ob a => Graph a a Source Github # (.) :: forall (b :: GRAPH p) (c :: GRAPH p) (a :: GRAPH p). Graph b c -> Graph a b -> Graph a c Source Github #
ThinProfunctor p => Profunctor (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods dimap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p) (d :: GRAPH p). (c ~> a) -> (b ~> d) -> Graph a b -> Graph c d Source Github # lmap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p). (c ~> a) -> Graph a b -> Graph c b Source Github # rmap :: forall (b :: GRAPH p) (d :: GRAPH p) (a :: GRAPH p). (b ~> d) -> Graph a b -> Graph a d Source Github # (\\) :: forall (a :: GRAPH p) (b :: GRAPH p) r. ((Ob a, Ob b) => r) -> Graph a b -> r Source Github #

diagonalElement :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j) (bk :: k) r. ThinProfunctor p => (('GR aj ak :: GRAPH p) ~> ('GR bj bk :: GRAPH p)) -> (HasArrow p aj bk => r) -> r Source Github #

A morphism gives two equal ways to compute the "diagonal", which is an element of the profunctor.

type ARROW k = GRAPH (Id :: k -> k -> Type) Source Github #

The arrow category is the graph of the hom-functor. Here we require the category to be thin.

type ELEMENTS (f :: k +-> j) = GRAPH (Rep f) Source Github #

The category of elements of a functor.

type COMMA (f :: j +-> k) (g :: k1 +-> k) = GRAPH (Direp f g) Source Github #

The comma category f/g is the graph of C(f(-), g(=)).