Portability | non-portable |
---|---|

Stability | experimental |

Maintainer | alfonso.acosta@gmail.com |

`FSVec`

: Fixed sized vectors. Vectors with numerically parameterized size.

- data Nat s => FSVec s a
- empty :: FSVec D0 a
- (+>) :: (Nat s, Pos s', Succ s s') => a -> FSVec s a -> FSVec s' a
- singleton :: a -> FSVec D1 a
- vectorCPS :: [a] -> (forall s. Nat s => FSVec s a -> w) -> w
- vectorTH :: Lift a => [a] -> ExpQ
- v :: QuasiQuoter
- unsafeVector :: Nat s => s -> [a] -> FSVec s a
- reallyUnsafeVector :: [a] -> FSVec s a
- readFSVec :: Read a => String -> (forall s. Nat s => FSVec s a -> w) -> w
- length :: forall s a. Nat s => FSVec s a -> Int
- genericLength :: forall s a n. (Nat s, Num n) => FSVec s a -> n
- lengthT :: Nat s => FSVec s a -> s
- fromVector :: Nat s => FSVec s a -> [a]
- null :: FSVec D0 a -> Bool
- (!) :: (Pos s, Nat i, i :<: s) => FSVec s a -> i -> a
- replace :: (Nat s, Nat i) => FSVec s a -> i -> a -> FSVec s a
- head :: Pos s => FSVec s a -> a
- last :: Pos s => FSVec s a -> a
- init :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a
- tail :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' a
- take :: (Nat i, Nat s, Min s i s') => i -> FSVec s a -> FSVec s' a
- drop :: (Nat i, Nat s, Min s i sm, Sub s sm s') => i -> FSVec s a -> FSVec s' a
- select :: (Nat f, Nat s, Nat n, f :<: i, Mul s n smn, Add f smn fasmn, fasmn :<=: i) => f -> s -> n -> FSVec i a -> FSVec n a
- group :: (Pos n, Nat s, Div s n s') => n -> FSVec s a -> FSVec s' (FSVec n a)
- (<+) :: (Nat s, Pos s', Succ s s') => FSVec s a -> a -> FSVec s' a
- (++) :: (Nat s1, Nat s2, Add s1 s2 s3) => FSVec s1 a -> FSVec s2 a -> FSVec s3 a
- map :: Nat s => (a -> b) -> FSVec s a -> FSVec s b
- zipWith :: Nat s => (a -> b -> c) -> FSVec s a -> FSVec s b -> FSVec s c
- foldl :: Nat s => (a -> b -> a) -> a -> FSVec s b -> a
- foldr :: Nat s => (b -> a -> a) -> a -> FSVec s b -> a
- zip :: Nat s => FSVec s a -> FSVec s b -> FSVec s (a, b)
- unzip :: Nat s => FSVec s (a, b) -> (FSVec s a, FSVec s b)
- shiftl :: Pos s => FSVec s a -> a -> FSVec s a
- shiftr :: Pos s => FSVec s a -> a -> FSVec s a
- rotl :: forall s a. Nat s => FSVec s a -> FSVec s a
- rotr :: Nat s => FSVec s a -> FSVec s a
- concat :: (Nat s1, Nat s2, Nat s3, Mul s1 s2 s3) => FSVec s1 (FSVec s2 a) -> FSVec s3 a
- reverse :: Nat s => FSVec s a -> FSVec s a
- iterate :: Nat s => s -> (a -> a) -> a -> FSVec s a
- generate :: Nat s => s -> (a -> a) -> a -> FSVec s a
- copy :: Nat s => s -> a -> FSVec s a

# Documentation

data Nat s => FSVec s a Source

Fixed-Sized Vector data type, indexed with type-level naturals, the first index for all vectors is 0

(+>) :: (Nat s, Pos s', Succ s s') => a -> FSVec s a -> FSVec s' aSource

Cons operator, note it's not a constructor

vectorCPS :: [a] -> (forall s. Nat s => FSVec s a -> w) -> wSource

Build a vector from a list (CPS style)

Vector quasiquoter

unsafeVector :: Nat s => s -> [a] -> FSVec s aSource

Build a vector from a list (unsafe version: The static/dynamic size of the list is checked to match at runtime)

reallyUnsafeVector :: [a] -> FSVec s aSource

Build a vector from a list.

Unlike unsafeVector, reallyunsafeVector doesn't have access to the static size of the list and thus cannot not check it against its dynamic size (which saves traversing the list at runtime to obtain the dynamic length).

Therefore, reallyUnsafeVector (the name is that long on purspose) can be used to gain some performance but may break the consistency of the size parameter if not handled with care (i.e. the size parameter can nolonger be checked statically and the fullfilment of function constraints is left to the programmers judgement).

Do not use reallyUnsafeVector unless you know what you're doing!

readFSVec :: Read a => String -> (forall s. Nat s => FSVec s a -> w) -> wSource

Read a vector. As it happens with vectorCPS, this is the best we can achieve

genericLength :: forall s a n. (Nat s, Num n) => FSVec s a -> nSource

generic value-level length of a vector

fromVector :: Nat s => FSVec s a -> [a]Source

Transform Vector to a list

init :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' aSource

Return all but the last element of a vector

tail :: (Pos s, Succ s' s) => FSVec s a -> FSVec s' aSource

Return all but the first element of a vector

take :: (Nat i, Nat s, Min s i s') => i -> FSVec s a -> FSVec s' aSource

Take the first i elements of a vector

drop :: (Nat i, Nat s, Min s i sm, Sub s sm s') => i -> FSVec s a -> FSVec s' aSource

Drop the first i elements of a vector

select :: (Nat f, Nat s, Nat n, f :<: i, Mul s n smn, Add f smn fasmn, fasmn :<=: i) => f -> s -> n -> FSVec i a -> FSVec n aSource

The function `select`

selects elements in the vector. The first argument
gives the initial element, starting from zero, the second argument gives the
stepsize between elements and the last argument gives the number of
elements.

group :: (Pos n, Nat s, Div s n s') => n -> FSVec s a -> FSVec s' (FSVec n a)Source

break a vector into subvectors of size n.

(<+) :: (Nat s, Pos s', Succ s s') => FSVec s a -> a -> FSVec s' aSource

add an element at the end of a vector. (Inverse of '(+>)')

(++) :: (Nat s1, Nat s2, Add s1 s2 s3) => FSVec s1 a -> FSVec s2 a -> FSVec s3 aSource

Concatenate two vectors

map :: Nat s => (a -> b) -> FSVec s a -> FSVec s bSource

Apply a function on all elements of a vector

zipWith :: Nat s => (a -> b -> c) -> FSVec s a -> FSVec s b -> FSVec s cSource

Applies function pairwise on two vectors

foldl :: Nat s => (a -> b -> a) -> a -> FSVec s b -> aSource

Folds a function from the right to the left over a vector using an initial value.

foldr :: Nat s => (b -> a -> a) -> a -> FSVec s b -> aSource

Folds a function from the left to the right over a vector using an initial value.

zip :: Nat s => FSVec s a -> FSVec s b -> FSVec s (a, b)Source

zip two vectors into a vector of tuples.

unzip :: Nat s => FSVec s (a, b) -> (FSVec s a, FSVec s b)Source

unzip a vector of tuples into two vectors.

rotl :: forall s a. Nat s => FSVec s a -> FSVec s aSource

Rotate a vector to the left. Note that this fuctions does not change the size of a vector.

rotr :: Nat s => FSVec s a -> FSVec s aSource

Rotate a vector to the left. Note that this fuctions does not change the size of a vector.

concat :: (Nat s1, Nat s2, Nat s3, Mul s1 s2 s3) => FSVec s1 (FSVec s2 a) -> FSVec s3 aSource

flatten a vector of vectors to a single vector

iterate :: Nat s => s -> (a -> a) -> a -> FSVec s aSource

generate a vector with a given number of elements starting from an initial element using a supplied function for the generation of elements.

FSVec> iterate d5 (+1) 1

<1,2,3,4,5> :: Num a => FSVec D5 a