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

TypeLevel.Number.Nat

Description

This is type level natural numbers. They are represented using binary encoding which means that reasonable large numbers could be represented. With default context stack depth (20) maximal number is 2^18-1 (262143).

```Z           = 0
I Z         = 1
O (I Z)     = 2
I (I Z)     = 3
O (O (I Z)) = 4
...```

It's easy to see that representation for each number is not unique. One could add any numbers of leading zeroes:

`I Z = I (O Z) = I (O (O Z)) = 1`

In order to enforce uniqueness of representation only numbers without leading zeroes are members of Nat type class. This means than types are equal if and only if numbers are equal.

Natural numbers support comparison and following operations: Next, Prev, Add, Sub, Mul. All operations on numbers return normalized numbers.

Interface type classes are reexported from TypeLevel.Number.Classes

Synopsis

# Natural numbers

data I n Source

One bit.

Instances

 Nat (I n) => Show (I n) Nat (I n) => Positive (I n) Nat (I n) => NonZero (I n) Nat (I n) => Nat (O (I n)) Nat (I Z) Nat (O n) => Nat (I (O n)) Nat (I n) => Nat (I (I n)) Nat (I n) => Reify (I n) Int64 Nat (I n) => Reify (I n) Int32 (Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (I Z))))))))))))))))) => Reify (I n) Int16 (Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (I n) Int8 Nat (I n) => Reify (I n) Word64 Nat (I n) => Reify (I n) Word32 (Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (I Z)))))))))))))))))) => Reify (I n) Word16 (Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (I n) Word8 Nat (I n) => Reify (I n) Int Nat (I n) => Reify (I n) Integer type Mul n (I m) type Add Z (I n) type Compare Z (I n) = IsLesser type Normalized (I n) = I (Normalized 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) type Next (I n) = O (Next n) type Sub (I n) Z type Add (I n) Z type Compare (I n) Z = IsGreater type Sub (O n) (I m) type Sub (I n) (I m) type Sub (I n) (O m) type Add (O n) (I m) type Add (I n) (I m) type Add (I n) (O m) type Compare (O n) (I m) type Compare (I n) (I m) = Compare n m type Compare (I n) (O m)

data O n Source

Zero bit.

Instances

 Nat (O n) => Show (O n) Nat (O n) => Positive (O n) Nat (O n) => NonZero (O n) Number_Is_Denormalized Z => Nat (O Z) Nat (O n) => Nat (O (O n)) Nat (I n) => Nat (O (I n)) Nat (O n) => Nat (I (O n)) Nat (O n) => Reify (O n) Int64 Nat (O n) => Reify (O n) Int32 (Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (I Z))))))))))))))))) => Reify (O n) Int16 (Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (O n) Int8 Nat (O n) => Reify (O n) Word64 Nat (O n) => Reify (O n) Word32 (Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (I Z)))))))))))))))))) => Reify (O n) Word16 (Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (O n) Word8 Nat (O n) => Reify (O n) Int Nat (O n) => Reify (O n) Integer type Mul n (O m) = Normalized (O (Mul n m)) type Add Z (O n) type Compare Z (O n) = IsLesser type Normalized (O n) type Prev (O (O n)) = I (Prev (O n)) type Prev (O (I n)) = I (Prev (I n)) type Prev (I (O n)) = O (O n) type Next (O n) = I n type Sub (O n) Z type Add (O n) Z type Compare (O n) Z = IsGreater type Sub (O n) (I m) type Sub (O n) (O m) type Sub (I n) (O m) type Add (O n) (I m) type Add (O n) (O m) type Add (I n) (O m) type Compare (O n) (I m) type Compare (O n) (O m) = Compare n m type Compare (I n) (O m)

data Z Source

Bit stream terminator.

Instances

 Show Z Nat Z Reify Z Int Reify Z Int8 Reify Z Int16 Reify Z Int32 Reify Z Int64 Reify Z Integer Reify Z Word8 Reify Z Word16 Reify Z Word32 Reify Z Word64 Number_Is_Denormalized Z => Nat (O Z) Nat (I Z) type Normalized Z = Z type Next Z = I Z type Mul n Z = Z type Sub Z Z type Add Z Z type Compare Z Z = IsEqual type Add Z (O n) type Add Z (I n) type Compare Z (O n) = IsLesser type Compare Z (I n) = IsLesser type Prev (I Z) = Z type Sub (O n) Z type Sub (I n) Z type Add (O n) Z type Add (I n) Z type Compare (O n) Z = IsGreater type Compare (I n) Z = IsGreater

class Nat n where Source

Type class for natural numbers. Only numbers without leading zeroes are members of this type class.

Methods

toInt :: Integral i => n -> i Source

Convert natural number to integral value. It's not checked whether value could be represented.

Instances

 Nat Z Number_Is_Denormalized Z => Nat (O Z) Nat (O n) => Nat (O (O n)) Nat (I n) => Nat (O (I n)) Nat (I Z) Nat (O n) => Nat (I (O n)) Nat (I n) => Nat (I (I n))

## Lifting

data SomeNat where Source

Some natural number

Constructors

 SomeNat :: Nat n => n -> SomeNat

Instances

 Show SomeNat Typeable * SomeNat

withNat :: forall i a. Integral i => (forall n. Nat n => n -> a) -> i -> a Source

Apply function which could work with any `Nat` value only know at runtime.

```n123 :: \$(natT 123)