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

data Dn n Source

Digit -1

Instances

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

data D0 n Source

Digit 0

Instances

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

data D1 n Source

Digit 1

Instances

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

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

IntT ZZ Source 
IntT (D1 ZZ) Source 
IntT (D1 n) => IntT (D1 (D1 n)) Source 
IntT (D0 n) => IntT (D1 (D0 n)) Source 
IntT (Dn n) => IntT (D1 (Dn n)) Source 
IntT (D1 n) => IntT (D0 (D1 n)) Source 
IntT (D0 n) => IntT (D0 (D0 n)) Source 
IntT (Dn n) => IntT (D0 (Dn n)) Source 
IntT (Dn ZZ) Source 
IntT (D1 n) => IntT (Dn (D1 n)) Source 
IntT (D0 n) => IntT (Dn (D0 n)) Source 
IntT (Dn n) => IntT (Dn (Dn n)) 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.