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

Contents

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.

Synopsis

Integer numbers

Digit stream terminator

Instances

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

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

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

class IntT n where Source

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

Methods

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

Instances

Lifting

Some natural number

Instances

Show SomeInt
Typeable * SomeInt

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.

Generate type for integer number.