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 | Haskell98 |
TypeLevel.Number.Int
Description
Type level signed integer numbers are implemented using balanced ternary encoding much in the same way as natural numbers.
Currently following operations are supported: Next, Prev, Add, Sub, Mul.
Integer numbers
Digit stream terminator
Instances
IntT ZZ Source # | |
IntT (D1 ZZ) Source # | |
IntT (Dn ZZ) Source # | |
type Normalized ZZ Source # | |
type Negate ZZ Source # | |
type Prev ZZ Source # | |
type Next ZZ Source # | |
type Mul n ZZ Source # | |
type Sub ZZ ZZ Source # | |
type Add ZZ ZZ Source # | |
type Sub ZZ (D1 n) Source # | |
type Sub ZZ (D0 n) Source # | |
type Sub ZZ (Dn n) Source # | |
type Add ZZ (D1 n) Source # | |
type Add ZZ (D0 n) Source # | |
type Add ZZ (Dn n) Source # | |
type Sub (D1 n) ZZ Source # | |
type Sub (D0 n) ZZ Source # | |
type Sub (Dn n) ZZ Source # | |
type Add (D1 n) ZZ Source # | |
type Add (D0 n) ZZ Source # | |
type Add (Dn n) ZZ Source # | |
Digit -1
Instances
IntT (Dn n) => IntT (D1 (Dn n)) Source # | |
IntT (Dn n) => IntT (D0 (Dn n)) Source # | |
IntT (Dn ZZ) Source # | |
IntT (D1 n) => IntT (Dn (D1 n)) Source # | |
IntT (D0 n) => IntT (Dn (D0 n)) Source # | |
IntT (Dn n) => IntT (Dn (Dn n)) Source # | |
type Mul n (Dn m) Source # | |
type Sub ZZ (Dn n) Source # | |
type Add ZZ (Dn n) Source # | |
type Normalized (Dn n) Source # | |
type Negate (Dn n) Source # | |
type Prev (Dn n) Source # | |
type Next (Dn n) Source # | |
type Sub (Dn n) ZZ Source # | |
type Add (Dn n) ZZ Source # | |
type Sub (D1 n) (Dn m) Source # | |
type Sub (D0 n) (Dn m) Source # | |
type Sub (Dn n) (D1 m) Source # | |
type Sub (Dn n) (D0 m) Source # | |
type Sub (Dn n) (Dn m) Source # | |
type Add (D1 n) (Dn m) Source # | |
type Add (D0 n) (Dn m) Source # | |
type Add (Dn n) (D1 m) Source # | |
type Add (Dn n) (D0 m) Source # | |
type Add (Dn n) (Dn m) Source # | |
Digit 0
Instances
IntT (D0 n) => IntT (D1 (D0 n)) Source # | |
IntT (D1 n) => IntT (D0 (D1 n)) Source # | |
IntT (D0 n) => IntT (D0 (D0 n)) Source # | |
IntT (Dn n) => IntT (D0 (Dn n)) Source # | |
IntT (D0 n) => IntT (Dn (D0 n)) Source # | |
type Mul n (D0 m) Source # | |
type Sub ZZ (D0 n) Source # | |
type Add ZZ (D0 n) Source # | |
type Normalized (D0 n) Source # | |
type Negate (D0 n) Source # | |
type Prev (D0 n) Source # | |
type Next (D0 n) Source # | |
type Sub (D0 n) ZZ Source # | |
type Add (D0 n) ZZ Source # | |
type Sub (D1 n) (D0 m) Source # | |
type Sub (D0 n) (D1 m) Source # | |
type Sub (D0 n) (D0 m) Source # | |
type Sub (D0 n) (Dn m) Source # | |
type Sub (Dn n) (D0 m) Source # | |
type Add (D1 n) (D0 m) Source # | |
type Add (D0 n) (D1 m) Source # | |
type Add (D0 n) (D0 m) Source # | |
type Add (D0 n) (Dn m) Source # | |
type Add (Dn n) (D0 m) Source # | |
Digit 1
Instances
IntT (D1 ZZ) Source # | |
IntT (D1 n) => IntT (D1 (D1 n)) Source # | |
IntT (D0 n) => IntT (D1 (D0 n)) Source # | |
IntT (Dn n) => IntT (D1 (Dn n)) Source # | |
IntT (D1 n) => IntT (D0 (D1 n)) Source # | |
IntT (D1 n) => IntT (Dn (D1 n)) Source # | |
type Mul n (D1 m) Source # | |
type Sub ZZ (D1 n) Source # | |
type Add ZZ (D1 n) Source # | |
type Normalized (D1 n) Source # | |
type Negate (D1 n) Source # | |
type Prev (D1 n) Source # | |
type Next (D1 n) Source # | |
type Sub (D1 n) ZZ Source # | |
type Add (D1 n) ZZ Source # | |
type Sub (D1 n) (D1 m) Source # | |
type Sub (D1 n) (D0 m) Source # | |
type Sub (D1 n) (Dn m) Source # | |
type Sub (D0 n) (D1 m) Source # | |
type Sub (Dn n) (D1 m) Source # | |
type Add (D1 n) (D1 m) Source # | |
type Add (D1 n) (D0 m) Source # | |
type Add (D1 n) (Dn m) Source # | |
type Add (D0 n) (D1 m) Source # | |
type Add (Dn n) (D1 m) Source # | |
Type class for type level integers. Only numbers without leading zeroes are members of the class.
Minimal complete definition
Methods
toInt :: Integral i => n -> i Source #
Convert natural number to integral value. It's not checked whether value could be represented.
Instances
IntT ZZ Source # | |
IntT (D1 ZZ) Source # | |
IntT (D1 n) => IntT (D1 (D1 n)) Source # | |
IntT (D0 n) => IntT (D1 (D0 n)) Source # | |
IntT (Dn n) => IntT (D1 (Dn n)) Source # | |
IntT (D1 n) => IntT (D0 (D1 n)) Source # | |
IntT (D0 n) => IntT (D0 (D0 n)) Source # | |
IntT (Dn n) => IntT (D0 (Dn n)) Source # | |
IntT (Dn ZZ) Source # | |
IntT (D1 n) => IntT (Dn (D1 n)) Source # | |
IntT (D0 n) => IntT (Dn (D0 n)) Source # | |
IntT (Dn n) => IntT (Dn (Dn n)) Source # | |
Lifting
withInt :: forall i a. Integral i => (forall n. IntT n => n -> a) -> i -> a Source #
Apply function which could work with any Nat
value only know at runtime.
Template haskell utilities
module TypeLevel.Number.Classes