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





Experiment in length-typed vectors


Type-level numbers

data Z Source

Type-level representation of zero


data S n Source

Type-level representation of successor


IsNat n => IsNat (S n) 

type family a :+: b Source

Sum of type-level numbers

type N0 = ZSource

type N1 = S N0Source

type N2 = S N1Source

type N3 = S N2Source

type N4 = S N3Source

type N5 = S N4Source

type N6 = S N5Source

type N7 = S N6Source

type N8 = S N7Source

type N9 = S N8Source

type N10 = S N9Source

type N11 = S N10Source

type N12 = S N11Source

type N13 = S N12Source

type N14 = S N13Source

type N15 = S N14Source

type N16 = S N15Source

Typed natural numbers

data Nat whereSource


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


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 :: Nat n -> IntegerSource

Interpret a Nat as an Integer

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

Equality test

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

Sum of naturals

data m :<: n Source

Proof that m < n

data Index lim Source

A number under the given limit, with proof


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


Eq (Index lim) 

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

index2 :: Index (S (S (S m)))Source

index3 :: Index (S (S (S (S m))))Source


data Vec whereSource

Vectors with type-determined length, having empty vector (ZVec) and vector cons ('(:<)').


ZVec :: Vec Z a 
:< :: a -> Vec n a -> Vec (S n) a 


Functor (Vec n) 
IsNat n => Applicative (Vec n) 
Foldable (Vec n) 
Traversable (Vec n) 
Eq a => Eq (Vec n a)

Enumerate the elements of a vector. See also elemsV vElems :: Vec n a -> [a] vElems ZVec = [] vElems (a :< as) = a : vElems as

Ord a => Ord (Vec n a) 
Show a => Show (Vec n a) 
(IsNat n, Storable a) => Storable (Vec n a) 
(IsNat n, Num a) => VectorSpace (Vec n a) 
(IsNat n, Num a) => InnerSpace (Vec n a) 
(IsNat n, Num a) => AdditiveGroup (Vec n a) 

class IsNat n whereSource

n a vector length.


nat :: Nat nSource

pureV :: a -> Vec n aSource

elemsV :: [a] -> Vec n aSource

peekV :: Storable a => Ptr a -> IO (Vec n a)Source

pokeV :: Storable a => Ptr a -> Vec n a -> IO ()Source


IsNat Z 
IsNat n => IsNat (S n) 

(<+>) :: Vec m a -> Vec n a -> Vec (m :+: n) aSource

Concatenation of vectors

indices :: Nat n -> Vec n (Index n)Source

Indices under n: index0 :< index1 :< ...

vec1 :: a -> Vec1 aSource

vec2 :: a -> a -> Vec2 aSource

vec3 :: a -> a -> a -> Vec3 aSource

vec4 :: a -> a -> a -> a -> Vec4 aSource

un1 :: Vec1 a -> aSource

Extract element

un2 :: Vec2 a -> (a, a)Source

Extract elements

un3 :: Vec3 a -> (a, a, a)Source

Extract elements

un4 :: Vec4 a -> (a, a, a, a)Source

Extract elements

get0 :: Vec (S n) a -> Vec1 aSource

get1 :: Vec (S (S n)) a -> Vec1 aSource

get2 :: Vec (S (S (S n))) a -> Vec1 aSource

get3 :: Vec (S (S (S (S n)))) a -> Vec1 aSource

get :: Index n -> Vec n a -> Vec1 aSource

General indexing, taking a proof that the index is within bounds.

swizzle :: Vec n (Index m) -> Vec m a -> Vec n aSource

Swizzling. Extract multiple elements simultaneously.

split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a)Source

Split a vector