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

Stability experimental conal@conal.net Safe-Infered

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)

# Inequality proofs and indices

data m :<: n whereSource

Proof that `m < n`

Constructors

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

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)

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

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

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