Copyright	Alexey Khudyakov
License	BSD3-style (see LICENSE)
Maintainer	Alexey Khudyakov <[email protected]>
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 # show :: ZZ -> String # showList :: [ZZ] -> ShowS #
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 # show :: Dn n -> String # showList :: [Dn n] -> ShowS #
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 # show :: D0 n -> String # showList :: [D0 n] -> ShowS #
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 # show :: D1 n -> String # showList :: [D1 n] -> ShowS #
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 # show :: SomeInt -> String # showList :: [SomeInt] -> ShowS #

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 # show :: ZZ -> String # showList :: [ZZ] -> ShowS #
IntT (D0 n) => Show (D0 n) Source #
Instance details Methods showsPrec :: Int -> D0 n -> ShowS # show :: D0 n -> String # showList :: [D0 n] -> ShowS #
IntT (D1 n) => Show (D1 n) Source #
Instance details Methods showsPrec :: Int -> D1 n -> ShowS # show :: D1 n -> String # showList :: [D1 n] -> ShowS #
IntT (Dn n) => Show (Dn n) Source #
Instance details Methods showsPrec :: Int -> Dn n -> ShowS # show :: Dn n -> String # showList :: [Dn n] -> ShowS #