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) infixr 5

Instances

Monomorphicable Nat (Vector a)

Monomorphic representation of Vector a n is [a].

Associated Types

type MonomorphicRep (Vector a) (k1 :: Vector a -> *) :: *

Methods

promote :: MonomorphicRep (Vector a) k1 -> Monomorphic (Vector a) k1

demote :: Monomorphic (Vector a) k1 -> MonomorphicRep (Vector a) k1

Eq a => Eq (Vector a n)

Methods

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

(/=) :: Vector a n -> Vector a n -> Bool

Ord a => Ord (Vector a n)

Methods

compare :: Vector a n -> Vector a n -> Ordering

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

(<=) :: Vector a n -> Vector a n -> Bool

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

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

max :: Vector a n -> Vector a n -> Vector a n

min :: Vector a n -> Vector a n -> Vector a n

Show a => Show (Vector a n)

Methods

showsPrec :: Int -> Vector a n -> ShowS

show :: Vector a n -> String

showList :: [Vector a n] -> ShowS

NFData a => NFData (Vector a n)

Methods

rnf :: Vector a n -> ()

Hashable a => Hashable (Vector a n)

Methods

hashWithSalt :: Int -> Vector a n -> Int

hash :: Vector a n -> Int

type MonomorphicRep Nat (Vector a)

type MonomorphicRep Nat (Vector a) = [a]

type Index = Ordinal

Type synonym for Ordinal.

Re-exports

module Data.Type.Ordinal

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. SingI 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' :: SingI 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' :: SingI 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.

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

Extract the elements before the last of a non-empty list.

Since 1.4.2.0

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 :: SingI 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.

ifoldl :: (a -> Index n -> b -> a) -> a -> Vector b n -> a

Indexed version of foldl.

Since 1.4.2.0

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

sum takes the sum of the numbers contained in a sized vector.

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

product takes the product of the numbers contained in a sized vector.

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

Maximum element of a (statically) non-empty vector.

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

Minimum element of a (statically) non-empty vector.

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

Test if the element occurs in the vector?

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

Negation of elem.

Searching with a predicate

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

Find the first element which satisfies the given predicate. If there are no element satisfying the predicate, returns Nothing.

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.

Macros

sized :: Lift t => [t] -> ExpQ

Utility Template Haskell macro to lift plain lists upto sized vectors.

Since 1.4.3.0

>>> $(sized [1,2,3 :: Int])
1 :- (2 :- (3 :- Nil))

sized' :: [ExpQ] -> ExpQ

Similar to lift', but lifts the list of ExpQ instead. This function is useful to avoid the stage restriction.

Since 1.4.3.0

>>> let a = "foo" in $(sized' [[|a|],[|"bar"|],[|"baz"|]])
"foo" :- ("bar" :- ("baz" :- Nil))