TypeLevel.Number.Nat

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

data I n

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

data O n

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

data Z

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)

class Nat n where

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

Methods

toInt :: Integral i => n -> i

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

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

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

Create type for natural number.

nat :: Integer -> ExpQ

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

module TypeLevel.Number.Classes