TypeLevel.Number.Int

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

data ZZ

Digit stream terminator

Instances

Show ZZ

IntT ZZ

IntT (D1 ZZ)

IntT (Dn ZZ)

data Dn n

Digit -1

Instances

IntT (Dn n) => Show (Dn n)

IntT (Dn n) => IntT (D1 (Dn n))

IntT (Dn n) => IntT (D0 (Dn n))

IntT (Dn ZZ)

IntT (D1 n) => IntT (Dn (D1 n))

IntT (D0 n) => IntT (Dn (D0 n))

IntT (Dn n) => IntT (Dn (Dn n))

data D0 n

Digit 0

Instances

IntT (D0 n) => Show (D0 n)

IntT (D0 n) => IntT (D1 (D0 n))

IntT (D1 n) => IntT (D0 (D1 n))

IntT (D0 n) => IntT (D0 (D0 n))

IntT (Dn n) => IntT (D0 (Dn n))

IntT (D0 n) => IntT (Dn (D0 n))

data D1 n

Digit 1

Instances

IntT (D1 n) => Show (D1 n)

IntT (D1 ZZ)

IntT (D1 n) => IntT (D1 (D1 n))

IntT (D0 n) => IntT (D1 (D0 n))

IntT (Dn n) => IntT (D1 (Dn n))

IntT (D1 n) => IntT (D0 (D1 n))

IntT (D1 n) => IntT (Dn (D1 n))

class IntT n where

Type class for type level integers. Only numbers without leading zeroes are members of the class.

Methods

toInt :: Integral i => n -> i

Convert natural number to integral value. It's not checked whether value could be represented.

Instances

IntT ZZ

IntT (D1 ZZ)

IntT (D1 n) => IntT (D1 (D1 n))

IntT (D0 n) => IntT (D1 (D0 n))

IntT (Dn n) => IntT (D1 (Dn n))

IntT (D1 n) => IntT (D0 (D1 n))

IntT (D0 n) => IntT (D0 (D0 n))

IntT (Dn n) => IntT (D0 (Dn n))

IntT (Dn ZZ)

IntT (D1 n) => IntT (Dn (D1 n))

IntT (D0 n) => IntT (Dn (D0 n))

IntT (Dn n) => IntT (Dn (Dn n))

Lifting

data SomeInt

Some natural number

Instances

Show SomeInt

Typeable SomeInt

withInt :: forall i a. Integral i => (forall n. IntT n => n -> a) -> i -> a

Apply function which could work with any Nat value only know at runtime.

Template haskell utilities

intT :: Integer -> TypeQ

Generate type for integer number.

module TypeLevel.Number.Classes