type-level-numbers-0.1.1.2: Type level numbers implemented using type families.

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 | Haskell2010

TypeLevel.Number.Int

Contents

- Integer numbers
  - Lifting
- Template haskell utilities
- Orphan instances

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

- data ZZ
- data Dn n
- data D0 n
- data D1 n
- class IntT n where
  - toInt :: Integral i => n -> i
- data SomeInt
- withInt :: Integral i => (forall n. IntT n => n -> a) -> i -> a
- intT :: Integer -> TypeQ
- module TypeLevel.Number.Classes

# Integer numbers

data ZZ Source #

Digit stream terminator

#### Instances

Instances details

Show ZZ Source # |
Instance details Defined in TypeLevel.Number.Int Methods showsPrec :: Int -> ZZ -> ShowS Source # show :: ZZ -> String Source # showList :: [ZZ] -> ShowS Source #
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 Normalized ZZ = ZZ
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 Methods showsPrec :: Int -> SomeInt -> ShowS Source # show :: SomeInt -> String Source # showList :: [SomeInt] -> ShowS Source #

withInt :: 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.

module TypeLevel.Number.Classes

# Orphan instances

Show ZZ Source # |
Instance details Methods showsPrec :: Int -> ZZ -> ShowS Source # show :: ZZ -> String Source # showList :: [ZZ] -> ShowS Source #
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 #