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 = ZZ Source | |
type Negate ZZ = ZZ Source | |
type Prev ZZ = Dn ZZ Source | |
type Next ZZ = D1 ZZ Source | |
type Mul n ZZ = ZZ Source | |
type Sub ZZ ZZ = ZZ Source | |
type Add ZZ ZZ = ZZ Source | |
type Sub ZZ (D1 n) = Negate (D1 n) Source | |
type Sub ZZ (D0 n) = Negate (D0 n) Source | |
type Sub ZZ (Dn n) = Negate (Dn n) Source | |
type Add ZZ (D1 n) = Normalized (D1 n) Source | |
type Add ZZ (D0 n) = Normalized (D0 n) Source | |
type Add ZZ (Dn n) = Normalized (Dn n) Source | |
type Sub (D1 n) ZZ = D1 n Source | |
type Sub (D0 n) ZZ = D0 n Source | |
type Sub (Dn n) ZZ = Dn n Source | |
type Add (D1 n) ZZ = Normalized (D1 n) Source | |
type Add (D0 n) ZZ = Normalized (D0 n) Source | |
type Add (Dn n) ZZ = Normalized (Dn n) 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) = Negate (Dn n) Source | |
type Add ZZ (Dn n) = Normalized (Dn n) Source | |
type Normalized (Dn n) = Dn (Normalized n) Source | |
type Negate (Dn n) = D1 (Negate n) Source | |
type Prev (Dn n) = Normalized (D1 (Prev n)) Source | |
type Next (Dn n) = Normalized (D0 n) Source | |
type Sub (Dn n) ZZ = Dn n Source | |
type Add (Dn n) ZZ = Normalized (Dn n) Source | |
type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m)) Source | |
type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m)) Source | |
type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m)) Source | |
type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m)) Source | |
type Sub (Dn n) (Dn m) = Add (Dn n) (Negate (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) = Normalized (D0 (Mul n m)) Source | |
type Sub ZZ (D0 n) = Negate (D0 n) Source | |
type Add ZZ (D0 n) = Normalized (D0 n) Source | |
type Normalized (D0 n) Source | |
type Negate (D0 n) = D0 (Negate n) Source | |
type Prev (D0 n) = Dn n Source | |
type Next (D0 n) = D1 n Source | |
type Sub (D0 n) ZZ = D0 n Source | |
type Add (D0 n) ZZ = Normalized (D0 n) Source | |
type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m)) Source | |
type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m)) Source | |
type Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m)) Source | |
type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m)) Source | |
type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (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) = Negate (D1 n) Source | |
type Add ZZ (D1 n) = Normalized (D1 n) Source | |
type Normalized (D1 n) = D1 (Normalized n) Source | |
type Negate (D1 n) = Dn (Negate n) Source | |
type Prev (D1 n) = Normalized (D0 n) Source | |
type Next (D1 n) = Normalized (Dn (Next n)) Source | |
type Sub (D1 n) ZZ = D1 n Source | |
type Add (D1 n) ZZ = Normalized (D1 n) Source | |
type Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m)) Source | |
type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m)) Source | |
type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m)) Source | |
type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m)) Source | |
type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (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.
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