parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Copyright | (c) Galois Inc 2014-2019
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.Vector

Contents

- Lists
- Assignments
- Length
- Indexing
- Indexing with Fin
- Update
- Sub sequences
- Zipping
- Reorder
- Construction
  - Unfolding
- Splitting and joining
  - General
  - Vectors

Description

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.

Synopsis

- data Vector (n :: Natural) a
- fromList :: forall (n :: Natural) a. 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a)
- toList :: forall (n :: Natural) a. Vector n a -> [a]
- fromAssignment :: forall {k} f (ctx :: Ctx k) (tp :: k) e. (forall (tp' :: k). f tp' -> e) -> Assignment f (ctx ::> tp) -> Vector (CtxSize (ctx ::> tp)) e
- toAssignment :: forall {k} (ctx :: Ctx k) e f. Size ctx -> (forall (tp :: k). Index ctx tp -> e -> f tp) -> Vector (CtxSize ctx) e -> Assignment f ctx
- length :: forall (n :: Natural) a. Vector n a -> NatRepr n
- nonEmpty :: forall (n :: Natural) a. Vector n a -> LeqProof 1 n
- lengthInt :: forall (n :: Natural) a. Vector n a -> Int
- elemAt :: forall (i :: Natural) (n :: Natural) a. (i + 1) <= n => NatRepr i -> Vector n a -> a
- elemAtMaybe :: forall (n :: Natural) a. Int -> Vector n a -> Maybe a
- elemAtUnsafe :: forall (n :: Natural) a. Int -> Vector n a -> a
- indicesUpTo :: forall (n :: Nat). NatRepr n -> Vector (n + 1) (Fin (n + 1))
- indicesOf :: forall (n :: Natural) a. Vector n a -> Vector n (Fin n)
- insertAt :: forall (i :: Natural) (n :: Natural) a. (i + 1) <= n => NatRepr i -> a -> Vector n a -> Vector n a
- insertAtMaybe :: forall a (n :: Natural). Int -> a -> Vector n a -> Maybe (Vector n a)
- uncons :: forall (n :: Natural) a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
- unsnoc :: forall (n :: Natural) a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
- slice :: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> Vector n a -> Vector w a
- take :: forall (n :: Natural) (x :: Natural) a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a
- replace :: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((i + w) <= n, 1 <= w) => NatRepr i -> Vector w a -> Vector n a -> Vector n a
- mapAt :: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> (Vector w a -> Vector w a) -> Vector n a -> Vector n a
- mapAtM :: forall m (i :: Natural) (w :: Natural) (n :: Natural) a. (Monad m, (i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> (Vector w a -> m (Vector w a)) -> Vector n a -> m (Vector n a)
- zipWith :: forall a b c (n :: Natural). (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
- zipWithM :: forall m a b c (n :: Natural). Monad m => (a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
- zipWithM_ :: forall m a b (n :: Natural). Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()
- interleave :: forall (n :: Natural) a. 1 <= n => Vector n a -> Vector n a -> Vector (2 * n) a
- shuffle :: forall (n :: Natural) a. (Int -> Int) -> Vector n a -> Vector n a
- reverse :: forall a (n :: Natural). 1 <= n => Vector n a -> Vector n a
- rotateL :: forall (n :: Natural) a. Int -> Vector n a -> Vector n a
- rotateR :: forall (n :: Natural) a. Int -> Vector n a -> Vector n a
- shiftL :: forall a (n :: Natural). Int -> a -> Vector n a -> Vector n a
- shiftR :: forall a (n :: Natural). Int -> a -> Vector n a -> Vector n a
- singleton :: a -> Vector 1 a
- cons :: forall (n :: Natural) a. a -> Vector n a -> Vector (n + 1) a
- snoc :: forall (n :: Natural) a. Vector n a -> a -> Vector (n + 1) a
- generate :: forall (h :: Nat) a. NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> a) -> Vector (h + 1) a
- generateM :: forall m (h :: Nat) a. Monad m => NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a)
- unfoldr :: forall (h :: Nat) a b. NatRepr h -> (b -> (a, b)) -> b -> Vector (h + 1) a
- unfoldrM :: forall m (h :: Nat) a b. Monad m => NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a)
- unfoldrWithIndex :: forall (h :: Nat) a b. NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> b -> (a, b)) -> b -> Vector (h + 1) a
- unfoldrWithIndexM :: forall m (h :: Nat) a b. Monad m => NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> b -> m (a, b)) -> b -> m (Vector (h + 1) a)
- iterateN :: forall (n :: Nat) a. NatRepr n -> (a -> a) -> a -> Vector (n + 1) a
- iterateNM :: forall m (n :: Nat) a. Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a)
- joinWithM :: forall m f (n :: Natural) (w :: Natural). (1 <= w, Monad m) => (forall (l :: Natural). 1 <= l => NatRepr l -> f w -> f l -> m (f (w + l))) -> NatRepr w -> Vector n (f w) -> m (f (n * w))
- joinWith :: forall f (n :: Natural) (w :: Natural). 1 <= w => (forall (l :: Natural). 1 <= l => NatRepr l -> f w -> f l -> f (w + l)) -> NatRepr w -> Vector n (f w) -> f (n * w)
- splitWith :: forall f (w :: Natural) (n :: Natural). (1 <= w, 1 <= n) => Endian -> (forall (i :: Natural). (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w) -> NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)
- splitWithA :: forall f g (w :: Natural) (n :: Natural). (Applicative f, 1 <= w, 1 <= n) => Endian -> (forall (i :: Natural). (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w)) -> NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))
- split :: forall (w :: Natural) (n :: Natural) a. (1 <= w, 1 <= n) => NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)
- join :: forall (w :: Natural) (n :: Natural) a. 1 <= w => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
- append :: forall (m :: Natural) a (n :: Natural). Vector m a -> Vector n a -> Vector (m + n) a

# Documentation

data Vector (n :: Natural) a Source #

Fixed-size non-empty vectors.

#### Instances

Instances details

Functor (Vector n) Source # |
Instance details Defined in Data.Parameterized.Vector Methods fmap :: (a -> b) -> Vector n a -> Vector n b Source # (<$) :: a -> Vector n b -> Vector n a Source #
Foldable (Vector n) Source # |

Instance details

Defined in Data.Parameterized.Vector

Methods

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

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

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

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

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

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

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

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

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

toList :: Vector n a -> [a] Source #

null :: Vector n a -> Bool Source #

length :: Vector n a -> Int Source #

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

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

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

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

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

Traversable (Vector n) Source # |
Instance details Defined in Data.Parameterized.Vector Methods traverse :: Applicative f => (a -> f b) -> Vector n a -> f (Vector n b) Source # sequenceA :: Applicative f => Vector n (f a) -> f (Vector n a) Source # mapM :: Monad m => (a -> m b) -> Vector n a -> m (Vector n b) Source # sequence :: Monad m => Vector n (m a) -> m (Vector n a) Source #
FoldableWithIndex (Fin n) (Vector n) Source # |

Instance details

Defined in Data.Parameterized.Vector

Methods

ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vector n a -> m Source #

ifoldMap' :: Monoid m => (Fin n -> a -> m) -> Vector n a -> m Source #

ifoldr :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b Source #

ifoldl :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b Source #

ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b Source #

ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b Source #

FunctorWithIndex (Fin n) (Vector n) Source # |
Instance details Defined in Data.Parameterized.Vector Methods imap :: (Fin n -> a -> b) -> Vector n a -> Vector n b Source #
TraversableWithIndex (Fin n) (Vector n) Source # |
Instance details Defined in Data.Parameterized.Vector Methods itraverse :: Applicative f => (Fin n -> a -> f b) -> Vector n a -> f (Vector n b) Source #
Show a => Show (Vector n a) Source # |
Instance details Defined in Data.Parameterized.Vector Methods showsPrec :: Int -> Vector n a -> ShowS Source # show :: Vector n a -> String Source # showList :: [Vector n a] -> ShowS Source #
Eq a => Eq (Vector n a) Source # |
Instance details Defined in Data.Parameterized.Vector Methods (==) :: Vector n a -> Vector n a -> Bool Source # (/=) :: Vector n a -> Vector n a -> Bool Source #

# Lists

fromList :: forall (n :: Natural) a. 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a) Source #

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 :: forall (n :: Natural) a. Vector n a -> [a] Source #

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

# Assignments

fromAssignment :: forall {k} f (ctx :: Ctx k) (tp :: k) e. (forall (tp' :: k). f tp' -> e) -> Assignment f (ctx ::> tp) -> Vector (CtxSize (ctx ::> tp)) e Source #

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

This function uses the same ordering convention as `toVector`.

toAssignment :: forall {k} (ctx :: Ctx k) e f. Size ctx -> (forall (tp :: k). Index ctx tp -> e -> f tp) -> Vector (CtxSize ctx) e -> Assignment f ctx Source #

Convert a `Vector` into a `Assignment`.

This function uses the same ordering convention as `toVector`.

# Length

length :: forall (n :: Natural) a. Vector n a -> NatRepr n Source #

Length of the vector. `O(1)`

nonEmpty :: forall (n :: Natural) a. Vector n a -> LeqProof 1 n Source #

Proof that the length of this vector is not 0.

lengthInt :: forall (n :: Natural) a. Vector n a -> Int Source #

The length of the vector as an Int.

# Indexing

elemAt :: forall (i :: Natural) (n :: Natural) a. (i + 1) <= n => NatRepr i -> Vector n a -> a Source #

elemAtMaybe :: forall (n :: Natural) a. Int -> Vector n a -> Maybe a Source #

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

elemAtUnsafe :: forall (n :: Natural) a. Int -> Vector n a -> a Source #

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

# Indexing with Fin

indicesUpTo :: forall (n :: Nat). NatRepr n -> Vector (n + 1) (Fin (n + 1)) Source #

indicesOf :: forall (n :: Natural) a. Vector n a -> Vector n (Fin n) Source #

# Update

insertAt :: forall (i :: Natural) (n :: Natural) a. (i + 1) <= n => NatRepr i -> a -> Vector n a -> Vector n a Source #

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

insertAtMaybe :: forall a (n :: Natural). Int -> a -> Vector n a -> Maybe (Vector n a) Source #

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

# Sub sequences

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

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

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

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

slice Source #

Arguments

:: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((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 :: Natural) (x :: Natural) a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a Source #

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

replace Source #

Arguments

:: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((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 Source #

Arguments

:: forall (i :: Natural) (w :: Natural) (n :: Natural) a. ((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 Source #

Arguments

:: forall m (i :: Natural) (w :: Natural) (n :: Natural) a. (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 :: forall a b c (n :: Natural). (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c Source #

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

zipWithM :: forall m a b c (n :: Natural). Monad m => (a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c) Source #

zipWithM_ :: forall m a b (n :: Natural). Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m () Source #

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

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 :: forall (n :: Natural) a. (Int -> Int) -> Vector n a -> Vector n a Source #

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 :: Natural). 1 <= n => Vector n a -> Vector n a Source #

Reverse the vector.

rotateL :: forall (n :: Natural) a. Int -> Vector n a -> Vector n a Source #

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 :: forall (n :: Natural) a. Int -> Vector n a -> Vector n a Source #

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 :: forall a (n :: Natural). Int -> a -> Vector n a -> Vector n a Source #

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 :: forall a (n :: Natural). Int -> a -> Vector n a -> Vector n a Source #

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 :: a -> Vector 1 a Source #

Vector with exactly one element

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

Add an element to the head of a vector

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

Add an element to the tail of a vector

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

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 :: Nat) a. Monad m => NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a) Source #

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

## Unfolding

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

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 :: Nat) a b. Monad m => NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a) Source #

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 :: Nat) a b. NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> b -> (a, b)) -> b -> Vector (h + 1) a Source #

Unfold a vector, with access to the current index.

c.f. `Data.Vector.unfoldrExactN`

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

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

c.f. `Data.Vector.unfoldrExactNM`

iterateN :: forall (n :: Nat) a. NatRepr n -> (a -> a) -> a -> Vector (n + 1) a Source #

Build a vector by repeatedly applying a function to a seed value.

Compare to `iterateN`

iterateNM :: forall m (n :: Nat) a. Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a) Source #

Build a vector by repeatedly applying a monadic function to a seed value.

Compare to `iterateNM`.

# Splitting and joining

## General

joinWithM Source #

Arguments

:: forall m f (n :: Natural) (w :: Natural). (1 <= w, Monad m) |
=> (forall (l :: Natural). 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 Source #

Arguments

:: forall f (n :: Natural) (w :: Natural). 1 <= w |
=> (forall (l :: Natural). 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 Source #

Arguments

:: forall f (w :: Natural) (n :: Natural). (1 <= w, 1 <= n) |
=> Endian |
-> (forall (i :: Natural). (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 Source #

Arguments

:: forall f g (w :: Natural) (n :: Natural). (Applicative f, 1 <= w, 1 <= n) |
=> Endian |
-> (forall (i :: Natural). (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 Source #

Arguments

:: forall (w :: Natural) (n :: Natural) a. (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 :: forall (w :: Natural) (n :: Natural) a. 1 <= w => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a Source #

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 :: forall (m :: Natural) a (n :: Natural). Vector m a -> Vector n a -> Vector (m + n) a Source #

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