TypeLevel.Number.Classes

This module contain interface type classes for operations with type level numbers.

Comparison of numbers

type family Compare n m :: *

Type family for comparing two numbers. It's expected that for any two valid n and m 'Compare n m' is equal to IsLess when 'n<m', IsEqual when 'n=m' and IsGreater when 'n>m'.

compareN :: n -> m -> Compare n m

Data labels for types comparison

data IsLesser

Instances

Show IsLesser

data IsEqual

Instances

Show IsEqual

data IsGreater

Instances

Show IsGreater

Specialized type classes

These type classes are meant to be used in contexts to ensure relations between numbers. For example:

 someFunction :: Lesser n m => Data n -> Data m -> Data n
 someFunction = ...

They have generic instances and every number which is instance of Compare type family is instance of these type classes.

These instance could have problems. They weren't exensively tested. Also error messages are really unhelpful.

class Lesser n m

Numbers n and m are instances of this class if and only is n < m.

Instances

~ * (Compare n m) IsLesser => Lesser n m

class LesserEq n m

Numbers n and m are instances of this class if and only is n <= m.

Instances

OneOfTwo (Compare n m) IsLesser IsEqual => LesserEq n m

class Greater n m

Numbers n and m are instances of this class if and only is n > m.

Instances

~ * (Compare n m) IsGreater => Greater n m

class GreaterEq n m

Numbers n and m are instances of this class if and only is n >= m.

Instances

OneOfTwo (Compare n m) IsGreater IsEqual => GreaterEq n m

Special traits

class Positive n

Positive number.

Instances

Nat (O n) => Positive (O n)

Nat (I n) => Positive (I n)

class NonZero n

Non-zero number. For naturals it's same as positive

Instances

Nat (O n) => NonZero (O n)

Nat (I n) => NonZero (I n)

Arithmetic operations on numbers

type family Next n :: *

Next number.

nextN :: n -> Next n

type family Prev n :: *

Previous number

prevN :: n -> Prev n

type family Negate n :: *

Negate number.

negateN :: n -> Negate n

type family Add n m :: *

Sum of two numbers.

addN :: n -> m -> Add n m

type family Sub n m :: *

Difference of two numbers.

subN :: n -> m -> Sub n m

type family Mul n m :: *

Product of two numbers.

mulN :: n -> m -> Mul n m

type family Div n m :: *

Division of two numbers. n and m should be instances of this class only if remainder of 'n/m' is zero.

divN :: n -> m -> Div n m

Special classes

type family Normalized n :: *

Usually numbers have non-unique representation. This type family is canonical representation of number.