Copyright | Alexey Khudyakov |
---|---|
License | BSD3-style (see LICENSE) |
Maintainer | Alexey Khudyakov <alexey.skladnoy@gmail.com> |
Stability | unstable |
Portability | unportable (GHC only) |
Safe Haskell | None |
Language | Haskell98 |
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
Natural numbers
One bit.
Instances
Nat (I n) => Nat (O (I n)) Source | |
Nat (I Z) Source | |
Nat (O n) => Nat (I (O n)) Source | |
Nat (I n) => Nat (I (I n)) Source | |
type Mul n (I m) Source | |
type Add Z (I n) Source | |
type Compare Z (I n) = IsLesser Source | |
type Normalized (I n) = I (Normalized 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 | |
type Next (I n) = O (Next n) Source | |
type Sub (I n) Z Source | |
type Add (I n) Z Source | |
type Compare (I n) Z = IsGreater Source | |
type Sub (O n) (I m) Source | |
type Sub (I n) (I m) Source | |
type Sub (I n) (O m) Source | |
type Add (O n) (I m) Source | |
type Add (I n) (I m) Source | |
type Add (I n) (O m) Source | |
type Compare (O n) (I m) Source | |
type Compare (I n) (I m) = Compare n m Source | |
type Compare (I n) (O m) Source |
Zero bit.
Instances
Number_Is_Denormalized Z => Nat (O Z) Source | |
Nat (O n) => Nat (O (O n)) Source | |
Nat (I n) => Nat (O (I n)) Source | |
Nat (O n) => Nat (I (O n)) Source | |
type Mul n (O m) = Normalized (O (Mul n m)) Source | |
type Add Z (O n) Source | |
type Compare Z (O n) = IsLesser Source | |
type Normalized (O 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 (O n)) = O (O n) Source | |
type Next (O n) = I n Source | |
type Sub (O n) Z Source | |
type Add (O n) Z Source | |
type Compare (O n) Z = IsGreater Source | |
type Sub (O n) (I m) Source | |
type Sub (O n) (O m) Source | |
type Sub (I n) (O m) Source | |
type Add (O n) (I m) Source | |
type Add (O n) (O m) Source | |
type Add (I n) (O m) Source | |
type Compare (O n) (I m) Source | |
type Compare (O n) (O m) = Compare n m Source | |
type Compare (I n) (O m) Source |
Bit stream terminator.
Instances
Nat Z Source | |
Number_Is_Denormalized Z => Nat (O Z) Source | |
Nat (I Z) Source | |
type Normalized Z = Z Source | |
type Next Z = I Z Source | |
type Mul n Z = Z Source | |
type Sub Z Z Source | |
type Add Z Z Source | |
type Compare Z Z = IsEqual Source | |
type Add Z (O n) Source | |
type Add Z (I n) Source | |
type Compare Z (O n) = IsLesser Source | |
type Compare Z (I n) = IsLesser Source | |
type Prev (I Z) = Z Source | |
type Sub (O n) Z Source | |
type Sub (I n) Z Source | |
type Add (O n) Z Source | |
type Add (I n) Z Source | |
type Compare (O n) Z = IsGreater Source | |
type Compare (I n) Z = IsGreater Source |
Type class for natural numbers. Only numbers without leading zeroes are members of this type class.
Lifting
Some natural number
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.
Template haskell utilities
Here is usage example for natT:
n123 :: $(natT 123) n123 = undefined
module TypeLevel.Number.Classes