Data.Parameterized.Vector

A fixed-size vector of typed elements.

NB: This module contains an orphan instance. It will be included in GHC 8.10, see https://gitlab.haskell.org/ghc/ghc/merge_requests/273.

Documentation

data Vector n a

Fixed-size non-empty vectors.

Instances

Functor (Vector n)

Defined in Data.Parameterized.Vector

Methods

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

(<$) :: a -> Vector n b -> Vector n a

Foldable (Vector n)

Defined in Data.Parameterized.Vector

Methods

fold :: Monoid m => Vector n m -> m

foldMap :: Monoid m => (a -> m) -> Vector n a -> m

foldMap' :: Monoid m => (a -> m) -> Vector n a -> m

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

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

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

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

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

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

toList :: Vector n a -> [a]

null :: Vector n a -> Bool

length :: Vector n a -> Int

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

maximum :: Ord a => Vector n a -> a

minimum :: Ord a => Vector n a -> a

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

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

Traversable (Vector n)

Defined in Data.Parameterized.Vector

Methods

traverse :: Applicative f => (a -> f b) -> Vector n a -> f (Vector n b)

sequenceA :: Applicative f => Vector n (f a) -> f (Vector n a)

mapM :: Monad m => (a -> m b) -> Vector n a -> m (Vector n b)

sequence :: Monad m => Vector n (m a) -> m (Vector n a)

Eq a => Eq (Vector n a)

Defined in Data.Parameterized.Vector

Methods

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

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

Show a => Show (Vector n a)

Defined in Data.Parameterized.Vector

Methods

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

show :: Vector n a -> String

showList :: [Vector n a] -> ShowS

Lists

fromList :: 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a)

Make a vector of the given length and element type. Returns Nothing if the input list does not have the right number of elements. O(n).

toList :: Vector n a -> [a]

Get the elements of the vector as a list, lowest index first.

Assignments

fromAssignment :: forall f ctx tp e. (forall tp'. f tp' -> e) -> Assignment f (ctx ::> tp) -> Vector (CtxSize (ctx ::> tp)) e

Convert a non-empty Assignment to a fixed-size Vector.

This function uses the same ordering convention as toVector.

toAssignment :: Size ctx -> (forall tp. Index ctx tp -> e -> f tp) -> Vector (CtxSize ctx) e -> Assignment f ctx

Convert a Vector into a Assignment.

This function uses the same ordering convention as toVector.

Length

length :: Vector n a -> NatRepr n

Length of the vector. O(1)

nonEmpty :: Vector n a -> LeqProof 1 n

Proof that the length of this vector is not 0.

lengthInt :: Vector n a -> Int

The length of the vector as an Int.

Indexing

elemAt :: (i + 1) <= n => NatRepr i -> Vector n a -> a

elemAtMaybe :: Int -> Vector n a -> Maybe a

Get the element at the given index. O(1)

elemAtUnsafe :: Int -> Vector n a -> a

Get the element at the given index. Raises an exception if the element is not in the vector's domain. O(1)

Update

insertAt :: (i + 1) <= n => NatRepr i -> a -> Vector n a -> Vector n a

Insert an element at the given index. O(n).

insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)

Insert an element at the given index. Return Nothing if the element is outside the vector bounds. O(n).

Sub sequences

uncons :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))

Remove the first element of the vector, and return the rest, if any.

unsnoc :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))

Remove the last element of the vector, and return the rest, if any.

slice

Arguments

:: ((i + w) <= n, 1 <= w)

=> NatRepr i

Start index

-> NatRepr w

Width of sub-vector

-> Vector n a

-> Vector w a

Extract a subvector of the given vector.

take :: forall n x a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a

Take the front (lower-indexes) part of the vector.

replace

Arguments

:: ((i + w) <= n, 1 <= w)

=> NatRepr i

Start index

-> Vector w a

sub-vector

-> Vector n a

-> Vector n a

Replace a sub-section of a vector with the given sub-vector.

mapAt

Arguments

:: ((i + w) <= n, 1 <= w)

=> NatRepr i

Start index

-> NatRepr w

Section width

-> (Vector w a -> Vector w a)

map for the sub-vector

-> Vector n a

-> Vector n a

Scope a function to a sub-section of the given vector.

mapAtM

Arguments

:: Monad m

=> ((i + w) <= n, 1 <= w)

=> NatRepr i

Start index

-> NatRepr w

Section width

-> (Vector w a -> m (Vector w a))

map for the sub-vector

-> Vector n a

-> m (Vector n a)

Scope a monadic function to a sub-section of the given vector.

Zipping

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

Zip two vectors, potentially changing types. O(n)

zipWithM :: Monad m => (a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)

zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()

interleave :: forall n a. 1 <= n => Vector n a -> Vector n a -> Vector (2 * n) a

Interleave two vectors. The elements of the first vector are at even indexes in the result, the elements of the second are at odd indexes.

Reorder

shuffle :: (Int -> Int) -> Vector n a -> Vector n a

Move the elements around, as specified by the given function. * Note: the reindexing function says where each of the elements in the new vector come from. * Note: it is OK for the same input element to end up in mulitple places in the result. O(n)

reverse :: forall a n. 1 <= n => Vector n a -> Vector n a

Reverse the vector.

rotateL :: Int -> Vector n a -> Vector n a

Rotate "left". The first element of the vector is on the "left", so rotate left moves all elemnts toward the corresponding smaller index. Elements that fall off the beginning end up at the end.

rotateR :: Int -> Vector n a -> Vector n a

Rotate "right". The first element of the vector is on the "left", so rotate right moves all elemnts toward the corresponding larger index. Elements that fall off the end, end up at the beginning.

shiftL :: Int -> a -> Vector n a -> Vector n a

Move all elements towards smaller indexes. Elements that fall off the front are ignored. Empty slots are filled in with the given element. O(n).

shiftR :: Int -> a -> Vector n a -> Vector n a

Move all elements towards the larger indexes. Elements that "fall" off the end are ignored. Empty slots are filled in with the given element. O(n).

Construction

singleton :: forall a. a -> Vector 1 a

Vector with exactly one element

cons :: forall n a. a -> Vector n a -> Vector (n + 1) a

Add an element to the head of a vector

snoc :: forall n a. Vector n a -> a -> Vector (n + 1) a

Add an element to the tail of a vector

generate :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> Vector (h + 1) a

Apply a function to each element in a range starting at zero; return the a vector of values obtained. cf. both natFromZero and Data.Vector.generate

generateM :: forall m h a. Monad m => NatRepr h -> (forall n. n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a)

Since Vector is traversable, we can pretty trivially sequence natFromZeroVec inside a monad.

Unfolding

unfoldr :: forall h a b. NatRepr h -> (b -> (a, b)) -> b -> Vector (h + 1) a

Construct a vector with exactly h + 1 elements by repeatedly applying a generator function to a seed value.

c.f. Data.Vector.unfoldrExactN

unfoldrM :: forall m h a b. Monad m => NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a)

Monadically construct a vector with exactly h + 1 elements by repeatedly applying a generator function to a seed value.

c.f. Data.Vector.unfoldrExactNM

unfoldrWithIndex :: forall h a b. NatRepr h -> (forall n. n <= h => NatRepr n -> b -> (a, b)) -> b -> Vector (h + 1) a

Unfold a vector, with access to the current index.

c.f. Data.Vector.unfoldrExactN

unfoldrWithIndexM :: forall m h a b. Monad m => NatRepr h -> (forall n. n <= h => NatRepr n -> b -> m (a, b)) -> b -> m (Vector (h + 1) a)

Monadically unfold a vector, with access to the current index.

c.f. Data.Vector.unfoldrExactNM

Splitting and joining

General

joinWithM

Arguments

:: forall m f n w. (1 <= w, Monad m)

=> (forall l. 1 <= l => NatRepr l -> f w -> f l -> m (f (w + l)))

A function for joining contained elements. The first argument is the size of the accumulated third term, and the second argument is the element to join to the accumulated term. The function can use any join strategy desired (prepending/BigEndian, appending/LittleEndian, etc.).

-> NatRepr w

-> Vector n (f w)

-> m (f (n * w))

Monadically join a vector of values, using the given function. This functionality can sometimes be reproduced by creating a newtype wrapper and using joinWith, this implementation is provided for convenience.

joinWith

Arguments

:: forall f n w. 1 <= w

=> (forall l. 1 <= l => NatRepr l -> f w -> f l -> f (w + l))

A function for joining contained elements. The first argument is the size of the accumulated third term, and the second argument is the element to join to the accumulated term. The function can use any join strategy desired (prepending/BigEndian, appending/LittleEndian, etc.).

-> NatRepr w

-> Vector n (f w)

-> f (n * w)

Join a vector of vectors, using the given function to combine the sub-vectors.

splitWith

Arguments

:: forall f w n. (1 <= w, 1 <= n)

=> Endian

-> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)

A function for slicing out a chunk of length w, starting at i

-> NatRepr n

-> NatRepr w

-> f (n * w)

-> Vector n (f w)

Split a vector into a vector of vectors.

The Endian parameter determines the ordering of the inner vectors. If LittleEndian, then less significant bits go into smaller indexes. If BigEndian, then less significant bits go into larger indexes. See the documentation for split for more details.

splitWithA

Arguments

:: forall f g w n. (Applicative f, 1 <= w, 1 <= n)

=> Endian

-> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w))

f function for slicing out f chunk of length w, starting at i

-> NatRepr n

-> NatRepr w

-> g (n * w)

-> f (Vector n (g w))

An applicative version of splitWith.

Vectors

split

Arguments

:: (1 <= w, 1 <= n)

=> NatRepr n

Inner vector size

-> NatRepr w

Outer vector size

-> Vector (n * w) a

Input vector

-> Vector n (Vector w a)

Split a vector into a vector of vectors. The default ordering of the outer result vector is LittleEndian.

For example: let wordsize = knownNat :: NatRepr 3 vecsize = knownNat :: NatRepr 12 numwords = knownNat :: NatRepr 4 (12 / 3) Just inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ] in show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9], [10,11,12] ]" whereas a BigEndian result would have been [ [10,11,12], [7,8,9], [4,5,6], [1,2,3] ]

join :: 1 <= w => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a

Join a vector of vectors into a single vector. Assumes an append/LittleEndian join strategy: the order of the inner vectors is preserved in the result vector.

  let innersize = knownNat :: NatRepr 4
      Just inner1 = fromList innersize [ 1, 2, 3, 4 ]
      Just inner2 = fromList innersize [ 5, 6, 7, 8 ]
      Just inner3 = fromList innersize [ 9, 10, 11, 12 ]
      outersize = knownNat :: NatRepr 3
      Just outer = fromList outersize [ inner1, inner2, inner3 ]
  in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]

a prepend/BigEndian join strategy would have the result: [ 9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ]

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

Append two vectors. The first one is at lower indexes in the result.