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 #

Digit stream terminator

Instances

IntT ZZ # 

Methods

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

IntT (D1 ZZ) # 

Methods

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

IntT (Dn ZZ) # 

Methods

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

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

data Dn n #

Digit -1

Instances

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

Methods

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

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

Methods

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

IntT (Dn ZZ) # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

data D0 n #

Digit 0

Instances

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

data D1 n #

Digit 1

Instances

IntT (D1 ZZ) # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

class IntT n where #

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 #

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

Instances

IntT ZZ # 

Methods

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

IntT (D1 ZZ) # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

IntT (Dn ZZ) # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

Lifting

data SomeInt #

Some natural number

Instances

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.

Orphan instances

Show ZZ # 

Methods

showsPrec :: Int -> ZZ -> ShowS #

show :: ZZ -> String #

showList :: [ZZ] -> ShowS #

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

Methods

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

show :: D1 n -> String #

showList :: [D1 n] -> ShowS #

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

Methods

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

show :: D0 n -> String #

showList :: [D0 n] -> ShowS #

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

Methods

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

show :: Dn n -> String #

showList :: [Dn n] -> ShowS #