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

Stabilityexperimental
Maintainerconal@conal.net

TypeUnary.Vec

Contents

Description

Experiment in length-typed vectors

Synopsis

Documentation

Vectors

data Vec whereSource

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

Constructors

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

Instances

IsNat n => Monad (Vec n) 
Functor (Vec n) 
IsNat n => Applicative (Vec n) 
Foldable (Vec n) 
Traversable (Vec n) 
Eq a => Eq (Vec n a) 
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) 
ToVec (Vec n a) n a 

headV :: Vec (S n) a -> aSource

Type-safe head for vectors

tailV :: Vec (S n) a -> Vec n aSource

Type-safe tail for vectors

joinV :: Vec n (Vec n a) -> Vec n aSource

Equivalent to monad join for vectors

(<+>) :: 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

vec5 :: a -> a -> a -> a -> a -> Vec5 aSource

vec6 :: a -> a -> a -> a -> a -> a -> Vec6 aSource

vec7 :: a -> a -> a -> a -> a -> a -> a -> Vec7 aSource

vec8 :: a -> a -> a -> a -> a -> a -> a -> a -> Vec8 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

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

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

get0Source

Arguments

:: Vec (N1 :+: n) a 
-> a

Get first element

get1Source

Arguments

:: Vec (N2 :+: n) a 
-> a

Get second element

get2Source

Arguments

:: Vec (N3 :+: n) a 
-> a

Get third element

get3Source

Arguments

:: Vec (N4 :+: n) a 
-> a

Get fourth element

set :: Index n -> a -> Vec n a -> Vec n aSource

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

set0Source

Arguments

:: a 
-> Vec (N1 :+: n) a 
-> Vec (N1 :+: n) a

Set first element

set1Source

Arguments

:: a 
-> Vec (N2 :+: n) a 
-> Vec (N2 :+: n) a

Set second element

set2Source

Arguments

:: a 
-> Vec (N3 :+: n) a 
-> Vec (N3 :+: n) a

Set third element

set3Source

Arguments

:: a 
-> Vec (N4 :+: n) a 
-> Vec (N4 :+: n) a

Set fourth element

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

deleteV :: Eq a => a -> Vec (S n) a -> Vec n aSource

Delete exactly one occurrence of an element from a vector, raising an error if the element isn't present.

elemsV :: IsNat n => [a] -> Vec n aSource

Convert a list into a vector. Error if the list is too short or too long

class ToVec c n a whereSource

Methods

toVec :: c -> Vec n aSource

Instances

IsNat n => ToVec [a] n a 
ToVec (Vec n a) n a