type-level-numbers-0.1.1.1: Type level numbers implemented using type families.

CopyrightAlexey Khudyakov
LicenseBSD3-style (see LICENSE)
MaintainerAlexey Khudyakov <alexey.skladnoy@gmail.com>
Stabilityunstable
Portabilityunportable (GHC only)
Safe HaskellSafe
LanguageHaskell98

TypeLevel.Number.Classes

Contents

Description

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

Synopsis

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

Instances

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

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

Data labels for types comparison

data IsLesser #

Instances

data IsEqual #

Instances

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.

class NonZero n #

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

Arithmetic operations on numbers

type family Next n :: * #

Next number.

Instances

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

nextN :: n -> Next n #

type family Prev n :: * #

Previous number

Instances

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

prevN :: n -> Prev n #

type family Negate n :: * #

Negate number.

Instances

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

negateN :: n -> Negate n #

type family Add n m :: * #

Sum of two numbers.

Instances

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

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

type family Sub n m :: * #

Difference of two numbers.

Instances

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

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

type family Mul n m :: * #

Product of two numbers.

Instances

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

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.

Instances

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