Kinds.Num

Type-level Ord and Num.

This provides "kindclasses" (actually open type families) with functionality analogous to that provided by the typeclasses Ord and Num. Since type-level typeclasses don't exist, instead we translate each would-be method to its own open type family; then "instances" are implemented by providing clauses for each type family "method". Unfortunately this means we can't group methods into classes that must be implemented all-or-none, but in practice this seems to be okay.

Comparisons

type family Cmp (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 Cmp (x :: Nat) (y :: Nat)

Defined in Kinds.Num

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

type Cmp (x :: Integer) (y :: Integer)

Defined in Kinds.Integer

type Cmp (x :: Integer) (y :: Integer) = CmpInteger x y

type (<?) x y = IsLT (Cmp x y) infix 4

type (<=?) x y = IsLE (Cmp x y) infix 4

type (==?) x y = IsEQ (Cmp x y) infix 4

type (/=?) x y = IsNE (Cmp x y) infix 4

type (>=?) x y = IsGE (Cmp x y) infix 4

type (>?) x y = IsGT (Cmp x y) infix 4

Inequality Constraints

type (<) x y = Cmp x y ~ 'LT infix 4

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

type (==) x y = Cmp x y ~ 'EQ infix 4

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

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

type (>) x y = Cmp x y ~ 'GT infix 4

Conversions

type family FromNat (n :: Nat) :: k

Type-level numeric conversion from Nat. Like fromInteger in Num.

Instances

type FromNat n

Defined in Kinds.Num

type FromNat n = n

type FromNat n

Defined in Kinds.Integer

type FromNat n = 'Pos n

type family ToInteger (n :: k) :: Integer

Type-level conversion to Integer. Like toInteger in Integral.

Instances

type ToInteger (n :: Nat)

Defined in Kinds.Num

type ToInteger (n :: Nat) = 'Pos n

type ToInteger (n :: Integer)

Defined in Kinds.Integer

type ToInteger (n :: Integer) = n

Arithmetic

type family (x :: k) + (y :: k) :: k

Type-level addition "kindclass".

Instances

type (x :: Nat) + (y :: Nat)

Defined in Kinds.Num

type (x :: Nat) + (y :: Nat) = x + y

type (x :: Integer) + (y :: Integer)

Defined in Kinds.Integer

type (x :: Integer) + (y :: Integer) = AddInteger x y

type family (x :: k) - (y :: k) :: k

Type-level subtraction "kindclass".

Instances

type (x :: Nat) - (y :: Nat)

Defined in Kinds.Num

type (x :: Nat) - (y :: Nat) = x - y

type (x :: Integer) - (y :: Integer)

Defined in Kinds.Integer

type (x :: Integer) - (y :: Integer) = SubInteger x y

type family (x :: k) * (y :: k) :: k

Type-level multiplication "kindclass".

Instances

type (x :: Nat) * (y :: Nat)

Defined in Kinds.Num

type (x :: Nat) * (y :: Nat) = x * y

type (x :: Integer) * (y :: Integer)

Defined in Kinds.Integer

type (x :: Integer) * (y :: Integer) = MulInteger x y

Utility

type Proven b = b ~ 'True

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

type family IsLT o where ...

Test whether an Ordering is LT.

Equations

IsLT 'LT = 'True

IsLT o = 'False

type family IsLE o where ...

Test whether an Ordering is LT or EQ.

Equations

IsLE 'GT = 'False

IsLE o = 'True

type family IsGT o where ...

Test whether an Ordering is GT.

Equations

IsGT 'GT = 'True

IsGT o = 'False

type family IsGE o where ...

Test whether an Ordering is GT or EQ.

Equations

IsGE 'LT = 'False

IsGE o = 'True

type family IsEQ o where ...

Test whether an Ordering is EQ.

Equations

IsEQ 'EQ = 'True

IsEQ o = 'False

type family IsNE o where ...

Test whether an Ordering is LT or GT.

Equations

IsNE 'EQ = 'False

IsNE o = 'True