Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Cost

Description

The Lawvere cost category: extended natural numbers (C n or INF) as a thin category with an arrow a ~> b exactly when a >= b (GTE). Addition of costs provides a symmetric monoidal structure with C 0 as unit (and terminal object; INF is initial), so categories enriched in COST are generalized (Lawvere) metric spaces.

Documentation

data COST Source Github #

Constructors

C Nat
INF

Instances

Instances details

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 #

Monoidal COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Cost type Unit = 'C 0
type ('C a :: COST) ** ('C b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type ('C a :: COST) ** ('C b :: COST) = 'C (a + b)
type 'INF ** (b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type 'INF ** (b :: COST) = 'INF
type (a :: COST) ** 'INF
Instance details Defined in Proarrow.Category.Instance.Cost type (a :: COST) ** 'INF = 'INF

Methods

withOb2 :: forall (a :: COST) (b :: COST) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: COST). Ob a => ((Unit :: COST) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: COST). Ob a => a ~> ((Unit :: COST) ** a) Source Github #

rightUnitor :: forall (a :: COST). Ob a => (a ** (Unit :: COST)) ~> a Source Github #

rightUnitorInv :: forall (a :: COST). Ob a => a ~> (a ** (Unit :: COST)) Source Github #

associator :: forall (a :: COST) (b :: COST) (c :: COST). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: COST) (b :: COST) (c :: COST). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

SymMonoidal COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

swap :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Distributive COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

distL :: forall (a :: COST) (b :: COST) (c :: COST). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: COST) (b :: COST) (c :: COST). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: COST). Ob a => (a ** (InitialObject :: COST)) ~> (InitialObject :: COST) Source Github #

absorbR :: forall (a :: COST). Ob a => ((InitialObject :: COST) ** a) ~> (InitialObject :: COST) Source Github #

HasEpiMonoFactorization COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

factorize :: forall (a :: COST) (b :: COST). (a ~> b) -> (Hom COST :.: Hom COST) a b Source Github #

HasBinaryCoproducts COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type ('C a :: COST) \|\| ('C b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type ('C a :: COST) \|\| ('C b :: COST) = 'C (Min a b)
type 'INF \|\| (b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type 'INF \|\| (b :: COST) = b
type (a :: COST) \|\| 'INF
Instance details Defined in Proarrow.Category.Instance.Cost type (a :: COST) \|\| 'INF = a

Methods

withObCoprod :: forall (a :: COST) (b :: COST) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: COST) (a :: COST) (y :: COST). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: COST) (b :: COST) (x :: COST) (y :: COST). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasCoequalizers COST Source Github #

Dual to the HasEqualizers instance above.

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

coequalize :: forall (a :: COST) (b :: COST) r. (a ~> b) -> (a ~> b) -> (forall (c :: COST). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: COST) (x :: COST) (c' :: COST). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

HasInitialObject COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Cost type InitialObject = 'INF

Methods

initiate :: forall (a :: COST). Ob a => (InitialObject :: COST) ~> a Source Github #

HasPushouts COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

pushout :: forall (o :: COST) (a :: COST) (b :: COST) r. (o ~> a) -> (o ~> b) -> (forall (p :: COST). (a ~> p) -> (b ~> p) -> r) -> r Source Github #

factorPushout :: forall (a :: COST) (b :: COST) (p :: COST) (q :: COST). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

CategoryOf COST Source Github #

Cost category. Categories enriched in the cost category are lawvere metric spaces.

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Cost type (~>) = GTE
type Ob (a :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type Ob (a :: COST) = IsCost a

HasBinaryProducts COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type ('C a :: COST) && ('C b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type ('C a :: COST) && ('C b :: COST) = 'C (Max a b)
type 'INF && (b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type 'INF && (b :: COST) = 'INF
type (a :: COST) && 'INF
Instance details Defined in Proarrow.Category.Instance.Cost type (a :: COST) && 'INF = 'INF

Methods

withObProd :: forall (a :: COST) (b :: COST) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: COST) (x :: COST) (y :: COST). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: COST) (b :: COST) (x :: COST) (y :: COST). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasEqualizers COST Source Github #

COST is thin and totally ordered, so equalizers are trivial. factorEqualizer incl h just compares e and e' directly (their common bound x does not matter), erroring when and only when e' is finite and strictly less than e, or e is INF while e' is finite.

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

equalize :: forall (a :: COST) (b :: COST) r. (a ~> b) -> (a ~> b) -> (forall (e :: COST). (e ~> a) -> r) -> r Source Github #

factorEqualizer :: forall (e :: COST) (x :: COST) (e' :: COST). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #

HasPullbacks COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

pullback :: forall (o :: COST) (a :: COST) (b :: COST) r. (a ~> o) -> (b ~> o) -> (forall (p :: COST). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

factorPullback :: forall (a :: COST) (b :: COST) (p :: COST) (q :: COST). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

HasTerminalObject COST Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Cost type TerminalObject = 'C 0

Methods

terminate :: forall (a :: COST). Ob a => a ~> (TerminalObject :: COST) Source Github #

Promonad GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

id :: forall (a :: COST). Ob a => GTE a a Source Github #

(.) :: forall (b :: COST) (c :: COST) (a :: COST). GTE b c -> GTE a b -> GTE a c Source Github #

DecidableProfunctor GTE Source Github #

Decided by comparing the naturals; INF is below everything.

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type Holds GTE ('C a :: COST) ('C b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type Holds GTE ('C a :: COST) ('C b :: COST) = FromBool (b <=? a)
type Holds GTE ('C a :: COST) 'INF
Instance details Defined in Proarrow.Category.Instance.Cost type Holds GTE ('C a :: COST) 'INF = 'FLS
type Holds GTE 'INF (b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type Holds GTE 'INF (b :: COST) = 'TRU

Methods

decide :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => Decision GTE a b (Holds GTE a b) Source Github #

toHolds :: forall (a :: COST) (b :: COST) r. GTE a b -> ((Holds GTE a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type HasArrow GTE (a :: COST) (b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type HasArrow GTE (a :: COST) (b :: COST) = Holds GTE a b ~ 'TRU

Methods

arr :: forall (a :: COST) (b :: COST). (Ob a, Ob b, HasArrow GTE a b) => GTE a b Source Github #

withArr :: forall (a :: COST) (b :: COST) r. GTE a b -> ((HasArrow GTE a b, Ob a, Ob b) => r) -> r Source Github #

MonoidalProfunctor GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

one :: GTE (Unit :: COST) (Unit :: COST) Source Github #

(**) :: forall (x1 :: COST) (x2 :: COST) (y1 :: COST) (y2 :: COST). GTE x1 x2 -> GTE y1 y2 -> GTE (x1 ** y1) (x2 ** y2) Source Github #

Profunctor GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

dimap :: forall (c :: COST) (a :: COST) (b :: COST) (d :: COST). (c ~> a) -> (b ~> d) -> GTE a b -> GTE c d Source Github #

lmap :: forall (c :: COST) (a :: COST) (b :: COST). (c ~> a) -> GTE a b -> GTE c b Source Github #

rmap :: forall (b :: COST) (d :: COST) (a :: COST). (b ~> d) -> GTE a b -> GTE a d Source Github #

(\\) :: forall (a :: COST) (b :: COST) r. ((Ob a, Ob b) => r) -> GTE a b -> r Source Github #

(SNatI n, EnrichedProfunctor COST p, Enriched COST k, Enumerable k) => EnrichedProfunctor COST (Walk n p :: k -> k -> Type) Source Github #

Walks along a COST-weighted graph form the free Lawvere metric space on it: withProObj runs the fixed point that computes the shortest distances, underlying and enriched relate a walk of zero-cost pieces to a zero distance, and the actions of the base are the triangle inequality.

Instance details

Defined in Proarrow.Category.Enriched.Thin.Composition

Methods

withProObj :: forall (a :: k) (b :: k) r. (Ob a, Ob b) => (Ob (ProObj COST (Walk n p) a b) => r) -> r Source Github #

underlying :: forall (a :: k) (b :: k). Walk n p a b -> (Unit :: COST) ~> ProObj COST (Walk n p) a b Source Github #

enriched :: forall (a :: k) (b :: k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Walk n p) a b) -> Walk n p a b Source Github #

rmap :: forall (a :: k) (b :: k) (c :: k). (Ob a, Ob b, Ob c) => (HomObj COST b c ** ProObj COST (Walk n p) a b) ~> ProObj COST (Walk n p) a c Source Github #

lmap :: forall (a :: k) (b :: k) (c :: k). (Ob a, Ob b, Ob c) => (HomObj COST c a ** ProObj COST (Walk n p) a b) ~> ProObj COST (Walk n p) c b Source Github #

Indexed k => EnrichedProfunctor COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (Ob a, Ob b) => (Ob (ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) => r) -> r Source Github #

underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k). Discrete a b -> (Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b Source Github #

enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) -> Discrete 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 (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) 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 (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) c b Source Github #

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

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Unit = 'C 0

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type InitialObject = 'INF

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type (~>) = GTE

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type TerminalObject = 'C 0

type Ob (a :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Ob (a :: COST) = IsCost a

type 'INF ** (b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type 'INF ** (b :: COST) = 'INF

type (a :: COST) ** 'INF Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type (a :: COST) ** 'INF = 'INF

type 'INF || (b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type 'INF || (b :: COST) = b

type (a :: COST) || 'INF Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type (a :: COST) || 'INF = a

type 'INF && (b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type 'INF && (b :: COST) = 'INF

type (a :: COST) && 'INF Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type (a :: COST) && 'INF = 'INF

type HasArrow GTE (a :: COST) (b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type HasArrow GTE (a :: COST) (b :: COST) = Holds GTE a b ~ 'TRU

type Holds GTE 'INF (b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE 'INF (b :: COST) = 'TRU

type Holds GTE ('C a :: COST) 'INF Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE ('C a :: COST) 'INF = 'FLS

type Holds GTE ('C a :: COST) ('C b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE ('C a :: COST) ('C b :: COST) = FromBool (b <=? a)

type ProObj COST (Walk n p :: k -> k -> Type) (a :: k) (b :: k) Source Github #

Instance details

Defined in Proarrow.Category.Enriched.Thin.Composition

type ProObj COST (Walk n p :: k -> k -> Type) (a :: k) (b :: k) = Walks COST n p a b

type ('C a :: COST) ** ('C b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type ('C a :: COST) ** ('C b :: COST) = 'C (a + b)

type ('C a :: COST) || ('C b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type ('C a :: COST) || ('C b :: COST) = 'C (Min a b)

type ('C a :: COST) && ('C b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type ('C a :: COST) && ('C b :: COST) = 'C (Max a b)

type ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Delta COST (Equal a b)

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

data SCost (n :: COST) where Source Github #

Constructors

SC :: forall (n1 :: Nat). KnownNat n1 => SCost ('C n1)
SINF :: SCost 'INF

data GTE (a :: COST) (b :: COST) where Source Github #

Constructors

Inf :: forall (b :: COST). Ob b => GTE 'INF b
GTE :: forall (a1 :: Nat) (b1 :: Nat). (KnownNat a1, KnownNat b1, b1 <= a1) => GTE ('C a1) ('C b1)

Instances

Instances details

Promonad GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

id :: forall (a :: COST). Ob a => GTE a a Source Github #

(.) :: forall (b :: COST) (c :: COST) (a :: COST). GTE b c -> GTE a b -> GTE a c Source Github #

DecidableProfunctor GTE Source Github #

Decided by comparing the naturals; INF is below everything.

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type Holds GTE ('C a :: COST) ('C b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type Holds GTE ('C a :: COST) ('C b :: COST) = FromBool (b <=? a)
type Holds GTE ('C a :: COST) 'INF
Instance details Defined in Proarrow.Category.Instance.Cost type Holds GTE ('C a :: COST) 'INF = 'FLS
type Holds GTE 'INF (b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type Holds GTE 'INF (b :: COST) = 'TRU

Methods

decide :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => Decision GTE a b (Holds GTE a b) Source Github #

toHolds :: forall (a :: COST) (b :: COST) r. GTE a b -> ((Holds GTE a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type HasArrow GTE (a :: COST) (b :: COST)
Instance details Defined in Proarrow.Category.Instance.Cost type HasArrow GTE (a :: COST) (b :: COST) = Holds GTE a b ~ 'TRU

Methods

arr :: forall (a :: COST) (b :: COST). (Ob a, Ob b, HasArrow GTE a b) => GTE a b Source Github #

withArr :: forall (a :: COST) (b :: COST) r. GTE a b -> ((HasArrow GTE a b, Ob a, Ob b) => r) -> r Source Github #

MonoidalProfunctor GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

one :: GTE (Unit :: COST) (Unit :: COST) Source Github #

(**) :: forall (x1 :: COST) (x2 :: COST) (y1 :: COST) (y2 :: COST). GTE x1 x2 -> GTE y1 y2 -> GTE (x1 ** y1) (x2 ** y2) Source Github #

Profunctor GTE Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

dimap :: forall (c :: COST) (a :: COST) (b :: COST) (d :: COST). (c ~> a) -> (b ~> d) -> GTE a b -> GTE c d Source Github #

lmap :: forall (c :: COST) (a :: COST) (b :: COST). (c ~> a) -> GTE a b -> GTE c b Source Github #

rmap :: forall (b :: COST) (d :: COST) (a :: COST). (b ~> d) -> GTE a b -> GTE a d Source Github #

(\\) :: forall (a :: COST) (b :: COST) r. ((Ob a, Ob b) => r) -> GTE a b -> r Source Github #

type HasArrow GTE (a :: COST) (b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type HasArrow GTE (a :: COST) (b :: COST) = Holds GTE a b ~ 'TRU

type Holds GTE 'INF (b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE 'INF (b :: COST) = 'TRU

type Holds GTE ('C a :: COST) 'INF Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE ('C a :: COST) 'INF = 'FLS

type Holds GTE ('C a :: COST) ('C b :: COST) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE ('C a :: COST) ('C b :: COST) = FromBool (b <=? a)

lteTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat) r. (a <= b, b <= c, KnownNat a, KnownNat c) => (a <= c => r) -> r Source Github #

plusMonotone :: forall (a :: Nat) (b :: Nat) (c :: Natural) (d :: Natural) r. (a <= b, c <= d, KnownNat (a + c), KnownNat (b + d)) => ((a + c) <= (b + d) => r) -> r Source Github #

withPlusIsNat :: forall (a :: Nat) (b :: Nat) r. (KnownNat a, KnownNat b) => (KnownNat (a + b) => r) -> r Source Github #

class IsCost (a :: COST) where Source Github #

Methods

sing :: SCost a Source Github #

Instances

Instances details

IsCost 'INF Source Github #
Instance details Defined in Proarrow.Category.Instance.Cost Methods sing :: SCost 'INF Source Github #
KnownNat n => IsCost ('C n) Source Github #
Instance details Defined in Proarrow.Category.Instance.Cost Methods sing :: SCost ('C n) Source Github #