TypeUnary.Nat

Experiment in length-typed vectors

Documentation

module TypeUnary.TyNat

Value-typed natural numbers

data Nat :: * -> * where

Constructors

Zero :: Nat Z

Succ :: IsNat n => Nat n -> Nat (S n)

Instances

Show (Nat n)

predN :: Nat (S n) -> Nat n

zero :: Nat N0

one :: Nat N1

two :: Nat N2

three :: Nat N3

four :: Nat N4

withIsNat :: (IsNat n => Nat n -> a) -> Nat n -> a

natSucc :: Nat n -> Nat (S n)

natIsNat :: Nat n -> IsNat n => Nat n

natToZ :: Num a => Nat n -> a

Interpret a Nat as a plain number

natEq :: Nat m -> Nat n -> Maybe (m :=: n)

Equality test

natAdd :: Nat m -> Nat n -> Nat (m :+: n)

Sum of naturals

natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)

Product of naturals

class IsNat n where

Is n a natural number type?

Methods

nat :: Nat n

Instances

IsNat Z

IsNat n => IsNat (S n)

induction :: forall p. p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n))) -> forall n. IsNat n => Dict (p n)

Peano's induction principle

class ((n :+: Z) ~ n) => PlusZero n

Instances

(~) * ((:+:) n Z) n => PlusZero n

plusZero :: IsNat n => Dict (PlusZero n)

Inequality proofs and indices

data m :<: n where infix 4

Proof that m < n

Constructors

ZLess :: Z :<: S n

SLess :: (m :<: n) -> S m :<: S n

succLim :: (m :<: n) -> m :<: S n

Increase the upper limit in an inequality proof

data Index lim

A number under the given limit, with proof

Constructors

forall n . IsNat n => Index (n :<: lim) (Nat n)

Instances

Eq (Index lim)

IsNat n => Num (Index n)

Show (Index n)

unIndex :: (Num a, Enum a) => Index m -> a

succI :: Index m -> Index (S m)

index0 :: Index (N1 :+: m)

index1 :: Index (N2 :+: m)

index2 :: Index (N3 :+: m)

index3 :: Index (N4 :+: m)

coerceToIndex :: (Eq i, Show i, Num i, IsNat m) => i -> Index m

Index generation from integer. Can fail dynamically if the integer is too large.