Safe Haskell	None
Language	GHC2024

Proarrow.Profunctor.Instance.Edges

Description

Relations and weighted graphs on a bare set of points, given as a table: a list of edges with their weights in the enriching category v. Edges is an enriched profunctor on the discrete category of an Indexed kind (over a discrete base there is nothing to be compatible with), so it composes, and its Kleene closure Closure is reachability for BOOL weights and shortest paths for COST weights.

Synopsis

data Edges (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) where
- Edge :: forall {k} {v} (a :: DISCRETE k) (b :: DISCRETE k) (es :: [(k, k, v)]). (Ob a, Ob b, WeightOf es a b ~ (Unit :: v)) => Edges es a b
type family WeightOf (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) :: v where ...
data EdgeList (es :: [(k, k, v)]) where
- ENil :: forall {k} {v}. EdgeList ('[] :: [(k, k, v)])
- ECons :: forall {k} {v} (x :: k) (y :: k) (w :: v) (es1 :: [(k, k, v)]). (KnownIndex x, KnownIndex y, Ob w) => EdgeList es1 -> EdgeList ('(x, y, w) ': es1)
class KnownEdges (es :: [(k, k, v)]) where
- edges :: EdgeList es
withObWeight :: forall {k} {v} (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) r. (Quantale v, Indexed k, KnownEdges es, KnownIndex a, KnownIndex b) => (Ob (WeightOf es a b) => r) -> r
enrichedEdge :: forall {k} {v} (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k). (Quantale v, Indexed k, KnownEdges es, KnownIndex a, KnownIndex b) => ((Unit :: v) ~> WeightOf es a b) -> Edges es a b

Documentation

data Edges (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) where Source Github #

A weighted graph on the bare set of points of an Indexed kind, given as a list of edges with their weights in v: an enriched profunctor on the discrete category, since over a discrete base there is nothing to be compatible with. Unlisted pairs are at InitialObject, a pair listed twice takes its first weight, and an element is a pair at Unit weight.

Constructors

Edge :: forall {k} {v} (a :: DISCRETE k) (b :: DISCRETE k) (es :: [(k, k, v)]). (Ob a, Ob b, WeightOf es a b ~ (Unit :: v)) => Edges es a b

Instances

Instances details

(Indexed k, KnownEdges es) => EnrichedProfunctor COST (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #	A graph with `COST` weights: a weighted graph, whose closure is shortest paths.
Instance details Defined in Proarrow.Profunctor.Instance.Edges Methods withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (Ob a, Ob b) => (Ob (ProObj COST (Edges es) a b) => r) -> r Source Github # underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k). Edges es a b -> (Unit :: COST) ~> ProObj COST (Edges es) a b Source Github # enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Edges es) a b) -> Edges es a b Source Github # rmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST b c ProObj COST (Edges es) a b) ~> ProObj COST (Edges es) a c Source Github # lmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST c a ProObj COST (Edges es) a b) ~> ProObj COST (Edges es) c b Source Github #
(Indexed k, KnownEdges es) => DecidableProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Edges Methods decide :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => Decision (Edges es) a b (Holds (Edges es) a b) Source Github # toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((Holds (Edges es) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
(Indexed k, KnownEdges es) => ThinProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #	A graph with `BOOL` weights is a relation on the points: decided by walking the edge list.
Instance details Defined in Proarrow.Profunctor.Instance.Edges Methods arr :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b, HasArrow (Edges es) a b) => Edges es a b Source Github # withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((HasArrow (Edges es) a b, Ob a, Ob b) => r) -> r Source Github #
Indexed k => Profunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Edges Methods dimap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k) (d :: DISCRETE k). (c ~> a) -> (b ~> d) -> Edges es a b -> Edges es c d Source Github # lmap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k). (c ~> a) -> Edges es a b -> Edges es c b Source Github # rmap :: forall (b :: DISCRETE k) (d :: DISCRETE k) (a :: DISCRETE k). (b ~> d) -> Edges es a b -> Edges es a d Source Github # (\\) :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. ((Ob a, Ob b) => r) -> Edges es a b -> r Source Github #
type ProObj COST (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Edges type ProObj COST (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = WeightOf es a b
type HasArrow (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Edges type HasArrow (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Holds (Edges es) a b ~ 'TRU
type Holds (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Edges type Holds (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = WeightOf es a b

type family WeightOf (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) :: v where ... Source Github #

Equations

WeightOf ('[] :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) = InitialObject :: v
WeightOf ('(x, y, w) ': es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) = If (Equal a ('D x) && Equal b ('D y)) w (WeightOf es a b)

data EdgeList (es :: [(k, k, v)]) where Source Github #

The edge list, reflected to the value level.

Constructors

ENil :: forall {k} {v}. EdgeList ('[] :: [(k, k, v)])
ECons :: forall {k} {v} (x :: k) (y :: k) (w :: v) (es1 :: [(k, k, v)]). (KnownIndex x, KnownIndex y, Ob w) => EdgeList es1 -> EdgeList ('(x, y, w) ': es1)

class KnownEdges (es :: [(k, k, v)]) where Source Github #

Methods

edges :: EdgeList es Source Github #

Instances

Instances details

KnownEdges ('[] :: [(k, k, v)]) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Edges Methods edges :: EdgeList ('[] :: [(k, k, v)]) Source Github #
(KnownIndex x, KnownIndex y, Ob w, KnownEdges es) => KnownEdges ('(x, y, w) ': es :: [(k, k, v)]) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Edges Methods edges :: EdgeList ('(x, y, w) ': es) Source Github #

withObWeight :: forall {k} {v} (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k) r. (Quantale v, Indexed k, KnownEdges es, KnownIndex a, KnownIndex b) => (Ob (WeightOf es a b) => r) -> r Source Github #

The weight of a pair, reflected to the value level by walking the edge list.

enrichedEdge :: forall {k} {v} (es :: [(k, k, v)]) (a :: DISCRETE k) (b :: DISCRETE k). (Quantale v, Indexed k, KnownEdges es, KnownIndex a, KnownIndex b) => ((Unit :: v) ~> WeightOf es a b) -> Edges es a b Source Github #

A unit into a weight is an edge at the unit, since an object above the unit is the unit.