type-natural-0.1.0.0: Type-level natural and proofs of their properties.

Data.Type.Natural

Description

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

Synopsis

# Natural Numbers

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

data Nat Source

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 aSource

data family Sing a

## Smart constructors

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

## Arithmetic functions and their singletons.

min :: Nat -> Nat -> NatSource

type family Min a a :: NatSource

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

max :: Nat -> Nat -> NatSource

type family Max a a :: NatSource

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

type :+: n m = n :+ mSource

type family a :+ a :: NatSource

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

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

type :*: n m = n :* mSource

Type-level multiplication.

type family a :* a :: NatSource

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

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

Multiplication for singleton numbers.

type :-: n m = n :- mSource

type family a :- a :: NatSource

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

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

## Type-level predicate & judgements

data Leq n m whereSource

Constructors

 ZeroLeq :: SNat m -> Leq Zero m SuccLeqSucc :: Leq n m -> Leq (S n) (S m)

Instances

 Preorder Nat Leq

class n :<= m Source

Comparison via type-class.

Instances

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

type family a :<<= a :: BoolSource

Boolean-valued type-level comparison function.

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

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

leqRefl :: SNat n -> Leq n nSource

leqSucc :: SNat n -> Leq n (S n)Source

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

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

type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)Source

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

# Conversion functions

natToInt :: Integral n => Nat -> nSource

Convert `Nat` into normal integers.

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

Convert integral numbers into `Nat`

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

Convert 'SNat n' into normal integers.

# Quasi quotes for natural numbers

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

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

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 mSource

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

leqRhs :: Leq n m -> SNat mSource

leqLhs :: Leq n m -> SNat nSource

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

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

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

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

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

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

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

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

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

# Useful type synonyms and constructors

type Zero = ZSource

type Two = S OneSource

type N0 = ZeroSource

type N1 = OneSource

type N2 = TwoSource

type N4 = FourSource

type N5 = FiveSource

type N6 = SixSource

type N9 = NineSource

type N10 = TenSource