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 :: * 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 Source 
type Compare Z (O n) = IsLesser Source 
type Compare Z (I n) = IsLesser Source 
type Compare (O n) Z = IsGreater Source 
type Compare (I n) Z = IsGreater Source 
type Compare (O n) (I m) Source 
type Compare (O n) (O m) = Compare n m Source 
type Compare (I n) (I m) = Compare n m Source 
type Compare (I n) (O m) Source 

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

Data labels for types comparison

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 Source 

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 Source 

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 Source 

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 Source 

Special traits

class Positive n Source

Positive number.

class NonZero n Source

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

Arithmetic operations on numbers

type family Next n :: * Source

Next number.

Instances

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

nextN :: n -> Next n Source

type family Prev n :: * Source

Previous number

Instances

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

prevN :: n -> Prev n Source

type family Negate n :: * Source

Negate number.

Instances

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

type family Add n m :: * Source

Sum of two numbers.

Instances

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

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

type family Sub n m :: * Source

Difference of two numbers.

Instances

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

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

type family Mul n m :: * Source

Product of two numbers.

Instances

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

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 Source 
type Normalized Z = Z Source 
type Normalized (D1 n) = D1 (Normalized n) Source 
type Normalized (D0 n) Source 
type Normalized (Dn n) = Dn (Normalized n) Source 
type Normalized (O n) Source 
type Normalized (I n) = I (Normalized n) Source