Safe Haskell	Safe-Inferred
Language	Haskell2010

Kinds.Ord

Contents

Comparisons
Utility

Description

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.

Synopsis

type family Compare (x :: k) (y :: k) :: Ordering
type (<?) x y = CompareCond x y True False False
type (<=?) x y = CompareCond x y True True False
type (==?) x y = CompareCond x y False True False
type (/=?) x y = CompareCond x y True False True
type (>=?) x y = CompareCond x y False True True
type (>?) x y = CompareCond x y False False True
type (<) x y = Proven (x <? y)
type (<=) x y = Proven (x <=? y)
type (==) x y = Proven (x ==? y)
type (/=) x y = Proven (x /=? y)
type (>=) x y = Proven (x >=? y)
type (>) x y = Proven (x >? y)
type Max x y = CompareCond x y y y x
type Min x y = CompareCond x y x x y
data OrderingI m n where
- LTI :: Compare m n ~ 'LT => OrderingI m n
- EQI :: Compare m m ~ 'EQ => OrderingI m m
- GTI :: Compare m n ~ 'GT => OrderingI m n
type Proven b = b ~ 'True
type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where ...
type CompareCond x y lt eq gt = OrdCond (Compare x y) lt eq gt

Comparisons

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

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

Instances details

type Compare (x :: Nat) (y :: Nat) Source #
Instance details Defined in Kinds.Ord type Compare (x :: Nat) (y :: Nat) = CmpNat x y

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

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

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

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

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

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

Inequality Constraints

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

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

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

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

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

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

Selection

type Max x y = CompareCond x y y y x Source #

type Min x y = CompareCond x y x x y Source #

Proof Witnesses

data OrderingI m n where Source #

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

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 ... Source #

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

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