Copyright	Alexey Khudyakov
License	BSD3-style (see LICENSE)
Maintainer	Alexey Khudyakov <alexey.skladnoy@gmail.com>
Stability	unstable
Portability	unportable (GHC only)
Safe Haskell	Safe-Inferred
Language	Haskell98

TypeLevel.Number.Classes

Contents

Comparison of numbers
Arithmetic operations on numbers
Special classes

Description

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

Synopsis

Comparison of numbers

type family Compare n m :: * Source

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'.

Instances

type Compare Z Z = IsEqual
type Compare Z (O n) = IsLesser
type Compare Z (I n) = IsLesser
type Compare (O n) Z = IsGreater
type Compare (I n) Z = IsGreater
type Compare (O n) (I m)
type Compare (O n) (O m) = Compare n m
type Compare (I n) (I m) = Compare n m
type Compare (I n) (O m)

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

Data labels for types comparison

data IsLesser Source

Instances

Show IsLesser

data IsEqual Source

Instances

Show IsEqual

data IsGreater Source

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 Source

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 Source

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 Source

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 Source

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 Source

Positive number.

Instances

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

class NonZero n Source

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 :: * Source

Next number.

Instances

type Next ZZ = D1 ZZ
type Next Z = I Z
type Next (D1 n) = Normalized (Dn (Next n))
type Next (D0 n) = D1 n
type Next (Dn n) = Normalized (D0 n)
type Next (O n) = I n
type Next (I n) = O (Next n)

nextN :: n -> Next n Source

type family Prev n :: * Source

Previous number

Instances

type Prev ZZ = Dn ZZ
type Prev (D1 n) = Normalized (D0 n)
type Prev (D0 n) = Dn n
type Prev (Dn n) = Normalized (D1 (Prev n))
type Prev (O (O n)) = I (Prev (O n))
type Prev (O (I n)) = I (Prev (I n))
type Prev (I Z) = Z
type Prev (I (O n)) = O (O n)
type Prev (I (I n)) = O (I n)

prevN :: n -> Prev n Source

type family Negate n :: * Source

Negate number.

Instances

type Negate ZZ = ZZ
type Negate (D1 n) = Dn (Negate n)
type Negate (D0 n) = D0 (Negate n)
type Negate (Dn n) = D1 (Negate n)

negateN :: n -> Negate n Source

type family Add n m :: * Source

Sum of two numbers.

Instances

type Add ZZ ZZ = ZZ
type Add Z Z
type Add ZZ (D1 n) = Normalized (D1 n)
type Add ZZ (D0 n) = Normalized (D0 n)
type Add ZZ (Dn n) = Normalized (Dn n)
type Add Z (O n)
type Add Z (I n)
type Add (D1 n) ZZ = Normalized (D1 n)
type Add (D0 n) ZZ = Normalized (D0 n)
type Add (Dn n) ZZ = Normalized (Dn n)
type Add (O n) Z
type Add (I n) Z
type Add (D1 n) (D1 m)
type Add (D1 n) (D0 m)
type Add (D1 n) (Dn m)
type Add (D0 n) (D1 m)
type Add (D0 n) (D0 m)
type Add (D0 n) (Dn m)
type Add (Dn n) (D1 m)
type Add (Dn n) (D0 m)
type Add (Dn n) (Dn m)
type Add (O n) (I m)
type Add (O n) (O m)
type Add (I n) (I m)
type Add (I n) (O m)

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

type family Sub n m :: * Source

Difference of two numbers.

Instances

type Sub ZZ ZZ = ZZ
type Sub Z Z
type Sub ZZ (D1 n) = Negate (D1 n)
type Sub ZZ (D0 n) = Negate (D0 n)
type Sub ZZ (Dn n) = Negate (Dn n)
type Sub (D1 n) ZZ = D1 n
type Sub (D0 n) ZZ = D0 n
type Sub (Dn n) ZZ = Dn n
type Sub (O n) Z
type Sub (I n) Z
type Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))
type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
type Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
type Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))
type Sub (O n) (I m)
type Sub (O n) (O m)
type Sub (I n) (I m)
type Sub (I n) (O m)

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

type family Mul n m :: * Source

Product of two numbers.

Instances

type Mul n Z = Z
type Mul n ZZ = ZZ
type Mul n (I m)
type Mul n (O m) = Normalized (O (Mul n m))
type Mul n (D1 m)
type Mul n (D0 m) = Normalized (D0 (Mul n m))
type Mul n (Dn m)

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

type family Div n m :: * Source

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 Source

Special classes

type family Normalized n :: * Source

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

Instances

type Normalized ZZ = ZZ
type Normalized Z = Z
type Normalized (D1 n) = D1 (Normalized n)
type Normalized (D0 n)
type Normalized (Dn n) = Dn (Normalized n)
type Normalized (O n)
type Normalized (I n) = I (Normalized n)