Data.Type.Natural

Type level peano natural number, some arithmetic functions and their singletons.

Natural numbers and its singleton type

data Nat

Peano natural numbers. It will be promoted to the type-level natural number.

Constructors

Z

S Nat

Instances

Eq Nat

Num Nat

Ord Nat

Show Nat

data SNat n where

Singleton type for Nat. When constructing data, use smart constructors such as sZ and sS.

Constructors

SZ :: SNat Z

SS :: SNat n -> SNat (S n)

Smart constructors

sZ :: SNat Z

The smart constructor for SZ.

sS :: SNat n -> SNat (S n)

The smart constructor for SS n.

Arithmetic functions and thir singletons.

min :: Nat -> Nat -> Nat

Minimum function.

type family Min n m :: Nat

Type-level minimum function.

sMin :: SNat n -> SNat m -> SNat (Min n m)

Singleton function for minimum function.

max :: Nat -> Nat -> Nat

Maximum function.

type family Max n m :: Nat

Type-level maximum function.

sMax :: SNat n -> SNat m -> SNat (Max n m)

Singleton function for maximum.

type family n :+: m :: Nat

Type-level addition.

(%+) :: SNat n -> SNat m -> SNat (n :+: m)

Addition for singleton numbers.

type family n :*: m :: Nat

Type-level multiplication.

(%*) :: SNat n -> SNat m -> SNat (n :*: m)

Multiplication for singleton numbers.

type family n :-: m :: Nat

(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)

Type-level predicate & judgements

data Leq n m where

Comparison witness via GADTs.

Constructors

ZeroLeq :: SNat m -> Leq Zero m

SuccLeqSucc :: Leq n m -> Leq (S n) (S m)

class n :<= m

Comparison via type-class.

Instances

Z :<= n

:<= n m => (S n) :<= (S m)

type family n :<<= m :: Bool

Comparison function

data LeqInstance n m

leqRefl :: SNat n -> LeqInstance n n

leqSucc :: SNat n -> LeqInstance n (S n)

boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m

boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m

propToClassLeq :: Leq n m -> LeqInstance n m

Type-classes for singletons

class Sing n where

Singleton type-class. This class will be removed soon after singletons package available for the latest Haskell Paltform.

Methods

sing :: SNat n

Automatically compute singletons.

Instances

Sing Z

Sing n => Sing (S n)

data SingInstance a where

Witness for Sing instance. This type will be removed soon after singletons package available for the latest Haskell Paltform.

Constructors

SingInstance :: Sing a => SingInstance a

singInstance :: SNat n -> SingInstance n

Get witness for singleton integers. This function will be removed soon after singletons package available for the latest Haskell Paltform.

Conversion functions

natToInt :: Integral n => Nat -> n

Convert Nat into normal integers.

intToNat :: (Integral a, Ord a) => a -> Nat

Convert integral numbers into Nat

sNatToInt :: Num n => SNat x -> n

Convert 'SNat n' into normal integers.

Useful type synonyms and constructors

type Zero = Z

type One = S Zero

type Two = S One

type Three = S Two

type Four = S Three

type Five = S Four

type Six = S Five

type Seven = S Six

type Eight = S Seven

type Nine = S Eight

type Ten = S Nine

type Eleven = S Ten

type Twelve = S Eleven

type Thirteen = S Twelve

type Fourteen = S Thirteen

type Fifteen = S Fourteen

type Sixteen = S Fifteen

type Seventeen = S Sixteen

type Eighteen = S Seventeen

type Nineteen = S Eighteen

type Twenty = S Nineteen

sZero :: SNat Z

sOne :: SNat One

sTwo :: SNat Two

sThree :: SNat Three

sFour :: SNat Four

sFive :: SNat Five

sSix :: SNat Six

sSeven :: SNat Seven

sEight :: SNat Eight

sNine :: SNat Nine

sTen :: SNat Ten

sEleven :: SNat Eleven

sTwelve :: SNat Twelve

sThirteen :: SNat Thirteen

sFourteen :: SNat Fourteen

sFifteen :: SNat Fifteen

sSixteen :: SNat Sixteen

sSeventeen :: SNat Seventeen

sEighteen :: SNat Eighteen

sNineteen :: SNat Nineteen

sTwenty :: SNat Twenty

type N0 = Z

type N1 = One

type N2 = Two

type N3 = Three

type N4 = Four

type N5 = Five

type N6 = Six

type N7 = Seven

type N8 = Eight

type N9 = Nine

type N10 = Ten

type N11 = Eleven

type N12 = Twelve

type N13 = Thirteen

type N14 = Fourteen

type N15 = Fifteen

type N16 = Sixteen

type N17 = Seventeen

type N18 = Eighteen

type N19 = Nineteen

type N20 = Twenty

sN0 :: SNat Z

sN1 :: SNat One

sN2 :: SNat Two

sN3 :: SNat Three

sN4 :: SNat Four

sN5 :: SNat Five

sN6 :: SNat Six

sN7 :: SNat Seven

sN8 :: SNat Eight

sN9 :: SNat Nine

sN10 :: SNat Ten

sN11 :: SNat Eleven

sN12 :: SNat Twelve

sN13 :: SNat Thirteen

sN14 :: SNat Fourteen

sN15 :: SNat Fifteen

sN16 :: SNat Sixteen

sN17 :: SNat Seventeen

sN18 :: SNat Eighteen

sN19 :: SNat Nineteen

sN20 :: SNat Twenty