Portability | unportable (GHC only) |
---|---|

Stability | unstable |

Maintainer | Alexey Khudyakov <alexey.skladnoy@gmail.com> |

Safe Haskell | None |

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.

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 |

Zero bit.

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 |

Bit stream terminator.

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

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