Safe Haskell | None |
---|---|

Language | Haskell98 |

Size-parameterized vector types and functions.

- data Vector a n where
- type Index = Ordinal
- module Data.Type.Ordinal
- replicate :: SNat n -> a -> Vector a n
- replicate' :: forall n a. SingI n => a -> Vector a n
- singleton :: a -> Vector a (S Z)
- uncons :: Vector a (S n) -> (a, Vector a n)
- fromList :: SNat n -> [a] -> Maybe (Vector a n)
- fromList' :: SingI n => [a] -> Maybe (Vector a n)
- unsafeFromList :: SNat n -> [a] -> Vector a n
- unsafeFromList' :: SingI n => [a] -> Vector a n
- toList :: Vector a n -> [a]
- append :: Vector a n -> Vector a m -> Vector a (n :+ m)
- head :: Vector a (S n) -> a
- last :: Vector a (S n) -> a
- tail :: Vector a (S n) -> Vector a n
- init :: Vector a (S n) -> Vector a n
- null :: Vector a n -> Bool
- length :: Vector a n -> Int
- sLength :: Vector a n -> SNat n
- map :: (a -> b) -> Vector a n -> Vector b n
- reverse :: forall a n. Vector a n -> Vector a n
- intersperse :: a -> Vector a n -> Vector a ((Two :* n) :- One)
- transpose :: SingI n => Vector (Vector a n) m -> Vector (Vector a m) n
- foldl :: (a -> b -> a) -> a -> Vector b n -> a
- foldl' :: forall a b n. (a -> b -> a) -> a -> Vector b n -> a
- foldl1 :: (a -> a -> a) -> Vector a (S n) -> a
- foldl1' :: (a -> a -> a) -> Vector a (S n) -> a
- foldr :: (a -> b -> b) -> b -> Vector a n -> b
- foldr1 :: (a -> a -> a) -> Vector a (S n) -> a
- ifoldl :: (a -> Index n -> b -> a) -> a -> Vector b n -> a
- concat :: Vector (Vector a n) m -> Vector a (m :* n)
- and :: Vector Bool m -> Bool
- or :: Vector Bool m -> Bool
- any :: (a -> Bool) -> Vector a n -> Bool
- all :: (a -> Bool) -> Vector a n -> Bool
- 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
- take :: ((n :<<= m) ~ True) => SNat n -> Vector a m -> Vector a n
- takeAtMost :: SNat n -> Vector a m -> Vector a (Min n m)
- drop :: ((n :<<= m) ~ True) => SNat n -> Vector a m -> Vector a (m :-: n)
- splitAt :: ((n :<<= m) ~ True) => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))
- splitAtMost :: SNat n -> Vector a m -> (Vector a (Min n m), Vector a (m :-: n))
- stripPrefix :: Eq a => Vector a n -> Vector a m -> Maybe (Vector a (m :- n))
- elem :: Eq a => a -> Vector a n -> Bool
- notElem :: Eq a => a -> Vector a n -> Bool
- find :: (a -> Bool) -> Vector a n -> Maybe a
- (!!) :: ((n :<<= m) ~ True) => Vector a (S m) -> SNat n -> a
- (%!!) :: Vector a n -> Index n -> a
- index :: ((n :<<= m) ~ True) => SNat n -> Vector a (S m) -> a
- sIndex :: Index n -> Vector a n -> a
- elemIndex :: Eq a => a -> Vector a n -> Maybe Int
- sElemIndex :: Eq a => a -> Vector a n -> Maybe (Index n)
- findIndex :: (a -> Bool) -> Vector a n -> Maybe Int
- sFindIndex :: (a -> Bool) -> Vector a n -> Maybe (Index n)
- findIndices :: (a -> Bool) -> Vector a n -> [Int]
- sFindIndices :: (a -> Bool) -> Vector a n -> [Index n]
- elemIndices :: Eq a => a -> Vector a n -> [Int]
- sElemIndices :: Eq a => a -> Vector a n -> [Index n]
- zip :: Vector a n -> Vector b m -> Vector (a, b) (Min n m)
- zipSame :: Vector a n -> Vector b n -> Vector (a, b) n
- zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)
- zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n
- unzip :: Vector (a, b) n -> (Vector a n, Vector b n)

# Vectors and indices

Fixed-length list.

## Re-exports

module Data.Type.Ordinal

# Conversion & Construction

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

`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 Source

`replicate`

, with the length inferred.

## List

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

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) Source

Convert a list into vector, with length inferred.

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

Unsafe version of `fromList`

.
If a given list is shorter than the length, it aborts.

unsafeFromList' :: SingI n => [a] -> Vector a n Source

Unsafe version of `unsafeFromList`

.

# Basic functions

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

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

null :: Vector a n -> Bool Source

Test whether a `Vector`

is empty, though it's clear from the type parameter.

# Vector transformations

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

`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 Source

`reverse`

`xs`

returns the elements of xs in reverse order. `xs`

must be finite.

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

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 Source

The `transpose`

function transposes the rows and columns of its argument.

# Reducing vectors (folds)

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

Indexed version of `foldl`

.
Since 1.4.2.0

## Special folds

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

The function `concat`

concatenates all vectors in th vector.

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

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 Source

Applied to a predicate and a list, `all`

determines if all element of the vector satisfies the predicate.

# Subvectors

## Extracting subvectors

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

`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) Source

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) Source

`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)) Source

`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)) Source

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)) Source

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

## Searching with a predicate

# Indexing vectors

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

List index (subscript) operator, starting from `sZero`

.

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

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.

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

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] Source

`Index`

version of `findIndices`

.

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

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] Source

`Index`

version of `elemIndices`

.

# Zipping vectors

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

`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 Source

Same as `zip`

, but the given vectors must have the same length.