Data.Vector.Sized

Size-parameterized vector types and functions.

Vectors and indices

data Vector a n where

Fixed-length list.

Constructors

Nil :: Vector a Z

:- :: a -> Vector a n -> Vector a (S n)

Instances

Monomorphicable Nat (Vector a)

Monomorphic representation of Vector a n is [a].

Eq a => Eq (Vector a n)

Show a => Show (Vector a n)

data Index n where

Index type for list.

Constructors

Index :: (S m :<<= n) ~ True => SNat m -> Index n

Instances

Show (Index n)

succIndex :: Index n -> Index (S n)

Succ index number.

indexToInt :: Index n -> Int

Convert index into integer.

Conversion & Construction

replicate :: SNat n -> a -> Vector a n

replicate n x is a vector of length n with x the value of every element.

replicate' :: forall n a. SingRep n => a -> Vector a n

replicate, with the length inferred.

singleton :: a -> Vector a (S Z)

Construct a singleton vector.

uncons :: Vector a (S n) -> (a, Vector a n)

Uncons the non-empty list.

List

fromList :: SNat n -> [a] -> Maybe (Vector a n)

Convert a list into a vector. If a given list is shorter than the length, it returns Nothing.

fromList' :: SingRep n => [a] -> Maybe (Vector a n)

Convert a list into vector, with length inferred.

unsafeFromList :: SNat n -> [a] -> Vector a n

Unsafe version of fromList. If a given list is shorter than the length, it aborts.

unsafeFromList' :: SingRep n => [a] -> Vector a n

Unsafe version of unsafeFromList.

toList :: Vector a n -> [a]

Convert a vector into a list.

Basic functions

append :: Vector a n -> Vector a m -> Vector a (n :+: m)

Append two Vectors.

head :: Vector a (S n) -> a

Extract the first element of a non-empty vector.

last :: Vector a (S n) -> a

Extract the last element of a non-empty vector.

tail :: Vector a (S n) -> Vector a n

Extract the elements after the head of a non-empty list.

null :: Vector a n -> Bool

Test whether a Vector is empty, though it's clear from the type parameter.

length :: Vector a n -> Int

length returns the length of a finite list as an Int.

sLength :: Vector a n -> SNat n

sLength returns the length of a finite list as a SNat n.

Vector transformations

map :: (a -> b) -> Vector a n -> Vector b n

map f xs is the vector obtained by applying f to each element of xs.

reverse :: forall a n. Vector a n -> Vector a n

reverse xs returns the elements of xs in reverse order. xs must be finite.

intersperse :: a -> Vector a n -> Vector a ((Two :* n) :- One)

The intersperse function takes an element and a vector and `intersperses' that element between the elements of the vector.

transpose :: SingRep n => Vector (Vector a n) m -> Vector (Vector a m) n

The transpose function transposes the rows and columns of its argument.

Reducing vectors (folds)

foldl :: (a -> b -> a) -> a -> Vector b n -> a

Left fold.

foldl' :: forall a b n. (a -> b -> a) -> a -> Vector b n -> a

A strict version of foldl.

foldl1 :: (a -> a -> a) -> Vector a (S n) -> a

Left fold for non-empty vector.

foldl1' :: (a -> a -> a) -> Vector a (S n) -> a

A strict version of foldl1.

foldr :: (a -> b -> b) -> b -> Vector a n -> b

Right fold.

foldr1 :: (a -> a -> a) -> Vector a (S n) -> a

Right fold for non-empty vector.

Special folds

concat :: Vector (Vector a n) m -> Vector a (m :*: n)

The function concat concatenates all vectors in th vector.

and :: Vector Bool m -> Bool

and returns the conjunction of a Boolean vector.

or :: Vector Bool m -> Bool

or returns the disjunction of a Boolean vector.

any :: (a -> Bool) -> Vector a n -> Bool

Applied to a predicate and a list, any determines if any element of the vector satisfies the predicate.

all :: (a -> Bool) -> Vector a n -> Bool

Applied to a predicate and a list, all determines if all element of the vector satisfies the predicate.

sum :: Num a => Vector a n -> a

product :: Num a => Vector a n -> a

maximum :: Ord a => Vector a (S n) -> a

minimum :: Ord a => Vector a (S n) -> a

Subvectors

Extracting subvectors

take :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n

take n xs returns the prefix of xs of length n, with n less than or equal to the length of xs.

takeAtMost :: SNat n -> Vector a m -> Vector a (Min n m)

A variant of take which returns entire xs if n is greater than the length of xs.

drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)

drop n xs returns the suffix of xs after the first n elements, with n less than or equal to the length of xs.

splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))

splitAt n xs returns a tuple where first element is xs prefix of length n and second element is the remainder of the list. n should be less than or equal to the length of xs.

splitAtMost :: SNat n -> Vector a m -> (Vector a (Min n m), Vector a (m :-: n))

A varian of splitAt which allows n to be greater than the length of xs.

stripPrefix :: Eq a => Vector a n -> Vector a m -> Maybe (Vector a (m :- n))

The stripPrefix function drops the given prefix from a vector. It returns Nothing if the vector did not start with the prefix given or shorter than the prefix, or Just the vector after the prefix, if it does.

Searching vectors

Searching by equality

elem :: Eq a => a -> Vector a n -> Bool

notElem :: Eq a => a -> Vector a n -> Bool

Searching with a predicate

find :: (a -> Bool) -> Vector a n -> Maybe a

Indexing vectors

(!!) :: (n :<<= m) ~ True => Vector a (S m) -> SNat n -> a

List index (subscript) operator, starting from sZero.

(%!!) :: Vector a n -> Index n -> a

A Index version of !!.

index :: (n :<<= m) ~ True => SNat n -> Vector a (S m) -> a

Flipped version of !!.

sIndex :: Index n -> Vector a n -> a

A Index version of index.

elemIndex :: Eq a => a -> Vector a n -> Maybe Int

The elemIndex function returns the index (as Int) of the first element in the given list which is equal (by ==) to the query element, or Nothing if there is no such element.

sElemIndex :: Eq a => a -> Vector a n -> Maybe (Index n)

Index version of elemIndex.

findIndex :: (a -> Bool) -> Vector a n -> Maybe Int

The findIndex function takes a predicate and a vector and returns the index of the first element in the vector satisfying the predicate, or Nothing if there is no such element.

sFindIndex :: (a -> Bool) -> Vector a n -> Maybe (Index n)

Index version of findIndex.

findIndices :: (a -> Bool) -> Vector a n -> [Int]

The findIndices function extends findIndex, by returning the indices of all elements satisfying the predicate, in ascending order.

sFindIndices :: (a -> Bool) -> Vector a n -> [Index n]

Index version of findIndices.

elemIndices :: Eq a => a -> Vector a n -> [Int]

The elemIndices function extends elemIndex, by returning the indices of all elements equal to the query element, in ascending order.

sElemIndices :: Eq a => a -> Vector a n -> [Index n]

Index version of elemIndices.

Zipping vectors

zip :: Vector a n -> Vector b m -> Vector (a, b) (Min n m)

zip takes two vectors and returns a vector of corresponding pairs. If one input list is short, excess elements of the longer list are discarded.

zipSame :: Vector a n -> Vector b n -> Vector (a, b) n

Same as zip, but the given vectors must have the same length.

zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)

zipWith generalises zip by zipping with the function given as the first argument, instead of a tupling function.

zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n

Same as zipWith, but the given vectors must have the same length.

unzip :: Vector (a, b) n -> (Vector a n, Vector b n)

Inverse of zipSame.