Safe Haskell	None
Language	Haskell2010

Data.Type.Nat

Contents

Natural, Nat numbers
Showing
Singleton
Implicit
Equality
Induction
- Example: unfoldedFix
Arithmetic
Conversion to GHC Nat
Aliases
- Nat
- promoted Nat
Proofs

Description

Nat numbers. DataKinds stuff.

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

Synopsis

data Nat
- = Z
- | S Nat
toNatural :: Nat -> Natural
fromNatural :: Natural -> Nat
cata :: a -> (a -> a) -> Nat -> a
explicitShow :: Nat -> String
explicitShowsPrec :: Int -> Nat -> ShowS
data SNat (n :: Nat ) where
- SZ :: SNat ' Z
- SS :: SNatI n => SNat (' S n)
snatToNat :: forall n. SNat n -> Nat
snatToNatural :: forall n. SNat n -> Natural
class SNatI (n :: Nat ) where
- snat :: SNat n
withSNat :: SNat n -> ( SNatI n => r) -> r
reify :: forall r. Nat -> ( forall n. SNatI n => Proxy n -> r) -> r
reflect :: forall n proxy. SNatI n => proxy n -> Nat
reflectToNum :: forall n m proxy. ( SNatI n, Num m) => proxy n -> m
eqNat :: forall n m. ( SNatI n, SNatI m) => Maybe (n :~: m)
type family EqNat (n :: Nat ) (m :: Nat ) where ...
discreteNat :: forall n m. ( SNatI n, SNatI m) => Dec (n :~: m)
induction :: forall n f. SNatI n => f ' Z -> ( forall m. SNatI m => f m -> f (' S m)) -> f n
induction1 :: forall n f a. SNatI n => f ' Z a -> ( forall m. SNatI m => f m a -> f (' S m) a) -> f n a
class SNatI n => InlineInduction (n :: Nat ) where
- inlineInduction1 :: f ' Z a -> ( forall m. InlineInduction m => f m a -> f (' S m) a) -> f n a
inlineInduction :: forall n f. InlineInduction n => f ' Z -> ( forall m. InlineInduction m => f m -> f (' S m)) -> f n
unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a
type family Plus (n :: Nat ) (m :: Nat ) :: Nat where ...
type family Mult (n :: Nat ) (m :: Nat ) :: Nat where ...
type family Mult2 (n :: Nat ) :: Nat where ...
type family DivMod2 (n :: Nat ) :: ( Nat , Bool ) where ...
type family ToGHC (n :: Nat ) :: Nat where ...
type family FromGHC (n :: Nat ) :: Nat where ...
nat0 :: Nat
nat1 :: Nat
nat2 :: Nat
nat3 :: Nat
nat4 :: Nat
nat5 :: Nat
nat6 :: Nat
nat7 :: Nat
nat8 :: Nat
nat9 :: Nat
type Nat0 = ' Z
type Nat1 = ' S Nat0
type Nat2 = ' S Nat1
type Nat3 = ' S Nat2
type Nat4 = ' S Nat3
type Nat5 = ' S Nat4
type Nat6 = ' S Nat5
type Nat7 = ' S Nat6
type Nat8 = ' S Nat7
type Nat9 = ' S Nat8
proofPlusZeroN :: Plus Nat0 n :~: n
proofPlusNZero :: SNatI n => Plus n Nat0 :~: n
proofMultZeroN :: Mult Nat0 n :~: Nat0
proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0
proofMultOneN :: SNatI n => Mult Nat1 n :~: n
proofMultNOne :: SNatI n => Mult n Nat1 :~: n

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

Instances details

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

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 :: Nat ) where Source #

Singleton of Nat .

Constructors

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

Instances

Instances details

TestEquality SNat Source #
Instance details Defined in Data.Type.Nat Methods testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) Source #
Show ( SNat p) Source #
Instance details Defined in Data.Type.Nat Methods showsPrec :: Int -> SNat p -> ShowS Source # show :: SNat p -> String Source # showList :: [ SNat p] -> ShowS Source #

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

Convert SNat to Nat .

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

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

Convert SNat to Natural

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

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

Implicit

class SNatI (n :: Nat ) where Source #

Convenience class to get SNat .

Methods

snat :: SNat n Source #

Instances

Instances details

SNatI ' Z Source #
Instance details Defined in Data.Type.Nat Methods snat :: SNat ' Z Source #
SNatI n => SNatI (' S n) Source #
Instance details Defined in Data.Type.Nat Methods snat :: SNat (' S n) Source #

withSNat :: SNat n -> ( SNatI n => r) -> r Source #

Constructor SNatI dictionary from SNat .

Since: 0.0.3

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

Reify Nat .

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

Equality

eqNat :: forall n m. ( SNatI n, SNatI m) => Maybe (n :~: m) Source #

Decide equality of type-level numbers.

>>> eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
Just Refl

>>> eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
Nothing

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

Type family used to implement == from Data.Type.Equality module.

Equations

EqNat ' Z ' Z = ' True
EqNat (' S n) (' S m) = EqNat n m
EqNat n m = ' False

discreteNat :: forall n m. ( SNatI n, SNatI m) => Dec (n :~: m) Source #

Decide equality of type-level numbers.

>>> decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))
"Yes Refl"

Since: 0.0.3

Induction

induction Source #

Arguments

:: forall n f. 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

:: forall n f a. 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 Nat3 Int
Tagged 6

class SNatI n => InlineInduction (n :: Nat ) where Source #

The induction will be fully inlined.

See test/Inspection.hs .

Methods

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

Instances

Instances details

InlineInduction ' Z Source #
Instance details Defined in Data.Type.Nat Methods inlineInduction1 :: f ' Z a -> ( forall (m :: Nat ). InlineInduction m => f m a -> f (' S m) a) -> f ' Z a Source #
InlineInduction n => InlineInduction (' S n) Source #
Instance details Defined in Data.Type.Nat Methods inlineInduction1 :: f ' Z a -> ( forall (m :: Nat ). InlineInduction m => f m a -> f (' S m) a) -> f (' S n) a Source #

inlineInduction Source #

Arguments

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

See InlineInduction .

Example: unfoldedFix

unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a Source #

Unfold n steps of a general recursion.

Note: Always benchmark . This function may give you both bad properties: a lot of code (increased binary size), and worse performance.

For known n unfoldedFix will unfold recursion, for example

unfoldedFix (Proxy :: Proxy Nat3) f = f (f (f (fix f)))

Arithmetic

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

Addition.

>>> reflect (snat :: SNat (Plus Nat1 Nat2))
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 Nat2 Nat3))
6

Equations

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

type family Mult2 (n :: Nat ) :: Nat where ... Source #

Multiplication by two. Doubling.

>>> reflect (snat :: SNat (Mult2 Nat4))
8

Equations

Mult2 ' Z = ' Z
Mult2 (' S n) = ' S (' S ( Mult2 n))

type family DivMod2 (n :: Nat ) :: ( Nat , Bool ) where ... Source #

Division by two. False is 0 and True is 1 as a remainder.

>>> :kind! DivMod2 Nat7
DivMod2 Nat7 :: (Nat, Bool)
= '( 'S ('S ('S 'Z)), 'True)

>>> :kind! DivMod2 Nat4
DivMod2 Nat4 :: (Nat, Bool)
= '( 'S ('S 'Z), 'False)

Equations

DivMod2 ' Z = '(' Z , ' False )
DivMod2 (' S ' Z ) = '(' Z , ' True )
DivMod2 (' S (' S n)) = DivMod2' ( DivMod2 n)

Conversion to GHC Nat

type family ToGHC (n :: Nat ) :: Nat where ... Source #

Convert to GHC Nat .

>>> :kind! ToGHC Nat5
ToGHC Nat5 :: GHC.Nat
= 5

Equations

ToGHC ' Z = 0
ToGHC (' S n) = 1 + ToGHC n

type family FromGHC (n :: Nat ) :: Nat where ... Source #

Convert from GHC Nat .

>>> :kind! FromGHC 7
FromGHC 7 :: Nat
= 'S ('S ('S ('S ('S ('S ('S 'Z))))))

Equations

FromGHC 0 = ' Z
FromGHC n = ' S ( FromGHC (n - 1))

Aliases

Nat

nat0 :: Nat Source #

nat1 :: Nat Source #

nat2 :: Nat Source #

nat3 :: Nat Source #

nat4 :: Nat Source #

nat5 :: Nat Source #

nat6 :: Nat Source #

nat7 :: Nat Source #

nat8 :: Nat Source #

nat9 :: Nat Source #

promoted Nat

type Nat0 = ' Z Source #

type Nat1 = ' S Nat0 Source #

type Nat2 = ' S Nat1 Source #

type Nat3 = ' S Nat2 Source #

type Nat4 = ' S Nat3 Source #

type Nat5 = ' S Nat4 Source #

type Nat6 = ' S Nat5 Source #

type Nat7 = ' S Nat6 Source #

type Nat8 = ' S Nat7 Source #

type Nat9 = ' S Nat8 Source #

Proofs

proofPlusZeroN :: Plus Nat0 n :~: n Source #

0 + n = n

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

n + 0 = n

proofMultZeroN :: Mult Nat0 n :~: Nat0 Source #

0 * n = 0

proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0 Source #

n * 0 = 0

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

1 * n = n

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

n * 1 = n