Safe Haskell	Safe
Language	Haskell2010

Data.Type.Nat

Contents

Natural, Nat numbers
Showing
Singleton
Implicit
Induction
Arithmetic
Aliases
- Nat
- promoted Nat
Proofs

Description

Nat numbers. DataKinds stuff.

This module re-exports Data.Nat, and adds type-level things.

Synopsis

Natural, Nat numbers

data Nat Source #

Nat natural numbers.

Better than GHC's built-in Nat for some use cases.

Constructors

Z
S Nat

Instances

Enum Nat Source #
Methods succ :: Nat -> Nat # pred :: Nat -> Nat # toEnum :: Int -> Nat # fromEnum :: Nat -> Int # enumFrom :: Nat -> [Nat] # enumFromThen :: Nat -> Nat -> [Nat] # enumFromTo :: Nat -> Nat -> [Nat] # enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #
Eq Nat Source #
Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Integral Nat Source #
Methods quot :: Nat -> Nat -> Nat # rem :: Nat -> Nat -> Nat # div :: Nat -> Nat -> Nat # mod :: Nat -> Nat -> Nat # quotRem :: Nat -> Nat -> (Nat, Nat) # divMod :: Nat -> Nat -> (Nat, Nat) # toInteger :: Nat -> Integer #
Data Nat Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat # toConstr :: Nat -> Constr # dataTypeOf :: Nat -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Nat) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat) # gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r # gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #
Num Nat Source #
Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat Source #
Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Real Nat Source #
Methods toRational :: Nat -> Rational #
Show Nat Source #	`Nat` is printed as `Natural`. To see explicit structure, use `explicitShow` or `explicitShowsPrec`
Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
NFData Nat Source #
Methods rnf :: Nat -> () #
Hashable Nat Source #
Methods hashWithSalt :: Int -> Nat -> Int # hash :: Nat -> Int #

toNatural :: Nat -> Natural Source #

Convert Nat to Natural

>>> toNatural 0
0

>>> toNatural 2
2

>>> toNatural $ S $ S $ Z
2

fromNatural :: Natural -> Nat Source #

Convert Natural to Nat

>>> fromNatural 4
4

>>> explicitShow (fromNatural 4)
"S (S (S (S Z)))"

cata :: a -> (a -> a) -> Nat -> a Source #

Fold Nat.

>>> cata [] ('x' :) 2
"xx"

Showing

explicitShow :: Nat -> String Source #

show displaying a structure of Nat.

>>> explicitShow 0
"Z"

>>> explicitShow 2
"S (S Z)"

explicitShowsPrec :: Int -> Nat -> ShowS Source #

showsPrec displaying a structure of Nat.

Singleton

data SNat n where Source #

Singleton of Nat.

Constructors

SZ :: SNat Z
SS :: SNatI n => SNat (S n)

Instances

Show (SNat p) Source #
Methods showsPrec :: Int -> SNat p -> ShowS # show :: SNat p -> String # showList :: [SNat p] -> ShowS #

snatToNat :: forall n. SNat n -> Nat Source #

Convert SNat to Nat.

>>> snatToNat (snat :: SNat One)
1

snatToNatural :: forall n. SNat n -> Natural Source #

Convert SNat to Natural

>>> snatToNatural (snat :: SNat Zero)
0

>>> snatToNatural (snat :: SNat Two)
2

Implicit

class SNatI n where Source #

Convenience class to get SNat.

Minimal complete definition

snat

Methods

snat :: SNat n Source #

Instances

SNatI Z Source #
Methods snat :: SNat Z Source #
SNatI n => SNatI (S n) Source #
Methods snat :: SNat (S n) Source #

reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r Source #

Reify Nat.

>>> reify three reflect
3

reflect :: forall n proxy. SNatI n => proxy n -> Nat Source #

Reflect type-level Nat to the term level.

reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m Source #

As reflect but with any Num.

Induction

induction Source #

Arguments

:: SNatI n
=> f Z	zero case
-> (forall m. SNatI m => f m -> f (S m))	induction step
-> f n

Induction on Nat.

Useful in proofs or with GADTs, see source of proofPlusNZero.

induction1 Source #

Arguments

:: SNatI n
=> f Z a	zero case
-> (forall m. SNatI m => f m a -> f (S m) a)	induction step
-> f n a

Induction on Nat, functor form. Useful for computation.

>>> induction1 (Tagged 0) $ retagMap (+2) :: Tagged Three Int
Tagged 6

class SNatI n => InlineInduction n where Source #

The induction will be fully inlined.

See test/Inspection.hs.

Minimal complete definition

inlineInduction1

Methods

inlineInduction1 :: f Z a -> (forall m. SNatI m => f m a -> f (S m) a) -> f n a Source #

Instances

InlineInduction Z Source #
Methods inlineInduction1 :: f Z a -> (forall m. SNatI m => f m a -> f (S m) a) -> f Z a Source #
InlineInduction n => InlineInduction (S n) Source #
Methods inlineInduction1 :: f Z a -> (forall m. SNatI m => f m a -> f (S m) a) -> f (S n) a Source #

inlineInduction Source #

Arguments

:: InlineInduction n
=> f Z	zero case
-> (forall m. SNatI m => f m -> f (S m))	induction step
-> f n

See InlineInduction.

Arithmetic

type family Plus (n :: Nat) (m :: Nat) :: Nat where ... Source #

Addition.

>>> reflect (snat :: SNat (Plus One Two))
3

Equations

Plus Z m = m
Plus (S n) m = S (Plus n m)

type family Mult (n :: Nat) (m :: Nat) :: Nat where ... Source #

Multiplication.

>>> reflect (snat :: SNat (Mult Two Three))
6

Equations

Mult Z m = Z
Mult (S n) m = Plus m (Mult n m)

Aliases

Nat

zero :: Nat Source #

one :: Nat Source #

two :: Nat Source #

three :: Nat Source #

four :: Nat Source #

five :: Nat Source #

promoted Nat

type Zero = Z Source #

type One = S Zero Source #

type Two = S One Source #

type Three = S Two Source #

type Four = S Three Source #

type Five = S Four Source #

Proofs

proofPlusZeroN :: Plus Zero n :~: n Source #

0 + n = n

proofPlusNZero :: SNatI n => Plus n Zero :~: n Source #

n + 0 = n

proofMultZeroN :: Mult Zero n :~: Zero Source #

0 * n = 0

proofMultNZero :: forall n. SNatI n => Proxy n -> Mult n Zero :~: Zero Source #

n * 0 = n

proofMultOneN :: SNatI n => Mult One n :~: n Source #

1 * n = n

proofMultNOne :: SNatI n => Mult n One :~: n Source #

n * 1 = n