Safe Haskell	None
Language	GHC2024

Proarrow.Category.Enriched.Quantale

Description

Totally ordered, integral quantales, as far as computing closures of enriched profunctors needs them: BOOL (relations, reachability) and COST (metric spaces, shortest paths). Besides the structure their classes already provide, the closure needs a handful of facts reflected to the value level, collected in Quantale.

Synopsis

class (Semicartesian v, Distributive v, Decidable v) => Quantale v where
- minIs :: forall (x :: v) (y :: v). (Ob x, Ob y) => MinIs x y
- unitIsNotBottom :: ((Unit :: v) ~> (InitialObject :: v)) -> r
- unitIsTop :: forall (w :: v) r. Ob w => ((Unit :: v) ~> w) -> (w ~ (Unit :: v) => r) -> r
data MinIs (x :: v) (y :: v) where
- MinLeft :: forall {v} (x :: v) (y :: v). (x || y) ~ x => MinIs x y
- MinRight :: forall {v} (x :: v) (y :: v). (x || y) ~ y => MinIs x y
splitUnit :: forall {v} (x :: v) (y :: v). (Quantale v, Ob x, Ob y) => ((Unit :: v) ~> (x ** y)) -> ((Unit :: v) ~> x, (Unit :: v) ~> y)
bottomTensor :: forall {v} (x :: v) (y :: v). (Quantale v, Ob x, Ob y) => ((InitialObject :: v) ** x) ~> y
checkedArrow :: forall v (x :: v) (y :: v). (Decidable v, Ob x, Ob y) => x ~> y

Documentation

class (Semicartesian v, Distributive v, Decidable v) => Quantale v where Source Github #

As much of a quantale as a closure needs, and a totally ordered, integral one at that: a Semicartesian Distributive category, so that the unit is the top element and the bottom absorbs, in which the join of two objects is one of them (minIs) and the order is decidable. Totality is what makes a single best walk exist; in a quantale of, say, sets of paths, a join is attained by no one summand. Infinite joins are not needed, since there are finitely many objects.

The methods reflect to the value level facts that GHC cannot see through the type families: minIs is totality, and unitIsNotBottom and unitIsTop say the order is nondegenerate and skeletal -- the latter is antisymmetry at the unit, since Semicartesian already gives the arrow the other way.

Methods

minIs :: forall (x :: v) (y :: v). (Ob x, Ob y) => MinIs x y Source Github #

unitIsNotBottom :: ((Unit :: v) ~> (InitialObject :: v)) -> r Source Github #

unitIsTop :: forall (w :: v) r. Ob w => ((Unit :: v) ~> w) -> (w ~ (Unit :: v) => r) -> r Source Github #

Instances

Instances details

Quantale BOOL Source Github #	The walking arrow: the tensor is conjunction, the join disjunction.
Instance details Defined in Proarrow.Category.Enriched.Quantale Methods minIs :: forall (x :: BOOL) (y :: BOOL). (Ob x, Ob y) => MinIs x y Source Github # unitIsNotBottom :: ((Unit :: BOOL) ~> (InitialObject :: BOOL)) -> r Source Github # unitIsTop :: forall (w :: BOOL) r. Ob w => ((Unit :: BOOL) ~> w) -> (w ~ (Unit :: BOOL) => r) -> r Source Github #
Quantale COST Source Github #	Costs: the tensor is addition, the join the minimum. Distances are compared with `cmpNat`, whose evidence makes the type-level `Min` reduce; that a natural below `0` is `0` is arithmetic GHC cannot see, so it is checked at runtime.
Instance details Defined in Proarrow.Category.Enriched.Quantale Methods minIs :: forall (x :: COST) (y :: COST). (Ob x, Ob y) => MinIs x y Source Github # unitIsNotBottom :: ((Unit :: COST) ~> (InitialObject :: COST)) -> r Source Github # unitIsTop :: forall (w :: COST) r. Ob w => ((Unit :: COST) ~> w) -> (w ~ (Unit :: COST) => r) -> r Source Github #

data MinIs (x :: v) (y :: v) where Source Github #

Which of two objects their join is.

Constructors

MinLeft :: forall {v} (x :: v) (y :: v). (x \|\| y) ~ x => MinIs x y
MinRight :: forall {v} (x :: v) (y :: v). (x \|\| y) ~ y => MinIs x y

splitUnit :: forall {v} (x :: v) (y :: v). (Quantale v, Ob x, Ob y) => ((Unit :: v) ~> (x ** y)) -> ((Unit :: v) ~> x, (Unit :: v) ~> y) Source Github #

In an integral quantale a tensor lies below each of its factors, since the other factor is at most the unit, so a unit into a tensor is a unit into each factor.

bottomTensor :: forall {v} (x :: v) (y :: v). (Quantale v, Ob x, Ob y) => ((InitialObject :: v) ** x) ~> y Source Github #

The bottom absorbs the tensor, and nothing lies below the bottom.

checkedArrow :: forall v (x :: v) (y :: v). (Decidable v, Ob x, Ob y) => x ~> y Source Github #

The arrow between two objects of a decidable order, when the caller knows it exists but its existence is not derived structurally -- the triangle inequality for closures, for instance. As elsewhere in Proarrow.Category.Instance.Cost, it is checked at runtime.