GHC.TypeLits.Singletons

Natural number singletons

class NatSingleton p where

A class of singletons capable of representing any KnownNat natural number.

Minimal complete definition

natSingleton

Methods

natSingleton :: KnownNat n => p n

Instances

NatSingleton NatTwosComp

Methods

natSingleton :: KnownNat n => NatTwosComp n

NatSingleton NatPeano

Methods

natSingleton :: KnownNat n => NatPeano n

NatSingleton NatIsZero

Methods

natSingleton :: KnownNat n => NatIsZero n

NatSingleton (Proxy Nat)

Methods

natSingleton :: KnownNat n => Proxy Nat n

(KnownNat b, NatSingleton p) => NatSingleton (NatBaseComp p b)

Methods

natSingleton :: KnownNat n => NatBaseComp p b n

data NatIsZero n where

A natural number is either 0 or 1 plus something.

Constructors

IsZero :: NatIsZero 0

IsNonZero :: KnownNat n => NatIsZero (1 + n)

Instances

ShowN NatIsZero

Methods

showsPrecN :: Int -> NatIsZero n -> ShowS

NatSingleton NatIsZero

Methods

natSingleton :: KnownNat n => NatIsZero n

Show (NatIsZero n)

Methods

showsPrec :: Int -> NatIsZero n -> ShowS

show :: NatIsZero n -> String

showList :: [NatIsZero n] -> ShowS

data NatPeano n where

A natural number is either 0 or a successor of another natural number.

Constructors

PeanoZero :: NatPeano 0

PeanoSucc :: KnownNat n => NatPeano n -> NatPeano (1 + n)

Instances

ShowN NatPeano

Methods

showsPrecN :: Int -> NatPeano n -> ShowS

NatSingleton NatPeano

Methods

natSingleton :: KnownNat n => NatPeano n

Show (NatPeano n)

Methods

showsPrec :: Int -> NatPeano n -> ShowS

show :: NatPeano n -> String

showList :: [NatPeano n] -> ShowS

data NatTwosComp n where

A natural number is either 0, or twice another natural number plus 1 or 2.

Constructors

TwosCompZero :: NatTwosComp 0

TwosCompx2p1 :: KnownNat n => NatTwosComp n -> NatTwosComp (1 + (2 * n))

TwosCompx2p2 :: KnownNat n => NatTwosComp n -> NatTwosComp (2 + (2 * n))

Instances

ShowN NatTwosComp

Methods

showsPrecN :: Int -> NatTwosComp n -> ShowS

NatSingleton NatTwosComp

Methods

natSingleton :: KnownNat n => NatTwosComp n

Show (NatTwosComp n)

Methods

showsPrec :: Int -> NatTwosComp n -> ShowS

show :: NatTwosComp n -> String

showList :: [NatTwosComp n] -> ShowS

data NatBaseComp p b n where

A natural number is either 0, or b times another natural number plus a digit in [1, b].

Constructors

BaseCompZero :: NatBaseComp p b 0

BaseCompxBp1p :: (KnownNat k, (1 + k) <= b, KnownNat n) => p k -> NatBaseComp p b n -> NatBaseComp p b ((1 + k) + (b * n))

Instances

ShowN p => ShowN (NatBaseComp p b)

Methods

showsPrecN :: Int -> NatBaseComp p b n -> ShowS

(KnownNat b, NatSingleton p) => NatSingleton (NatBaseComp p b)

Methods

natSingleton :: KnownNat n => NatBaseComp p b n

ShowN p => Show (NatBaseComp p b n)

Methods

showsPrec :: Int -> NatBaseComp p b n -> ShowS

show :: NatBaseComp p b n -> String

showList :: [NatBaseComp p b n] -> ShowS

Positive number singleton

class PositiveSingleton p where

A class of singletons capable of representing postive KnownNat natural numbers.

Minimal complete definition

posSingleton

Methods

posSingleton :: KnownNat n => p (1 + n)

Instances

PositiveSingleton PosBinary

Methods

posSingleton :: KnownNat n => PosBinary (1 + n)

PositiveSingleton Unary

Methods

posSingleton :: KnownNat n => Unary (1 + n)

PositiveSingleton (Proxy Nat)

Methods

posSingleton :: KnownNat n => Proxy Nat (1 + n)

(KnownNat b, NatSingleton p) => PositiveSingleton (PosBase p b)

Methods

posSingleton :: KnownNat n => PosBase p b (1 + n)

data Unary n where

A positive number is either 1 or a successor of another positive number.

Constructors

UnaryOne :: Unary 1

UnarySucc :: KnownNat n => Unary n -> Unary (1 + n)

Instances

PositiveSingleton Unary

Methods

posSingleton :: KnownNat n => Unary (1 + n)

ShowN Unary

Methods

showsPrecN :: Int -> Unary n -> ShowS

Show (Unary n)

Methods

showsPrec :: Int -> Unary n -> ShowS

show :: Unary n -> String

showList :: [Unary n] -> ShowS

data PosBinary n where

A positive number is either 1, or twice another positive number plus 0 or 1.

Constructors

BinOne :: PosBinary 1

Bin0 :: KnownNat n => PosBinary n -> PosBinary (2 * n)

Bin1 :: KnownNat n => PosBinary n -> PosBinary (1 + (2 * n))

Instances

PositiveSingleton PosBinary

Methods

posSingleton :: KnownNat n => PosBinary (1 + n)

ShowN PosBinary

Methods

showsPrecN :: Int -> PosBinary n -> ShowS

Show (PosBinary n)

Methods

showsPrec :: Int -> PosBinary n -> ShowS

show :: PosBinary n -> String

showList :: [PosBinary n] -> ShowS

data PosBase p b n where

A positive number is either a digit in [1, b), or another positive number times b plus a digit in [0, b).

Constructors

BaseLead :: (KnownNat k, (1 + k) <= b, k ~ (1 + n)) => p k -> PosBase p b k

BaseDigit :: (KnownNat k, (1 + k) <= b, KnownNat n) => p k -> PosBase p b n -> PosBase p b (k + (b * n))

Instances

(KnownNat b, NatSingleton p) => PositiveSingleton (PosBase p b)

Methods

posSingleton :: KnownNat n => PosBase p b (1 + n)

ShowN p => ShowN (PosBase p b)

Methods

showsPrecN :: Int -> PosBase p b n -> ShowS

ShowN p => Show (PosBase p b n)

Methods

showsPrec :: Int -> PosBase p b n -> ShowS

show :: PosBase p b n -> String

showList :: [PosBase p b n] -> ShowS

class ShowN p where

Auxiliary class for implementing Show on higher-kinded singletons.

Minimal complete definition

showsPrecN

Methods

showsPrecN :: Int -> p n -> ShowS

Instances

ShowN PosBinary

Methods

showsPrecN :: Int -> PosBinary n -> ShowS

ShowN Unary

Methods

showsPrecN :: Int -> Unary n -> ShowS

ShowN NatTwosComp

Methods

showsPrecN :: Int -> NatTwosComp n -> ShowS

ShowN NatPeano

Methods

showsPrecN :: Int -> NatPeano n -> ShowS

ShowN NatIsZero

Methods

showsPrecN :: Int -> NatIsZero n -> ShowS

ShowN (Proxy Nat)

Methods

showsPrecN :: Int -> Proxy Nat n -> ShowS

ShowN p => ShowN (PosBase p b)

Methods

showsPrecN :: Int -> PosBase p b n -> ShowS

ShowN p => ShowN (NatBaseComp p b)

Methods

showsPrecN :: Int -> NatBaseComp p b n -> ShowS