type-unary-0.2.8: Type-level and typed unary natural numbers, inequality proofs, vectors

Stability experimental conal@conal.net Safe-Inferred

TypeUnary.Nat

Description

Experiment in length-typed vectors

Synopsis

# Value-typed natural numbers

data Nat whereSource

Constructors

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

Instances

 Show (Nat n)

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

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

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

natToZ :: (Enum a, Num a) => Nat n -> aSource

Interpret a `Nat` as a plain number

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

Equality test

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

Sum of naturals

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

Product of naturals

class IsNat n whereSource

Is `n` a natural number type?

Methods

nat :: Nat nSource

Instances

 IsNat Z IsNat n => IsNat (S n)

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

Peano's induction principle

# Inequality proofs and indices

data m :<: n whereSource

Proof that `m < n`

Constructors

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

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

Increase the upper limit in an inequality proof

data Index lim Source

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 -> aSource

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

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

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