Kinds.Ord

Type-level Ord.

On recent versions of base, this just re-exports things from Data.Type.Ord. On older versions, it provides its own implementation, moved from older versions of numeric-kinds.

Comparisons

type family Compare (x :: k) (y :: k) :: Ordering

Type-level Ord "kindclass".

Note this has an invisible dependent k parameter that makes the textually-identical instances for different kinds actually different. Neat!

Instances

type Compare (x :: Nat) (y :: Nat)

Defined in Kinds.Ord

type Compare (x :: Nat) (y :: Nat) = CmpNat x y

type (<?) x y = CompareCond x y True False False infix 4

type (<=?) x y = CompareCond x y True True False infix 4

type (==?) x y = CompareCond x y False True False infix 9

type (/=?) x y = CompareCond x y True False True infix 9

type (>=?) x y = CompareCond x y False True True infix 4

type (>?) x y = CompareCond x y False False True infix 4

Inequality Constraints

type (<) x y = Proven (x <? y) infix 4

type (<=) x y = Proven (x <=? y) infix 4

type (==) x y = Proven (x ==? y) infix 4

type (/=) x y = Proven (x /=? y) infix 4

type (>=) x y = Proven (x >=? y) infix 4

type (>) x y = Proven (x >? y) infix 4

Selection

type Max x y = CompareCond x y y y x

type Min x y = CompareCond x y x x y

Proof Witnesses

data OrderingI m n where

Ordering results carrying evidence of type-level ordering relations.

Constructors

LTI :: Compare m n ~ 'LT => OrderingI m n

EQI :: Compare m m ~ 'EQ => OrderingI m m

GTI :: Compare m n ~ 'GT => OrderingI m n

Utility

type Proven b = b ~ 'True

Turns a type-level Bool into a Constraint that it's True.

type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where ...

Type-level eliminator for Ordering.

OrdCond o lt eq gt selects from among lt, eq, and gt according to o.

Equations

OrdCond 'LT lt eq gt = lt

OrdCond 'EQ lt eq gt = eq

OrdCond 'GT lt eq gt = gt

type CompareCond x y lt eq gt = OrdCond (Compare x y) lt eq gt

CompareCond x y lt eq gt is lt if x is less than y, and so on.