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 HaskellNone
LanguageHaskell98

TypeLevel.Number.Nat

Contents

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) => Nat (O (I n)) Source # 

Methods

toInt :: Integral i => O (I n) -> i Source #

Nat (I Z) Source # 

Methods

toInt :: Integral i => I Z -> i Source #

Nat (O n) => Nat (I (O n)) Source # 

Methods

toInt :: Integral i => I (O n) -> i Source #

Nat (I n) => Nat (I (I n)) Source # 

Methods

toInt :: Integral i => I (I n) -> i Source #

type Mul n (I m) Source # 
type Mul n (I m)
type Add Z (I n) Source # 
type Add Z (I n)
type Compare Z (I n) Source # 
type Compare Z (I n) = IsLesser
type Normalized (I n) Source # 
type Normalized (I n) = I (Normalized n)
type Prev (O (I n)) Source # 
type Prev (O (I n)) = I (Prev (I n))
type Prev (I Z) Source # 
type Prev (I Z) = Z
type Prev (I (O n)) Source # 
type Prev (I (O n)) = O (O n)
type Prev (I (I n)) Source # 
type Prev (I (I n)) = O (I n)
type Next (I n) Source # 
type Next (I n) = O (Next n)
type Sub (I n) Z Source # 
type Sub (I n) Z
type Add (I n) Z Source # 
type Add (I n) Z
type Compare (I n) Z Source # 
type Compare (I n) Z = IsGreater
type Sub (O n) (I m) Source # 
type Sub (O n) (I m)
type Sub (I n) (I m) Source # 
type Sub (I n) (I m)
type Sub (I n) (O m) Source # 
type Sub (I n) (O m)
type Add (O n) (I m) Source # 
type Add (O n) (I m)
type Add (I n) (I m) Source # 
type Add (I n) (I m)
type Add (I n) (O m) Source # 
type Add (I n) (O m)
type Compare (O n) (I m) Source # 
type Compare (O n) (I m)
type Compare (I n) (I m) Source # 
type Compare (I n) (I m) = Compare n m
type Compare (I n) (O m) Source # 
type Compare (I n) (O m)

data O n Source #

Zero bit.

Instances

Number_Is_Denormalized Z => Nat (O Z) Source # 

Methods

toInt :: Integral i => O Z -> i Source #

Nat (O n) => Nat (O (O n)) Source # 

Methods

toInt :: Integral i => O (O n) -> i Source #

Nat (I n) => Nat (O (I n)) Source # 

Methods

toInt :: Integral i => O (I n) -> i Source #

Nat (O n) => Nat (I (O n)) Source # 

Methods

toInt :: Integral i => I (O n) -> i Source #

type Mul n (O m) Source # 
type Mul n (O m) = Normalized (O (Mul n m))
type Add Z (O n) Source # 
type Add Z (O n)
type Compare Z (O n) Source # 
type Compare Z (O n) = IsLesser
type Normalized (O n) Source # 
type Normalized (O n)
type Prev (O (O n)) Source # 
type Prev (O (O n)) = I (Prev (O n))
type Prev (O (I n)) Source # 
type Prev (O (I n)) = I (Prev (I n))
type Prev (I (O n)) Source # 
type Prev (I (O n)) = O (O n)
type Next (O n) Source # 
type Next (O n) = I n
type Sub (O n) Z Source # 
type Sub (O n) Z
type Add (O n) Z Source # 
type Add (O n) Z
type Compare (O n) Z Source # 
type Compare (O n) Z = IsGreater
type Sub (O n) (I m) Source # 
type Sub (O n) (I m)
type Sub (O n) (O m) Source # 
type Sub (O n) (O m)
type Sub (I n) (O m) Source # 
type Sub (I n) (O m)
type Add (O n) (I m) Source # 
type Add (O n) (I m)
type Add (O n) (O m) Source # 
type Add (O n) (O m)
type Add (I n) (O m) Source # 
type Add (I n) (O m)
type Compare (O n) (O m) Source # 
type Compare (O n) (O m) = Compare n m
type Compare (O n) (I m) Source # 
type Compare (O n) (I m)
type Compare (I n) (O m) Source # 
type Compare (I n) (O m)

data Z Source #

Bit stream terminator.

Instances

Nat Z Source # 

Methods

toInt :: Integral i => Z -> i Source #

Number_Is_Denormalized Z => Nat (O Z) Source # 

Methods

toInt :: Integral i => O Z -> i Source #

Nat (I Z) Source # 

Methods

toInt :: Integral i => I Z -> i Source #

type Normalized Z Source # 
type Normalized Z = Z
type Next Z Source # 
type Next Z = I Z
type Mul n Z Source # 
type Mul n Z = Z
type Sub Z Z Source # 
type Sub Z Z
type Add Z Z Source # 
type Add Z Z
type Compare Z Z Source # 
type Add Z (O n) Source # 
type Add Z (O n)
type Add Z (I n) Source # 
type Add Z (I n)
type Compare Z (O n) Source # 
type Compare Z (O n) = IsLesser
type Compare Z (I n) Source # 
type Compare Z (I n) = IsLesser
type Prev (I Z) Source # 
type Prev (I Z) = Z
type Sub (O n) Z Source # 
type Sub (O n) Z
type Sub (I n) Z Source # 
type Sub (I n) Z
type Add (O n) Z Source # 
type Add (O n) Z
type Add (I n) Z Source # 
type Add (I n) Z
type Compare (O n) Z Source # 
type Compare (O n) Z = IsGreater
type Compare (I n) Z Source # 
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.

Minimal complete definition

toInt

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

Methods

toInt :: Integral i => Z -> i Source #

Number_Is_Denormalized Z => Nat (O Z) Source # 

Methods

toInt :: Integral i => O Z -> i Source #

Nat (O n) => Nat (O (O n)) Source # 

Methods

toInt :: Integral i => O (O n) -> i Source #

Nat (I n) => Nat (O (I n)) Source # 

Methods

toInt :: Integral i => O (I n) -> i Source #

Nat (I Z) Source # 

Methods

toInt :: Integral i => I Z -> i Source #

Nat (O n) => Nat (I (O n)) Source # 

Methods

toInt :: Integral i => I (O n) -> i Source #

Nat (I n) => Nat (I (I n)) Source # 

Methods

toInt :: Integral i => I (I n) -> i Source #

Lifting

data SomeNat where Source #

Some natural number

Constructors

SomeNat :: Nat n => n -> SomeNat 

Instances

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

natT :: Integer -> TypeQ Source #

Create type for natural number.

nat :: Integer -> ExpQ Source #

Create value for type level natural. Value itself is undefined.

Orphan instances

Show Z Source # 

Methods

showsPrec :: Int -> Z -> ShowS #

show :: Z -> String #

showList :: [Z] -> ShowS #

Reify Z Int Source # 
Reify Z Int8 Source # 
Reify Z Int16 Source # 
Reify Z Int32 Source # 
Reify Z Int64 Source # 
Reify Z Integer Source # 
Reify Z Word8 Source # 
Reify Z Word16 Source # 
Reify Z Word32 Source # 
Reify Z Word64 Source # 
Nat (O n) => Show (O n) Source # 

Methods

showsPrec :: Int -> O n -> ShowS #

show :: O n -> String #

showList :: [O n] -> ShowS #

Nat (I n) => Show (I n) Source # 

Methods

showsPrec :: Int -> I n -> ShowS #

show :: I n -> String #

showList :: [I n] -> ShowS #

Nat (O n) => Positive (O n) Source # 
Nat (I n) => Positive (I n) Source # 
Nat (O n) => NonZero (O n) Source # 
Nat (I n) => NonZero (I n) Source # 
Nat (O n) => Reify (O n) Int64 Source # 

Methods

witness :: Witness (O n) Int64 Source #

Nat (O n) => Reify (O n) Int32 Source # 

Methods

witness :: Witness (O n) Int32 Source #

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

Methods

witness :: Witness (O n) Int16 Source #

(Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (O n) Int8 Source # 

Methods

witness :: Witness (O n) Int8 Source #

Nat (O n) => Reify (O n) Word64 Source # 

Methods

witness :: Witness (O n) Word64 Source #

Nat (O n) => Reify (O n) Word32 Source # 

Methods

witness :: Witness (O n) Word32 Source #

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

Methods

witness :: Witness (O n) Word16 Source #

(Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (O n) Word8 Source # 

Methods

witness :: Witness (O n) Word8 Source #

Nat (O n) => Reify (O n) Int Source # 

Methods

witness :: Witness (O n) Int Source #

Nat (O n) => Reify (O n) Integer Source # 
Nat (I n) => Reify (I n) Int64 Source # 

Methods

witness :: Witness (I n) Int64 Source #

Nat (I n) => Reify (I n) Int32 Source # 

Methods

witness :: Witness (I n) Int32 Source #

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

Methods

witness :: Witness (I n) Int16 Source #

(Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (I n) Int8 Source # 

Methods

witness :: Witness (I n) Int8 Source #

Nat (I n) => Reify (I n) Word64 Source # 

Methods

witness :: Witness (I n) Word64 Source #

Nat (I n) => Reify (I n) Word32 Source # 

Methods

witness :: Witness (I n) Word32 Source #

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

Methods

witness :: Witness (I n) Word16 Source #

(Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (I n) Word8 Source # 

Methods

witness :: Witness (I n) Word8 Source #

Nat (I n) => Reify (I n) Int Source # 

Methods

witness :: Witness (I n) Int Source #

Nat (I n) => Reify (I n) Integer Source #