singleton-typelits-0.0.0.0: Singletons and induction over GHC TypeLits

Copyright(C) 2017 mniip
LicenseMIT
Maintainermniip@mniip.com
Stabilityexperimental
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

GHC.TypeLits.Singletons

Contents

Description

 

Synopsis

Natural number singletons

class NatSingleton (p :: Nat -> *) where Source #

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

Minimal complete definition

natSingleton

Methods

natSingleton :: KnownNat n => p n Source #

data NatIsZero (n :: Nat) where Source #

A natural number is either 0 or 1 plus something.

Constructors

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

data NatPeano (n :: Nat) where Source #

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) 

data NatTwosComp (n :: Nat) where Source #

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

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

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) Source # 

Methods

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

(KnownNat b, NatSingleton p) => NatSingleton (NatBaseComp p b) Source # 
ShowN p => Show (NatBaseComp p b n) Source # 

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 Source #

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

Minimal complete definition

posSingleton

Methods

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

data Unary (n :: Nat) where Source #

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

data PosBinary (n :: Nat) where Source #

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

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

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) Source # 

Methods

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

ShowN p => ShowN (PosBase p b) Source # 

Methods

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

ShowN p => Show (PosBase p b n) Source # 

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 Source #

Auxiliary class for implementing Show on higher-kinded singletons.

Minimal complete definition

showsPrecN

Methods

showsPrecN :: Int -> p n -> ShowS Source #