Data.Type.Natural

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

Re-exported modules.

Natural Numbers

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

data Nat

Constructors

Z

S Nat

Instances

Eq Nat

Num Nat

Ord Nat

Show Nat

SingI Nat Z

Preorder Nat Leq

Monomorphicable Nat (Sing Nat)

SingKind Nat (KindParam Nat)

SingRep Nat n0 => SingI Nat (S n0)

SingE Nat (KindParam Nat)

SEq Nat (KindParam Nat)

Eq (Sing Nat n)

Show (Sing Nat n)

Singleton type for Nat.

type SNat a = Sing a

data family Sing a

Smart constructors

sZ :: Sing Z

sS :: forall n. Sing n -> Sing (S n)

Arithmetic functions and their singletons.

min :: Nat -> Nat -> Nat

type family Min a a :: Nat

sMin :: forall t t. Sing t -> Sing t -> Sing (Min t t)

max :: Nat -> Nat -> Nat

type family Max a a :: Nat

sMax :: forall t t. Sing t -> Sing t -> Sing (Max t t)

type :+: n m = n :+ m

type family a :+ a :: Nat

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

Addition for singleton numbers.

(%:+) :: forall t t. Sing t -> Sing t -> Sing (:+ t t)

type :*: n m = n :* m

Type-level multiplication.

type family a :* a :: Nat

(%:*) :: forall t t. Sing t -> Sing t -> Sing (:* t t)

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

Multiplication for singleton numbers.

type :-: n m = n :- m

type family a :- a :: Nat

(%:-) :: forall t t. Sing t -> Sing t -> Sing (:- t t)

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

Type-level predicate & judgements

data Leq n m where

Comparison via GADTs.

Constructors

ZeroLeq :: SNat m -> Leq Zero m

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

Instances

Preorder Nat Leq

class n :<= m

Comparison via type-class.

Instances

Z :<= n

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

type family a :<<= a :: Bool

Boolean-valued type-level comparison function.

(%:<<=) :: forall t t. Sing t -> Sing t -> Sing (:<<= t t)

type LeqInstance n m = Dict (n :<= m)

leqRefl :: SNat n -> Leq n n

leqSucc :: SNat n -> Leq 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 LeqTrueInstance a b = Dict ((a :<<= b) ~ True)

propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m

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.

Quasi quotes for natural numbers

nat :: QuasiQuoter

Quotesi-quoter for Nat. This can be used for an expression, pattern and type.

for example: sing :: SNat ([nat| 2 |] :+ [nat| 5 |])

snat :: QuasiQuoter

Quotesi-quoter for SNat. This can be used for an expression, pattern and type.

For example: [snat|12|] %+ [snat| 5 |], sing :: [snat| 12 |], f [snat| 12 |] = "hey"

Properties of natural numbers

succCongEq :: (n :=: m) -> S n :=: S m

plusCongR :: SNat n -> (m :=: m') -> (m :+ n) :=: (m' :+ n)

plusCongL :: SNat n -> (m :=: m') -> (n :+ m) :=: (n :+ m')

succPlusL :: SNat n -> SNat m -> (S n :+ m) :=: S (n :+ m)

succPlusR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m)

plusZR :: SNat n -> (n :+: Z) :=: n

plusZL :: SNat n -> (Z :+: n) :=: n

eqPreservesS :: (n :=: m) -> S n :=: S m

plusAssociative :: SNat n -> SNat m -> SNat l -> (n :+: (m :+: l)) :=: ((n :+: m) :+: l)

multAssociative :: SNat n -> SNat m -> SNat l -> (n :* (m :* l)) :=: ((n :* m) :* l)

multComm :: SNat n -> SNat m -> (n :* m) :=: (m :* n)

multZL :: SNat m -> (Zero :* m) :=: Zero

multZR :: SNat m -> (m :* Zero) :=: Zero

multOneL :: SNat n -> (One :* n) :=: n

multOneR :: SNat n -> (n :* One) :=: n

plusMultDistr :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l))

multPlusDistr :: SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l))

multCongL :: SNat n -> (m :=: l) -> (n :* m) :=: (n :* l)

multCongR :: SNat n -> (m :=: l) -> (m :* n) :=: (l :* n)

sAndPlusOne :: SNat n -> S n :=: (n :+: One)

plusCommutative :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n)

minusCongEq :: (n :=: m) -> SNat l -> (n :-: l) :=: (m :-: l)

minusNilpotent :: SNat n -> (n :-: n) :=: Zero

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

plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n

plusMinusEqR :: SNat n -> SNat m -> ((m :+: n) :-: m) :=: n

plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)

plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)

zAbsorbsMinR :: SNat n -> Min n Z :=: Z

zAbsorbsMinL :: SNat n -> Min Z n :=: Z

minLeqL :: SNat n -> SNat m -> Leq (Min n m) n

minLeqR :: SNat n -> SNat m -> Leq (Min n m) m

plusSR :: SNat n -> SNat m -> S (n :+: m) :=: (n :+: S m)

leqRhs :: Leq n m -> SNat m

leqLhs :: Leq n m -> SNat n

leqTrans :: Leq n m -> Leq m l -> Leq n l

minComm :: SNat n -> SNat m -> Min n m :=: Min m n

leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m

maxZL :: SNat n -> Max Z n :=: n

maxComm :: SNat n -> SNat m -> Max n m :=: Max m n

maxZR :: SNat n -> Max n Z :=: n

maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)

maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)

plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)

Useful type synonyms and constructors

zero :: Nat

one :: Nat

two :: Nat

three :: Nat

four :: Nat

five :: Nat

six :: Nat

seven :: Nat

eight :: Nat

nine :: Nat

ten :: Nat

eleven :: Nat

twelve :: Nat

thirteen :: Nat

fourteen :: Nat

fifteen :: Nat

sixteen :: Nat

seventeen :: Nat

eighteen :: Nat

nineteen :: Nat

twenty :: Nat

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 :: Sing Zero

sOne :: Sing One

sTwo :: Sing Two

sThree :: Sing Three

sFour :: Sing Four

sFive :: Sing Five

sSix :: Sing Six

sSeven :: Sing Seven

sEight :: Sing Eight

sNine :: Sing Nine

sTen :: Sing Ten

sEleven :: Sing Eleven

sTwelve :: Sing Twelve

sThirteen :: Sing Thirteen

sFourteen :: Sing Fourteen

sFifteen :: Sing Fifteen

sSixteen :: Sing Sixteen

sSeventeen :: Sing Seventeen

sEighteen :: Sing Eighteen

sNineteen :: Sing Nineteen

sTwenty :: Sing Twenty

n0 :: Nat

n1 :: Nat

n2 :: Nat

n3 :: Nat

n4 :: Nat

n5 :: Nat

n6 :: Nat

n7 :: Nat

n8 :: Nat

n9 :: Nat

n10 :: Nat

n11 :: Nat

n12 :: Nat

n13 :: Nat

n14 :: Nat

n15 :: Nat

n16 :: Nat

n17 :: Nat

n18 :: Nat

n19 :: Nat

n20 :: Nat

type N0 = Zero

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 :: Sing N0

sN1 :: Sing N1

sN2 :: Sing N2

sN3 :: Sing N3

sN4 :: Sing N4

sN5 :: Sing N5

sN6 :: Sing N6

sN7 :: Sing N7

sN8 :: Sing N8

sN9 :: Sing N9

sN10 :: Sing N10

sN11 :: Sing N11

sN12 :: Sing N12

sN13 :: Sing N13

sN14 :: Sing N14

sN15 :: Sing N15

sN16 :: Sing N16

sN17 :: Sing N17

sN18 :: Sing N18

sN19 :: Sing N19

sN20 :: Sing N20