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

data O n 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 

data Z 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 

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