type-level-numbers-0.1.1.1: Type level numbers implemented using type families.
CopyrightAlexey Khudyakov
LicenseBSD3-style (see LICENSE)
MaintainerAlexey Khudyakov <alexey.skladnoy@gmail.com>
Stabilityunstable
Portabilityunportable (GHC only)
Safe HaskellSafe-Inferred
LanguageHaskell98

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.

Synopsis

Integer numbers

data ZZ Source #

Digit stream terminator

Instances

Instances details
Show ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

IntT ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => ZZ -> i Source #

IntT (D1 ZZ) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 ZZ -> i Source #

IntT (Dn ZZ) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn ZZ -> i Source #

type Negate ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Negate ZZ = ZZ
type Next ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Next ZZ = D1 ZZ
type Normalized ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Prev ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Prev ZZ = Dn ZZ
type Add ZZ ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add ZZ ZZ = ZZ
type Mul n ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Mul n ZZ = ZZ
type Sub ZZ ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub ZZ ZZ = ZZ
type Add ZZ (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add ZZ (D0 n) = Normalized (D0 n)
type Add ZZ (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add ZZ (D1 n) = Normalized (D1 n)
type Add ZZ (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add ZZ (Dn n) = Normalized (Dn n)
type Sub ZZ (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub ZZ (D0 n) = Negate (D0 n)
type Sub ZZ (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub ZZ (D1 n) = Negate (D1 n)
type Sub ZZ (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub ZZ (Dn n) = Negate (Dn n)
type Add (D0 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D0 n) ZZ = Normalized (D0 n)
type Add (D1 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D1 n) ZZ = Normalized (D1 n)
type Add (Dn n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (Dn n) ZZ = Normalized (Dn n)
type Sub (D0 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D0 n) ZZ = D0 n
type Sub (D1 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D1 n) ZZ = D1 n
type Sub (Dn n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (Dn n) ZZ = Dn n

data Dn n Source #

Digit -1

Instances

Instances details
IntT (Dn n) => Show (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

showsPrec :: Int -> Dn n -> ShowS Source #

show :: Dn n -> String Source #

showList :: [Dn n] -> ShowS Source #

IntT (Dn n) => IntT (D0 (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (Dn n) -> i Source #

IntT (Dn n) => IntT (D1 (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (Dn n) -> i Source #

IntT (D0 n) => IntT (Dn (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (D0 n) -> i Source #

IntT (D1 n) => IntT (Dn (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (D1 n) -> i Source #

IntT (Dn n) => IntT (Dn (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (Dn n) -> i Source #

IntT (Dn ZZ) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn ZZ -> i Source #

type Add ZZ (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add ZZ (Dn n) = Normalized (Dn n)
type Mul n (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Mul n (Dn m)
type Sub ZZ (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub ZZ (Dn n) = Negate (Dn n)
type Negate (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Negate (Dn n) = D1 (Negate n)
type Next (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Next (Dn n) = Normalized (D0 n)
type Normalized (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Normalized (Dn n) = Dn (Normalized n)
type Prev (Dn n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Prev (Dn n) = Normalized (D1 (Prev n))
type Add (Dn n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (Dn n) ZZ = Normalized (Dn n)
type Sub (Dn n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (Dn n) ZZ = Dn n
type Add (D0 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D0 n) (Dn m)
type Add (D1 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D1 n) (Dn m)
type Add (Dn n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (Dn n) (D0 m)
type Add (Dn n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (Dn n) (D1 m)
type Add (Dn n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (Dn n) (Dn m)
type Sub (D0 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type Sub (D1 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
type Sub (Dn n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
type Sub (Dn n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
type Sub (Dn n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))

data D0 n Source #

Digit 0

Instances

Instances details
IntT (D0 n) => Show (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

showsPrec :: Int -> D0 n -> ShowS Source #

show :: D0 n -> String Source #

showList :: [D0 n] -> ShowS Source #

IntT (D0 n) => IntT (D0 (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (D0 n) -> i Source #

IntT (D1 n) => IntT (D0 (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (D1 n) -> i Source #

IntT (Dn n) => IntT (D0 (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (Dn n) -> i Source #

IntT (D0 n) => IntT (D1 (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (D0 n) -> i Source #

IntT (D0 n) => IntT (Dn (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (D0 n) -> i Source #

type Add ZZ (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add ZZ (D0 n) = Normalized (D0 n)
type Mul n (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Mul n (D0 m) = Normalized (D0 (Mul n m))
type Sub ZZ (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub ZZ (D0 n) = Negate (D0 n)
type Negate (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Negate (D0 n) = D0 (Negate n)
type Next (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Next (D0 n) = D1 n
type Normalized (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Normalized (D0 n)
type Prev (D0 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Prev (D0 n) = Dn n
type Add (D0 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D0 n) ZZ = Normalized (D0 n)
type Sub (D0 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D0 n) ZZ = D0 n
type Add (D0 n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D0 n) (D0 m)
type Add (D0 n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D0 n) (D1 m)
type Add (D0 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D0 n) (Dn m)
type Add (D1 n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D1 n) (D0 m)
type Add (Dn n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (Dn n) (D0 m)
type Sub (D0 n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
type Sub (D0 n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
type Sub (D0 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type Sub (D1 n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
type Sub (Dn n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))

data D1 n Source #

Digit 1

Instances

Instances details
IntT (D1 n) => Show (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

showsPrec :: Int -> D1 n -> ShowS Source #

show :: D1 n -> String Source #

showList :: [D1 n] -> ShowS Source #

IntT (D1 n) => IntT (D0 (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (D1 n) -> i Source #

IntT (D0 n) => IntT (D1 (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (D0 n) -> i Source #

IntT (D1 n) => IntT (D1 (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (D1 n) -> i Source #

IntT (Dn n) => IntT (D1 (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (Dn n) -> i Source #

IntT (D1 ZZ) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 ZZ -> i Source #

IntT (D1 n) => IntT (Dn (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (D1 n) -> i Source #

type Add ZZ (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add ZZ (D1 n) = Normalized (D1 n)
type Mul n (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Mul n (D1 m)
type Sub ZZ (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub ZZ (D1 n) = Negate (D1 n)
type Negate (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Negate (D1 n) = Dn (Negate n)
type Next (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Next (D1 n) = Normalized (Dn (Next n))
type Normalized (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Normalized (D1 n) = D1 (Normalized n)
type Prev (D1 n) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Prev (D1 n) = Normalized (D0 n)
type Add (D1 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D1 n) ZZ = Normalized (D1 n)
type Sub (D1 n) ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D1 n) ZZ = D1 n
type Add (D0 n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D0 n) (D1 m)
type Add (D1 n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D1 n) (D0 m)
type Add (D1 n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D1 n) (D1 m)
type Add (D1 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (D1 n) (Dn m)
type Add (Dn n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Add (Dn n) (D1 m)
type Sub (D0 n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
type Sub (D1 n) (D0 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
type Sub (D1 n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))
type Sub (D1 n) (Dn m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
type Sub (Dn n) (D1 m) Source # 
Instance details

Defined in TypeLevel.Number.Int

type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))

class IntT n where 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

Instances details
IntT ZZ Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => ZZ -> i Source #

IntT (D0 n) => IntT (D0 (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (D0 n) -> i Source #

IntT (D1 n) => IntT (D0 (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (D1 n) -> i Source #

IntT (Dn n) => IntT (D0 (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D0 (Dn n) -> i Source #

IntT (D0 n) => IntT (D1 (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (D0 n) -> i Source #

IntT (D1 n) => IntT (D1 (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (D1 n) -> i Source #

IntT (Dn n) => IntT (D1 (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 (Dn n) -> i Source #

IntT (D1 ZZ) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => D1 ZZ -> i Source #

IntT (D0 n) => IntT (Dn (D0 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (D0 n) -> i Source #

IntT (D1 n) => IntT (Dn (D1 n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (D1 n) -> i Source #

IntT (Dn n) => IntT (Dn (Dn n)) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn (Dn n) -> i Source #

IntT (Dn ZZ) Source # 
Instance details

Defined in TypeLevel.Number.Int

Methods

toInt :: Integral i => Dn ZZ -> i Source #

Lifting

data SomeInt Source #

Some natural number

Instances

Instances details
Show SomeInt Source # 
Instance details

Defined in TypeLevel.Number.Int

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

intT :: Integer -> TypeQ Source #

Generate type for integer number.

Orphan instances

Show ZZ Source # 
Instance details

IntT (D0 n) => Show (D0 n) Source # 
Instance details

Methods

showsPrec :: Int -> D0 n -> ShowS Source #

show :: D0 n -> String Source #

showList :: [D0 n] -> ShowS Source #

IntT (D1 n) => Show (D1 n) Source # 
Instance details

Methods

showsPrec :: Int -> D1 n -> ShowS Source #

show :: D1 n -> String Source #

showList :: [D1 n] -> ShowS Source #

IntT (Dn n) => Show (Dn n) Source # 
Instance details

Methods

showsPrec :: Int -> Dn n -> ShowS Source #

show :: Dn n -> String Source #

showList :: [Dn n] -> ShowS Source #