Kinds.Num

Type-level equivalent of a subset of Num.

This provides "kindclasses" (actually open type families) with functionality analogous to that provided by the Num typeclass. 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.

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