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

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

TypeLevel.Number.Nat

Contents

- Natural numbers
  - Lifting
- Template haskell utilities
- Orphan instances

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

- data I n
- data O n
- data Z
- class Nat n where
  - toInt :: Integral i => n -> i
- data SomeNat where
  - SomeNat :: forall n. Nat n => n -> SomeNat
- withNat :: Integral i => (forall n. Nat n => n -> a) -> i -> a
- natT :: Integer -> TypeQ
- nat :: Integer -> ExpQ
- module TypeLevel.Number.Classes

# Natural numbers

data I n Source #

One bit.

#### Instances

Instances details

Nat (I n) => Show (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods showsPrec :: Int -> I n -> ShowS Source # show :: I n -> String Source # showList :: [I n] -> ShowS Source #
Nat (I n) => NonZero (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat
Nat (I n) => Positive (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat
Nat (I n) => Nat (I (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I (I n) -> i Source #
Nat (O n) => Nat (I (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I (O n) -> i Source #
Nat (I Z) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I Z -> i Source #
Nat (I n) => Nat (O (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O (I n) -> i 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 # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Int16 Source #
Nat (I n) => Reify (I n) Int32 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Int32 Source #
Nat (I n) => Reify (I n) Int64 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Int64 Source #
(Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (I n) Int8 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Int8 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 # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Word16 Source #
Nat (I n) => Reify (I n) Word32 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Word32 Source #
Nat (I n) => Reify (I n) Word64 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Word64 Source #
(Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (I n) Word8 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Word8 Source #
Nat (I n) => Reify (I n) Integer Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Integer Source #
Nat (I n) => Reify (I n) Int Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (I n) Int Source #
type Add Z (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z (I n)
type Compare Z (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z (I n) = IsLesser
type Mul n (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Mul n (I m)
type Next (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Next (I n) = O (Next n)
type Normalized (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Normalized (I n) = I (Normalized n)
type Prev (I (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I (I n)) = O (I n)
type Prev (I (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I (O n)) = O (O n)
type Prev (I Z) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I Z) = Z
type Prev (O (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (O (I n)) = I (Prev (I n))
type Add (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) Z
type Compare (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) Z = IsGreater
type Sub (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) Z
type Add (I n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) (I m)
type Add (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) (O m)
type Add (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) (I m)
type Compare (I n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) (I m) = Compare n m
type Compare (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) (O m)
type Compare (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) (I m)
type Sub (I n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) (I m)
type Sub (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) (O m)
type Sub (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) (I m)

data O n Source #

Zero bit.

#### Instances

Instances details

Nat (O n) => Show (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods showsPrec :: Int -> O n -> ShowS Source # show :: O n -> String Source # showList :: [O n] -> ShowS Source #
Nat (O n) => NonZero (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat
Nat (O n) => Positive (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat
Nat (O n) => Nat (I (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I (O n) -> i Source #
Nat (I n) => Nat (O (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O (I n) -> i Source #
Nat (O n) => Nat (O (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O (O n) -> i Source #
Number_Is_Denormalized Z => Nat (O Z) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O Z -> i 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 # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Int16 Source #
Nat (O n) => Reify (O n) Int32 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Int32 Source #
Nat (O n) => Reify (O n) Int64 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Int64 Source #
(Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (O n) Int8 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Int8 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 # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Word16 Source #
Nat (O n) => Reify (O n) Word32 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Word32 Source #
Nat (O n) => Reify (O n) Word64 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Word64 Source #
(Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (O n) Word8 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Word8 Source #
Nat (O n) => Reify (O n) Integer Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Integer Source #
Nat (O n) => Reify (O n) Int Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness (O n) Int Source #
type Add Z (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z (O n)
type Compare Z (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z (O n) = IsLesser
type Mul n (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Mul n (O m) = Normalized (O (Mul n m))
type Next (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Next (O n) = I n
type Normalized (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Normalized (O n)
type Prev (I (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I (O n)) = O (O n)
type Prev (O (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (O (I n)) = I (Prev (I n))
type Prev (O (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (O (O n)) = I (Prev (O n))
type Add (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) Z
type Compare (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) Z = IsGreater
type Sub (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) Z
type Add (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) (O m)
type Add (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) (I m)
type Add (O n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) (O m)
type Compare (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) (O m)
type Compare (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) (I m)
type Compare (O n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) (O m) = Compare n m
type Sub (I n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) (O m)
type Sub (O n) (I m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) (I m)
type Sub (O n) (O m) Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) (O m)

data Z Source #

Bit stream terminator.

#### Instances

Instances details

Show Z Source # |
Instance details Defined in TypeLevel.Number.Nat Methods showsPrec :: Int -> Z -> ShowS Source # show :: Z -> String Source # showList :: [Z] -> ShowS Source #
Nat Z Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => Z -> i Source #
Reify Z Int16 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Int16 Source #
Reify Z Int32 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Int32 Source #
Reify Z Int64 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Int64 Source #
Reify Z Int8 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Int8 Source #
Reify Z Word16 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Word16 Source #
Reify Z Word32 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Word32 Source #
Reify Z Word64 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Word64 Source #
Reify Z Word8 Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Word8 Source #
Reify Z Integer Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Integer Source #
Reify Z Int Source # |
Instance details Defined in TypeLevel.Number.Nat Methods witness :: Witness Z Int Source #
Nat (I Z) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I Z -> i Source #
Number_Is_Denormalized Z => Nat (O Z) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O Z -> i Source #
type Next Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Next Z = I Z
type Normalized Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Normalized Z = Z
type Add Z Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z Z
type Compare Z Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z Z = IsEqual
type Mul n Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Mul n Z = Z
type Sub Z Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub Z Z
type Add Z (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z (I n)
type Add Z (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Add Z (O n)
type Compare Z (I n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z (I n) = IsLesser
type Compare Z (O n) Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare Z (O n) = IsLesser
type Prev (I Z) Source # |
Instance details Defined in TypeLevel.Number.Nat type Prev (I Z) = Z
type Add (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (I n) Z
type Add (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Add (O n) Z
type Compare (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) Z = IsGreater
type Compare (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) Z = IsGreater
type Sub (I n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) Z
type Sub (O n) Z Source # |
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) Z

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

Instances details

Nat Z Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => Z -> i Source #
Nat (I n) => Nat (I (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I (I n) -> i Source #
Nat (O n) => Nat (I (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I (O n) -> i Source #
Nat (I Z) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => I Z -> i Source #
Nat (I n) => Nat (O (I n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O (I n) -> i Source #
Nat (O n) => Nat (O (O n)) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O (O n) -> i Source #
Number_Is_Denormalized Z => Nat (O Z) Source # |
Instance details Defined in TypeLevel.Number.Nat Methods toInt :: Integral i => O Z -> i Source #

## Lifting

data SomeNat where Source #

Some natural number

Constructors

SomeNat :: forall n. Nat n => n -> SomeNat |

#### Instances

Instances details

Show SomeNat Source # |
Instance details Defined in TypeLevel.Number.Nat Methods showsPrec :: Int -> SomeNat -> ShowS Source # show :: SomeNat -> String Source # showList :: [SomeNat] -> ShowS Source #

withNat :: 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.

module TypeLevel.Number.Classes

# Orphan instances

Show Z Source # |
Instance details Methods showsPrec :: Int -> Z -> ShowS Source # show :: Z -> String Source # showList :: [Z] -> ShowS Source #
Reify Z Int16 Source # |
Instance details Methods witness :: Witness Z Int16 Source #
Reify Z Int32 Source # |
Instance details Methods witness :: Witness Z Int32 Source #
Reify Z Int64 Source # |
Instance details Methods witness :: Witness Z Int64 Source #
Reify Z Int8 Source # |
Instance details Methods witness :: Witness Z Int8 Source #
Reify Z Word16 Source # |
Instance details Methods witness :: Witness Z Word16 Source #
Reify Z Word32 Source # |
Instance details Methods witness :: Witness Z Word32 Source #
Reify Z Word64 Source # |
Instance details Methods witness :: Witness Z Word64 Source #
Reify Z Word8 Source # |
Instance details Methods witness :: Witness Z Word8 Source #
Reify Z Integer Source # |
Instance details Methods witness :: Witness Z Integer Source #
Reify Z Int Source # |
Instance details Methods witness :: Witness Z Int Source #
Nat (I n) => Show (I n) Source # |
Instance details Methods showsPrec :: Int -> I n -> ShowS Source # show :: I n -> String Source # showList :: [I n] -> ShowS Source #
Nat (O n) => Show (O n) Source # |
Instance details Methods showsPrec :: Int -> O n -> ShowS Source # show :: O n -> String Source # showList :: [O n] -> ShowS Source #
Nat (I n) => NonZero (I n) Source # |
Instance details
Nat (O n) => NonZero (O n) Source # |
Instance details
Nat (I n) => Positive (I n) Source # |
Instance details
Nat (O n) => Positive (O n) Source # |
Instance details
(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 # |
Instance details Methods witness :: Witness (I n) Int16 Source #
Nat (I n) => Reify (I n) Int32 Source # |
Instance details Methods witness :: Witness (I n) Int32 Source #
Nat (I n) => Reify (I n) Int64 Source # |
Instance details Methods witness :: Witness (I n) Int64 Source #
(Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (I n) Int8 Source # |
Instance details Methods witness :: Witness (I n) Int8 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 # |
Instance details Methods witness :: Witness (I n) Word16 Source #
Nat (I n) => Reify (I n) Word32 Source # |
Instance details Methods witness :: Witness (I n) Word32 Source #
Nat (I n) => Reify (I n) Word64 Source # |
Instance details Methods witness :: Witness (I n) Word64 Source #
(Nat (I n), Lesser (I n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (I n) Word8 Source # |
Instance details Methods witness :: Witness (I n) Word8 Source #
Nat (I n) => Reify (I n) Integer Source # |
Instance details Methods witness :: Witness (I n) Integer Source #
Nat (I n) => Reify (I n) Int Source # |
Instance details Methods witness :: Witness (I n) Int 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 # |
Instance details Methods witness :: Witness (O n) Int16 Source #
Nat (O n) => Reify (O n) Int32 Source # |
Instance details Methods witness :: Witness (O n) Int32 Source #
Nat (O n) => Reify (O n) Int64 Source # |
Instance details Methods witness :: Witness (O n) Int64 Source #
(Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (I Z))))))))) => Reify (O n) Int8 Source # |
Instance details Methods witness :: Witness (O n) Int8 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 # |
Instance details Methods witness :: Witness (O n) Word16 Source #
Nat (O n) => Reify (O n) Word32 Source # |
Instance details Methods witness :: Witness (O n) Word32 Source #
Nat (O n) => Reify (O n) Word64 Source # |
Instance details Methods witness :: Witness (O n) Word64 Source #
(Nat (O n), Lesser (O n) (O (O (O (O (O (O (O (O (I Z)))))))))) => Reify (O n) Word8 Source # |
Instance details Methods witness :: Witness (O n) Word8 Source #
Nat (O n) => Reify (O n) Integer Source # |
Instance details Methods witness :: Witness (O n) Integer Source #
Nat (O n) => Reify (O n) Int Source # |
Instance details Methods witness :: Witness (O n) Int Source #