Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Graph

Synopsis

data GRAPH (p :: k +-> j) = GR j k
type family GrJ (a :: GRAPH p) :: k where ...
type family GrK (a :: GRAPH p) :: k where ...
data Graph (a :: GRAPH p) (b :: GRAPH p1) where
- Graph :: forall {k} {k1} {p1 :: 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 p1)
elements :: forall {j} {k} p (aj :: j) (ak :: k) (bj :: j) (bk :: k). ThinProfunctor p => (('GR aj ak :: GRAPH p) ~> ('GR bj bk :: GRAPH p)) -> (p aj bk, p aj bk)

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 => 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 #

(\\) :: forall (a :: GRAPH p) (b :: GRAPH p) r. ((Ob a, Ob b) => r) -> Graph a b -> r 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 #

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 ab) (GrK ab) :: GRAPH p), Ob (GrJ ab), Ob (GrK ab), HasArrow p (GrJ ab) (GrK ab))

type family GrJ (a :: GRAPH p) :: k where ... Source Github #

Equations

GrJ ('GR j k3 :: GRAPH p) = j

type family GrK (a :: GRAPH p) :: k where ... Source Github #

Equations

GrK ('GR j2 k2 :: GRAPH p) = k2

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

Constructors

Graph :: forall {k} {k1} {p1 :: 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 p1)

Instances

Instances details

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 # (\\) :: forall (a :: GRAPH p) (b :: GRAPH p) r. ((Ob a, Ob b) => r) -> Graph a b -> r 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 #

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

A morphism gives two elements of the profunctor, these should be equal.