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

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 | Haskell2010

TypeLevel.Number.Classes

Contents

- Comparison of numbers
  - Data labels for types comparison
  - Specialized type classes
  - Special traits
- Arithmetic operations on numbers
- Special classes

Description

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

Synopsis

- type family Compare n m
- compareN :: n -> m -> Compare n m
- data IsLesser
- data IsEqual
- data IsGreater
- class Lesser n m
- class LesserEq n m
- class Greater n m
- class GreaterEq n m
- class Positive n
- class NonZero n
- type family Next n
- nextN :: n -> Next n
- type family Prev n
- prevN :: n -> Prev n
- type family Negate n
- negateN :: n -> Negate n
- type family Add n m
- addN :: n -> m -> Add n m
- type family Sub n m
- subN :: n -> m -> Sub n m
- type family Mul n m
- mulN :: n -> m -> Mul n m
- type family Div n m
- divN :: n -> m -> Div n m
- type family Normalized n

# 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

Instances details

type Compare Z Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z Z = IsEqual
type Compare Z (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z (I n) = IsLesser
type Compare Z (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z (O n) = IsLesser
type Compare (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) Z = IsGreater
type Compare (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) Z = IsGreater
type Compare (I n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) (I m) = Compare n m
type Compare (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) (O m)
type Compare (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) (I m)
type Compare (O n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) (O m) = Compare n m

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

## Data labels for types comparison

data IsLesser Source #

#### Instances

Instances details

Show IsLesser Source # |
Instance details Defined in TypeLevel.Number.Classes Methods showsPrec :: Int -> IsLesser -> ShowS Source # show :: IsLesser -> String Source # showList :: [IsLesser] -> ShowS Source #

data IsEqual Source #

#### Instances

Instances details

Show IsEqual Source # |
Instance details Defined in TypeLevel.Number.Classes Methods showsPrec :: Int -> IsEqual -> ShowS Source # show :: IsEqual -> String Source # showList :: [IsEqual] -> ShowS Source #

data IsGreater Source #

#### Instances

Instances details

Show IsGreater Source # |
Instance details Defined in TypeLevel.Number.Classes Methods showsPrec :: Int -> IsGreater -> ShowS Source # show :: IsGreater -> String Source # showList :: [IsGreater] -> ShowS Source #

## 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

Instances details

Compare n m ~ IsLesser => Lesser n m Source # |
Instance details Defined in TypeLevel.Number.Classes

class LesserEq n m Source #

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

#### Instances

Instances details

OneOfTwo (Compare n m) IsLesser IsEqual => LesserEq n m Source # |
Instance details Defined in TypeLevel.Number.Classes

class Greater n m Source #

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

#### Instances

Instances details

Compare n m ~ IsGreater => Greater n m Source # |
Instance details Defined in TypeLevel.Number.Classes

class GreaterEq n m Source #

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

#### Instances

Instances details

OneOfTwo (Compare n m) IsGreater IsEqual => GreaterEq n m Source # |
Instance details Defined in TypeLevel.Number.Classes

## Special traits

class Positive n Source #

Positive number.

#### Instances

Instances details

Nat (I n) => Positive (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat
Nat (O n) => Positive (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat

class NonZero n Source #

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

#### Instances

Instances details

Nat (I n) => NonZero (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat
Nat (O n) => NonZero (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat

# Arithmetic operations on numbers

type family Next n Source #

Next number.

#### Instances

Instances details

type Next ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Next ZZ = D1 ZZ
type Next Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Next Z = I Z
type Next (D0 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Next (D0 n) = D1 n
type Next (D1 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Next (D1 n) = Normalized (Dn (Next n))
type Next (Dn n) Source # |
Instance details Defined in TypeLevel.Number.Int type Next (Dn n) = Normalized (D0 n)
type Next (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Next (I n) = O (Next n)
type Next (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Next (O n) = I n

nextN :: n -> Next n Source #

type family Prev n Source #

Previous number

#### Instances

Instances details

type Prev ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Prev ZZ = Dn ZZ
type Prev (D0 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Prev (D0 n) = Dn n
type Prev (D1 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Prev (D1 n) = Normalized (D0 n)
type Prev (Dn n) Source # |
Instance details Defined in TypeLevel.Number.Int type Prev (Dn n) = Normalized (D1 (Prev n))
type Prev (I (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I (I n)) = O (I n)
type Prev (I (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I (O n)) = O (O n)
type Prev (I Z) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I Z) = Z
type Prev (O (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (O (I n)) = I (Prev (I n))
type Prev (O (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (O (O n)) = I (Prev (O n))

prevN :: n -> Prev n Source #

type family Negate n Source #

Negate number.

#### Instances

Instances details

type Negate ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Negate ZZ = ZZ
type Negate (D0 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Negate (D0 n) = D0 (Negate n)
type Negate (D1 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Negate (D1 n) = Dn (Negate n)
type Negate (Dn n) Source # |
Instance details Defined in TypeLevel.Number.Int type Negate (Dn n) = D1 (Negate n)

negateN :: n -> Negate n Source #

type family Add n m Source #

Sum of two numbers.

#### Instances

Instances details

type Add ZZ ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Add ZZ ZZ = ZZ
type Add Z Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z Z
type Add ZZ (D0 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Add ZZ (D0 n) = Normalized (D0 n)
type Add ZZ (D1 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Add ZZ (D1 n) = Normalized (D1 n)
type Add ZZ (Dn n) Source # |
Instance details Defined in TypeLevel.Number.Int type Add ZZ (Dn n) = Normalized (Dn n)
type Add Z (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z (I n)
type Add Z (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z (O n)
type Add (D0 n) ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) ZZ = Normalized (D0 n)
type Add (D1 n) ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) ZZ = Normalized (D1 n)
type Add (Dn n) ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) ZZ = Normalized (Dn n)
type Add (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) Z
type Add (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) Z
type Add (D0 n) (D0 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) (D0 m)
type Add (D0 n) (D1 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) (D1 m)
type Add (D0 n) (Dn m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) (Dn m)
type Add (D1 n) (D0 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) (D0 m)
type Add (D1 n) (D1 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) (D1 m)
type Add (D1 n) (Dn m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) (Dn m)
type Add (Dn n) (D0 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) (D0 m)
type Add (Dn n) (D1 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) (D1 m)
type Add (Dn n) (Dn m) Source # |
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) (Dn m)
type Add (I n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) (I m)
type Add (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) (O m)
type Add (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) (I m)
type Add (O n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) (O m)

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

type family Sub n m Source #

Difference of two numbers.

#### Instances

Instances details

type Sub ZZ ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Sub ZZ ZZ = ZZ
type Sub Z Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub Z Z
type Sub ZZ (D0 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub ZZ (D0 n) = Negate (D0 n)
type Sub ZZ (D1 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub ZZ (D1 n) = Negate (D1 n)
type Sub ZZ (Dn n) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub ZZ (Dn n) = Negate (Dn n)
type Sub (D0 n) ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) ZZ = D0 n
type Sub (D1 n) ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) ZZ = D1 n
type Sub (Dn n) ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) ZZ = Dn n
type Sub (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) Z
type Sub (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) Z
type Sub (D0 n) (D0 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
type Sub (D0 n) (D1 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
type Sub (D0 n) (Dn m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type Sub (D1 n) (D0 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
type Sub (D1 n) (D1 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))
type Sub (D1 n) (Dn m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
type Sub (Dn n) (D0 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
type Sub (Dn n) (D1 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
type Sub (Dn n) (Dn m) Source # |
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))
type Sub (I n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) (I m)
type Sub (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) (O m)
type Sub (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) (I m)
type Sub (O n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) (O m)

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

type family Mul n m Source #

Product of two numbers.

#### Instances

Instances details

type Mul n ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Mul n ZZ = ZZ
type Mul n Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Mul n Z = Z
type Mul n (D0 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Mul n (D0 m) = Normalized (D0 (Mul n m))
type Mul n (D1 m) Source # |
Instance details Defined in TypeLevel.Number.Int type Mul n (D1 m)
type Mul n (Dn m) Source # |
Instance details Defined in TypeLevel.Number.Int type Mul n (Dn m)
type Mul n (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Mul n (I m)
type Mul n (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Mul n (O m) = Normalized (O (Mul n 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

Instances details

type Normalized ZZ Source # |
Instance details Defined in TypeLevel.Number.Int type Normalized ZZ = ZZ
type Normalized Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Normalized Z = Z
type Normalized (D0 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Normalized (D0 n)
type Normalized (D1 n) Source # |
Instance details Defined in TypeLevel.Number.Int type Normalized (D1 n) = D1 (Normalized n)
type Normalized (Dn n) Source # |
Instance details Defined in TypeLevel.Number.Int type Normalized (Dn n) = Dn (Normalized n)
type Normalized (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Normalized (I n) = I (Normalized n)
type Normalized (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Normalized (O n)