Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Cost

Documentation

data COST Source Comments #

Constructors

C Nat
INF

Instances

Instances details

Monoidal COST Source Comments #

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

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

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

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

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

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

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

SymMonoidal COST Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

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

Distributive COST Source Comments #

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

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

distL0 :: forall (a :: COST). Ob a => (a ** (InitialObject :: COST)) ~> (InitialObject :: COST) Source Comments #

distR0 :: forall (a :: COST). Ob a => ((InitialObject :: COST) ** a) ~> (InitialObject :: COST) Source Comments #

CategoryOf COST Source Comments #

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

HasBinaryCoproducts COST Source Comments #

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

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

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

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

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

HasBinaryProducts COST Source Comments #

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

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

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

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

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

HasInitialObject COST Source Comments #

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

HasTerminalObject COST Source Comments #

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

Promonad GTE Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

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

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

MonoidalProfunctor GTE Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

par0 :: GTE (Unit :: COST) (Unit :: COST) Source Comments #

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

Profunctor GTE Source Comments #

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

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

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Unit = 'C 0

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

type (~>) = GTE

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

type InitialObject = 'INF

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

type TerminalObject = 'C 0

type Ob (a :: COST) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Cost

type Ob (a :: COST) = IsCost a

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

Instance details

Defined in Proarrow.Category.Instance.Cost

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

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

Instance details

Defined in Proarrow.Category.Instance.Cost

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

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

Instance details

Defined in Proarrow.Category.Instance.Cost

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

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

Instance details

Defined in Proarrow.Category.Instance.Cost

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

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

Instance details

Defined in Proarrow.Category.Instance.Cost

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

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

Instance details

Defined in Proarrow.Category.Instance.Cost

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Cost

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

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

Constructors

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

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

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 Comments #
Instance details Defined in Proarrow.Category.Instance.Cost Methods id :: forall (a :: COST). Ob a => GTE a a Source Comments # (.) :: forall (b :: COST) (c :: COST) (a :: COST). GTE b c -> GTE a b -> GTE a c Source Comments #
MonoidalProfunctor GTE Source Comments #
Instance details Defined in Proarrow.Category.Instance.Cost Methods par0 :: GTE (Unit :: COST) (Unit :: COST) Source Comments # par :: forall (x1 :: COST) (x2 :: COST) (y1 :: COST) (y2 :: COST). GTE x1 x2 -> GTE y1 y2 -> GTE (x1 y1) (x2 y2) Source Comments #
Profunctor GTE Source Comments #
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 Comments # (\\) :: forall (a :: COST) (b :: COST) r. ((Ob a, Ob b) => r) -> GTE a b -> r Source Comments #

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

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

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

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

Methods

sing :: SCost a Source Comments #

Instances

Instances details

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