GHC.TypeLits.Singletons

Natural number singletons

class NatSingleton (p :: Nat -> *) 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

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatTwosComp n

NatSingleton NatPeano

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatPeano n

NatSingleton NatIsZero

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatIsZero n

NatSingleton (Proxy :: Nat -> *)

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => Proxy n

(KnownNat b, b ~ (1 + c), NatSingleton p) => NatSingleton (NatBaseComp p b)

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatBaseComp p b n

data NatIsZero (n :: Nat) where

A natural number is either 0 or 1 plus something.

Constructors

IsZero :: NatIsZero 0

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

Instances

ShowN NatIsZero

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> NatIsZero n -> ShowS

NatSingleton NatIsZero

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatIsZero n

Show (NatIsZero n)

Defined in GHC.TypeLits.Singletons

Methods

showsPrec :: Int -> NatIsZero n -> ShowS

show :: NatIsZero n -> String

showList :: [NatIsZero n] -> ShowS

data NatPeano (n :: Nat) where

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

For example, 3 = 1 + (1 + (1 + 0)):

PeanoSucc (PeanoSucc (PeanoSucc PeanoZero)) :: NatPeano 3

Constructors

PeanoZero :: NatPeano 0

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

Instances

ShowN NatPeano

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> NatPeano n -> ShowS

NatSingleton NatPeano

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatPeano n

Show (NatPeano n)

Defined in GHC.TypeLits.Singletons

Methods

showsPrec :: Int -> NatPeano n -> ShowS

show :: NatPeano n -> String

showList :: [NatPeano n] -> ShowS

data NatTwosComp (n :: Nat) where

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

For example, 12 = 2 + 2 * (1 + 2 * (2 + 2 * 0)):

TwosCompx2p2 (TwosCompx2p1 (TwosCompx2p2 TwosCompZero)) :: NatTwosComp 12

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

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> NatTwosComp n -> ShowS

NatSingleton NatTwosComp

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatTwosComp n

Show (NatTwosComp n)

Defined in GHC.TypeLits.Singletons

Methods

showsPrec :: Int -> NatTwosComp n -> ShowS

show :: NatTwosComp n -> String

showList :: [NatTwosComp n] -> ShowS

data NatBaseComp (p :: Nat -> *) (b :: Nat) (n :: Nat) where

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

For example, 123 = (2 + 1) + 10 * ((1 + 1) + 10 * ((0 + 1) + 10 * 0)):

BaseCompxBp1p (natSingleton :: p 2) (BaseCompxBp1p (natSingleton :: p 1) (BaseCompxBp1p (natSingleton :: p 0) BaseCompZero)) :: NatBaseComp p 10 123

Constructors

BaseCompZero :: (KnownNat b, b ~ (1 + c)) => NatBaseComp p b 0

BaseCompxBp1p :: (KnownNat b, b ~ (1 + c), 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)

Defined in GHC.TypeLits.Singletons

Methods

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

(KnownNat b, b ~ (1 + c), NatSingleton p) => NatSingleton (NatBaseComp p b)

Defined in GHC.TypeLits.Singletons

Methods

natSingleton :: KnownNat n => NatBaseComp p b n

ShowN p => Show (NatBaseComp p b n)

Defined in GHC.TypeLits.Singletons

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 :: Nat -> *) 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

Defined in GHC.TypeLits.Singletons

Methods

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

PositiveSingleton Unary

Defined in GHC.TypeLits.Singletons

Methods

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

PositiveSingleton (Proxy :: Nat -> *)

Defined in GHC.TypeLits.Singletons

Methods

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

(KnownNat b, b ~ (2 + c), NatSingleton p) => PositiveSingleton (PosBase p b)

Defined in GHC.TypeLits.Singletons

Methods

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

data Unary (n :: Nat) where

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

For example, 5 = 1 + (1 + (1 + (1 + 1))):

UnarySucc (UnarySucc (UnarySucc (UnarySucc UnaryOne))) :: Unary 5

Constructors

UnaryOne :: Unary 1

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

Instances

PositiveSingleton Unary

Defined in GHC.TypeLits.Singletons

Methods

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

ShowN Unary

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> Unary n -> ShowS

Show (Unary n)

Defined in GHC.TypeLits.Singletons

Methods

showsPrec :: Int -> Unary n -> ShowS

show :: Unary n -> String

showList :: [Unary n] -> ShowS

data PosBinary (n :: Nat) where

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

For example, 10 = 0 + 2 * (1 + 2 * (0 + 2 * 1)):

Bin0 (Bin1 (Bin0 BinOne)) :: PosBinary 10

Constructors

BinOne :: PosBinary 1

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

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

Instances

PositiveSingleton PosBinary

Defined in GHC.TypeLits.Singletons

Methods

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

ShowN PosBinary

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> PosBinary n -> ShowS

Show (PosBinary n)

Defined in GHC.TypeLits.Singletons

Methods

showsPrec :: Int -> PosBinary n -> ShowS

show :: PosBinary n -> String

showList :: [PosBinary n] -> ShowS

data PosBase (p :: Nat -> *) (b :: Nat) (n :: Nat) where

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

For example, 123 = 3 + 10 * (2 + 10 * 1):

BaseDigit (natSingleton :: p 3) (BaseDigit (natSingleton :: p 2) (BaseLead (natSingleton :: p 1))) :: PosBase p 10 123

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, b ~ (2 + c), NatSingleton p) => PositiveSingleton (PosBase p b)

Defined in GHC.TypeLits.Singletons

Methods

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

ShowN p => ShowN (PosBase p b)

Defined in GHC.TypeLits.Singletons

Methods

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

ShowN p => Show (PosBase p b n)

Defined in GHC.TypeLits.Singletons

Methods

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

show :: PosBase p b n -> String

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

class ShowN (p :: Nat -> *) where

Auxiliary class for implementing Show on higher-kinded singletons.

Minimal complete definition

showsPrecN

Methods

showsPrecN :: Int -> p n -> ShowS

Instances

ShowN PosBinary

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> PosBinary n -> ShowS

ShowN Unary

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> Unary n -> ShowS

ShowN NatTwosComp

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> NatTwosComp n -> ShowS

ShowN NatPeano

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> NatPeano n -> ShowS

ShowN NatIsZero

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> NatIsZero n -> ShowS

ShowN (Proxy :: Nat -> *)

Defined in GHC.TypeLits.Singletons

Methods

showsPrecN :: Int -> Proxy n -> ShowS

ShowN p => ShowN (PosBase p b)

Defined in GHC.TypeLits.Singletons

Methods

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

ShowN p => ShowN (NatBaseComp p b)

Defined in GHC.TypeLits.Singletons

Methods

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