Data.Type.Nat

Nat numbers. DataKinds stuff.

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

Natural, Nat numbers

data Nat

Nat natural numbers.

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

Constructors

Z

S Nat

Instances

Enum Nat

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

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Integral Nat

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

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

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

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

Methods

toRational :: Nat -> Rational

Show Nat

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

Methods

rnf :: Nat -> ()

Hashable Nat

Methods

hashWithSalt :: Int -> Nat -> Int

hash :: Nat -> Int

toNatural :: Nat -> Natural

Convert Nat to Natural

>>> toNatural 0
0

>>> toNatural 2
2

>>> toNatural $ S $ S $ Z
2

fromNatural :: Natural -> Nat

Convert Natural to Nat

>>> fromNatural 4
4

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

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

Fold Nat.

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

Showing

explicitShow :: Nat -> String

show displaying a structure of Nat.

>>> explicitShow 0
"Z"

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

explicitShowsPrec :: Int -> Nat -> ShowS

showsPrec displaying a structure of Nat.

Singleton

data SNat n where

Singleton of Nat.

Constructors

SZ :: SNat Z

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

Instances

Show (SNat p)

Methods

showsPrec :: Int -> SNat p -> ShowS

show :: SNat p -> String

showList :: [SNat p] -> ShowS

snatToNat :: forall n. SNat n -> Nat

Convert SNat to Nat.

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

snatToNatural :: forall n. SNat n -> Natural

Convert SNat to Natural

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

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

Implicit

class SNatI n where

Convenience class to get SNat.

Minimal complete definition

snat

Methods

snat :: SNat n

Instances

SNatI Z

Methods

snat :: SNat Z

SNatI n => SNatI (S n)

Methods

snat :: SNat (S n)

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

Reify Nat.

>>> reify three reflect
3

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

Reflect type-level Nat to the term level.

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

As reflect but with any Num.

Induction

induction

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

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

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

Instances

InlineInduction Z

Methods

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

InlineInduction n => InlineInduction (S n)

Methods

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

inlineInduction

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

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

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

one :: Nat

two :: Nat

three :: Nat

four :: Nat

five :: Nat

promoted Nat

type Zero = Z

type One = S Zero

type Two = S One

type Three = S Two

type Four = S Three

type Five = S Four

Proofs

proofPlusZeroN :: Plus Zero n :~: n

0 + n = n

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

n + 0 = n

proofMultZeroN :: Mult Zero n :~: Zero

0 * n = 0

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

n * 0 = n

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

1 * n = n

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

n * 1 = n