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 HaskellNone
LanguageHaskell98

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

data ZZ Source #

Digit stream terminator

Instances

IntT ZZ Source # 

Methods

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

IntT (D1 ZZ) Source # 

Methods

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

IntT (Dn ZZ) Source # 

Methods

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

type Normalized ZZ Source # 
type Negate ZZ Source # 
type Negate ZZ = ZZ
type Prev ZZ Source # 
type Prev ZZ = Dn ZZ
type Next ZZ Source # 
type Next ZZ = D1 ZZ
type Mul n ZZ Source # 
type Mul n ZZ = ZZ
type Sub ZZ ZZ Source # 
type Sub ZZ ZZ = ZZ
type Add ZZ ZZ Source # 
type Add ZZ ZZ = ZZ
type Sub ZZ (D1 n) Source # 
type Sub ZZ (D1 n) = Negate (D1 n)
type Sub ZZ (D0 n) Source # 
type Sub ZZ (D0 n) = Negate (D0 n)
type Sub ZZ (Dn n) Source # 
type Sub ZZ (Dn n) = Negate (Dn n)
type Add ZZ (D1 n) Source # 
type Add ZZ (D1 n) = Normalized (D1 n)
type Add ZZ (D0 n) Source # 
type Add ZZ (D0 n) = Normalized (D0 n)
type Add ZZ (Dn n) Source # 
type Add ZZ (Dn n) = Normalized (Dn n)
type Sub (D1 n) ZZ Source # 
type Sub (D1 n) ZZ = D1 n
type Sub (D0 n) ZZ Source # 
type Sub (D0 n) ZZ = D0 n
type Sub (Dn n) ZZ Source # 
type Sub (Dn n) ZZ = Dn n
type Add (D1 n) ZZ Source # 
type Add (D1 n) ZZ = Normalized (D1 n)
type Add (D0 n) ZZ Source # 
type Add (D0 n) ZZ = Normalized (D0 n)
type Add (Dn n) ZZ Source # 
type Add (Dn n) ZZ = Normalized (Dn n)

data Dn n Source #

Digit -1

Instances

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

Methods

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

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

Methods

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

IntT (Dn ZZ) Source # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

type Mul n (Dn m) Source # 
type Mul n (Dn m)
type Sub ZZ (Dn n) Source # 
type Sub ZZ (Dn n) = Negate (Dn n)
type Add ZZ (Dn n) Source # 
type Add ZZ (Dn n) = Normalized (Dn n)
type Normalized (Dn n) Source # 
type Normalized (Dn n) = Dn (Normalized n)
type Negate (Dn n) Source # 
type Negate (Dn n) = D1 (Negate n)
type Prev (Dn n) Source # 
type Prev (Dn n) = Normalized (D1 (Prev n))
type Next (Dn n) Source # 
type Next (Dn n) = Normalized (D0 n)
type Sub (Dn n) ZZ Source # 
type Sub (Dn n) ZZ = Dn n
type Add (Dn n) ZZ Source # 
type Add (Dn n) ZZ = Normalized (Dn n)
type Sub (D1 n) (Dn m) Source # 
type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
type Sub (D0 n) (Dn m) Source # 
type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type Sub (Dn n) (D1 m) Source # 
type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
type Sub (Dn n) (D0 m) Source # 
type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
type Sub (Dn n) (Dn m) Source # 
type Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))
type Add (D1 n) (Dn m) Source # 
type Add (D1 n) (Dn m)
type Add (D0 n) (Dn m) Source # 
type Add (D0 n) (Dn m)
type Add (Dn n) (D1 m) Source # 
type Add (Dn n) (D1 m)
type Add (Dn n) (D0 m) Source # 
type Add (Dn n) (D0 m)
type Add (Dn n) (Dn m) Source # 
type Add (Dn n) (Dn m)

data D0 n Source #

Digit 0

Instances

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

type Mul n (D0 m) Source # 
type Mul n (D0 m) = Normalized (D0 (Mul n m))
type Sub ZZ (D0 n) Source # 
type Sub ZZ (D0 n) = Negate (D0 n)
type Add ZZ (D0 n) Source # 
type Add ZZ (D0 n) = Normalized (D0 n)
type Normalized (D0 n) Source # 
type Normalized (D0 n)
type Negate (D0 n) Source # 
type Negate (D0 n) = D0 (Negate n)
type Prev (D0 n) Source # 
type Prev (D0 n) = Dn n
type Next (D0 n) Source # 
type Next (D0 n) = D1 n
type Sub (D0 n) ZZ Source # 
type Sub (D0 n) ZZ = D0 n
type Add (D0 n) ZZ Source # 
type Add (D0 n) ZZ = Normalized (D0 n)
type Sub (D1 n) (D0 m) Source # 
type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
type Sub (D0 n) (D1 m) Source # 
type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
type Sub (D0 n) (D0 m) Source # 
type Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
type Sub (D0 n) (Dn m) Source # 
type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type Sub (Dn n) (D0 m) Source # 
type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
type Add (D1 n) (D0 m) Source # 
type Add (D1 n) (D0 m)
type Add (D0 n) (D1 m) Source # 
type Add (D0 n) (D1 m)
type Add (D0 n) (D0 m) Source # 
type Add (D0 n) (D0 m)
type Add (D0 n) (Dn m) Source # 
type Add (D0 n) (Dn m)
type Add (Dn n) (D0 m) Source # 
type Add (Dn n) (D0 m)

data D1 n Source #

Digit 1

Instances

IntT (D1 ZZ) Source # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Minimal complete definition

toInt

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 # 

Methods

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

IntT (D1 ZZ) Source # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

IntT (Dn ZZ) Source # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

Lifting

data SomeInt Source #

Some natural number

Instances

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 # 

Methods

showsPrec :: Int -> ZZ -> ShowS #

show :: ZZ -> String #

showList :: [ZZ] -> ShowS #

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

Methods

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

show :: D1 n -> String #

showList :: [D1 n] -> ShowS #

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

Methods

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

show :: D0 n -> String #

showList :: [D0 n] -> ShowS #

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

Methods

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

show :: Dn n -> String #

showList :: [Dn n] -> ShowS #