CLaSH.Sized.Vector

Vector constructors

data Vec :: Nat -> * -> * where

Fixed size vectors

• Lists with their length encoded in their type
• Vector elements have an ASCENDING subscript starting from 0 and ending at maxIndex (== length - 1).

>>> (3:>4:>5:>Nil)
<3,4,5>
>>> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a

Constructors

Nil :: Vec 0 a

(:>) :: a -> Vec n a -> Vec (n + 1) a infixr 5

Instances

Functor (Vec n)

KnownNat n => Applicative (Vec n)

NB: Not synthesisable

Foldable (Vec n)

Traversable (Vec n)

NB: Not synthesisable

Eq a => Eq (Vec n a)

Ord a => Ord (Vec n a)

Show a => Show (Vec n a)

(Default a, KnownNat n) => Default (Vec n a)

Lift a => Lift (Vec n a)

(KnownNat n, KnownNat (BitSize a), BitPack a) => BitPack (Vec n a)

KnownNat n => Bundle (Vec n a)

type Unbundled' t (Vec n a) = Vec n (Signal' t a)

type BitSize (Vec n a) = * n (BitSize a)

(<:) :: Vec n a -> a -> Vec (n + 1) a infixl 5

Add an element to the tail of a vector.

>>> (3:>4:>5:>Nil) <: 1
<3,4,5,1>
>>> :t (3:>4:>5:>Nil) <: 1
(3:>4:>5:>Nil) <: 1 :: Num a => Vec (3 + 1) a

singleton :: a -> Vec 1 a

Create a vector of one element

>>> singleton 5
<5>

Standard Vector functions

Extracting sub-Vectors

head :: Vec (n + 1) a -> a

Extract the first element of a vector

>>> head (1:>2:>3:>Nil)
1
>>> head Nil

<interactive>:...
    Couldn't match type ‘1’ with ‘0’
    Expected type: Vec (0 + 1) a
      Actual type: Vec 0 a
    In the first argument of ‘head’, namely ‘Nil’
    In the expression: head Nil

tail :: Vec (n + 1) a -> Vec n a

Extract the elements after the head of a vector

>>> tail (1:>2:>3:>Nil)
<2,3>
>>> tail Nil

<interactive>:...
    Couldn't match type ‘1’ with ‘0’
    Expected type: Vec (0 + 1) a
      Actual type: Vec 0 a
    In the first argument of ‘tail’, namely ‘Nil’
    In the expression: tail Nil

last :: Vec (n + 1) a -> a

Extract the last element of a vector

>>> last (1:>2:>3:>Nil)
3
>>> last Nil

<interactive>:...
    Couldn't match type ‘1’ with ‘0’
    Expected type: Vec (0 + 1) a
      Actual type: Vec 0 a
    In the first argument of ‘last’, namely ‘Nil’
    In the expression: last Nil

init :: Vec (n + 1) a -> Vec n a

Extract all the elements of a vector except the last element

>>> init (1:>2:>3:>Nil)
<1,2>
>>> init Nil

<interactive>:...
    Couldn't match type ‘1’ with ‘0’
    Expected type: Vec (0 + 1) a
      Actual type: Vec 0 a
    In the first argument of ‘init’, namely ‘Nil’
    In the expression: init Nil

take :: SNat m -> Vec (m + n) a -> Vec m a

take n, applied to a vector xs, returns the n-length prefix of xs

>>> take (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
<1,2,3>
>>> take d3               (1:>2:>3:>4:>5:>Nil)
<1,2,3>
>>> take d0               (1:>2:>Nil)
<>
>>> take d4               (1:>2:>Nil)

<interactive>:...
    Couldn't match type ‘4 + n0’ with ‘2’
    The type variable ‘n0’ is ambiguous
    Expected type: Vec (4 + n0) a
      Actual type: Vec (1 + 1) a
    In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’
    In the expression: take d4 (1 :> 2 :> Nil)
    In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)

takeI :: KnownNat m => Vec (m + n) a -> Vec m a

takeI xs, returns the prefix of xs as demanded by the context

>>> takeI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
<1,2>

drop :: SNat m -> Vec (m + n) a -> Vec n a

drop n xs returns the suffix of xs after the first n elements

>>> drop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
<4,5>
>>> drop d3               (1:>2:>3:>4:>5:>Nil)
<4,5>
>>> drop d0               (1:>2:>Nil)
<1,2>
>>> drop d4               (1:>2:>Nil)

<interactive>:...
    Couldn't match expected type ‘2’ with actual type ‘4 + n0’
    The type variable ‘n0’ is ambiguous
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

dropI :: KnownNat m => Vec (m + n) a -> Vec n a

dropI xs, returns the suffix of xs as demanded by the context

>>> dropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
<4,5>

at :: SNat m -> Vec (m + (n + 1)) a -> a

at n xs returns n'th element of xs

NB: vector elements have an ASCENDING subscript starting from 0 and ending at maxIndex.

>>> at (snat :: SNat 1) ((1:>2:>3:>4:>5:>Nil) :: Vec 5 Int)
2
>>> at d1               ((1:>2:>3:>4:>5:>Nil) :: Vec 5 Int)
2

select :: (CmpNat (i + s) (s * n) ~ GT) => SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a

select f s n xs selects n elements with stepsize s and offset f from xs

>>> select (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
<2,4,6>
>>> select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
<2,4,6>

selectI :: (CmpNat (i + s) (s * n) ~ GT, KnownNat n) => SNat f -> SNat s -> Vec (f + i) a -> Vec n a

selectI f s xs selects as many elements as demanded by the context with stepsize s and offset f from xs

>>> selectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
<2,4>

Combining Vectors

(++) :: Vec n a -> Vec m a -> Vec (n + m) a infixr 5

Append two vectors

>>> (1:>2:>3:>Nil) ++ (7:>8:>Nil)
<1,2,3,7,8>

(+>>) :: KnownNat n => a -> Vec n a -> Vec n a infixr 4

Add an element to the head of a vector, and extract all but the last element.

>>> 1 +>> (3:>4:>5:>Nil)
<1,3,4>
>>> 1 +>> Nil
<>

(<<+) :: KnownNat n => Vec n a -> a -> Vec n a infixl 4

Add an element to the tail of a vector, and extract all but the first element.

>>> (3:>4:>5:>Nil) <<+ 1
<4,5,1>
>>> Nil <<+ 1
<>

concat :: Vec n (Vec m a) -> Vec (n * m) a

Concatenate a vector of vectors

>>> concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)
<1,2,3,4,5,6,7,8,9,10,11,12>

zip :: Vec n a -> Vec n b -> Vec n (a, b)

zip takes two vectors and returns a vector of corresponding pairs.

>>> zip (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil)
<(1,4),(2,3),(3,2),(4,1)>

unzip :: Vec n (a, b) -> (Vec n a, Vec n b)

unzip transforms a vector of pairs into a vector of first components and a vector of second components.

>>> unzip ((1,4):>(2,3):>(3,2):>(4,1):>Nil)
(<1,2,3,4>,<4,3,2,1>)

shiftInAt0

Arguments

:: KnownNat n

=> Vec n a

The old vector

-> Vec m a

The elements to shift in at the head

-> (Vec n a, Vec m a)

(The new vector, shifted out elements)

Shift in elements to the head of a vector, bumping out elements at the tail. The result is a tuple containing:

• The new vector
• The shifted out elements

>>> shiftInAt0 (1 :> 2 :> 3 :> 4 :> Nil) ((-1) :> 0 :> Nil)
(<-1,0,1,2>,<3,4>)
>>> shiftInAt0 (1 :> Nil) ((-1) :> 0 :> Nil)
(<-1>,<0,1>)

shiftInAtN

Arguments

:: KnownNat m

=> Vec n a

The old vector

-> Vec m a

The elements to shift in at the tail

-> (Vec n a, Vec m a)

(The new vector, shifted out elements)

Shift in element to the tail of a vector, bumping out elements at the head. The result is a tuple containing:

• The new vector
• The shifted out elements

>>> shiftInAtN (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> Nil)
(<3,4,5,6>,<1,2>)
>>> shiftInAtN (1 :> Nil) (2 :> 3 :> Nil)
(<3>,<1,2>)

shiftOutFrom0

Arguments

:: (Default a, KnownNat m)

=> SNat m

m, the number of elements to shift out

-> Vec (m + n) a

The old vector

-> (Vec (m + n) a, Vec m a)

(The new vector, shifted out elements)

Shift m elements out from the head of a vector, filling up the tail with Default values. The result is a tuple containing:

• The new vector
• The shifted out values

>>> shiftOutFrom0 d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
(<3,4,5,0,0>,<1,2>)

shiftOutFromN

Arguments

:: (Default a, KnownNat (m + n))

=> SNat m

m, the number of elements to shift out

-> Vec (m + n) a

The old vector

-> (Vec (m + n) a, Vec m a)

(The new vector, shifted out elements)

Shift m elements out from the tail of a vector, filling up the head with Default values. The result is a tuple containing:

• The new vector
• The shifted out values

>>> shiftOutFromN d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
(<0,0,1,2,3>,<4,5>)

Splitting Vectors

splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)

Split a vector into two vectors at the given point

>>> splitAt (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil)
(<1,2,3>,<7,8>)
>>> splitAt d3 (1:>2:>3:>7:>8:>Nil)
(<1,2,3>,<7,8>)

splitAtI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)

Split a vector into two vectors where the length of the two is determined by the context

>>> splitAtI (1:>2:>3:>7:>8:>Nil) :: (Vec 2 Int, Vec 3 Int)
(<1,2>,<3,7,8>)

unconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)

Split a vector of (n * m) elements into a vector of vectors with length m, where m is given

>>> unconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
<<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>

unconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)

Split a vector of (n * m) elements into a vector of vectors with length m, where m is determined by the context

>>> unconcatI (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) :: Vec 2 (Vec 6 Int)
<<1,2,3,4,5,6>,<7,8,9,10,11,12>>

merge :: Vec n a -> Vec n a -> Vec (n + n) a

Merge two vectors, alternating their elements, i.e.,

>>> merge (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> 7 :> 8 :> Nil)
<1,5,2,6,3,7,4,8>

Applying functions to Vector elements

map :: (a -> b) -> Vec n a -> Vec n b

map f xs is the vector obtained by applying f to each element of xs, i.e.,

map f (x1 :> x2 :>  ... :> xn :> Nil) == (f x1 :> f x2 :> ... :> f xn :> Nil)

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

zipWith generalises zip by zipping with the function given as the first argument, instead of a tupling function. For example, zipWith (+) is applied to two vectors to produce the vector of corresponding sums.

zipWith f (x1 :> x2 :> ... xn :> Nil) (y1 :> y2 :> ... :> yn :> Nil) == (f x1 y1 :> f x2 y2 :> ... :> f xn yn :> Nil)

NB: zipWith is strict in its second argument, and lazy in its third. This matters when zipWith is used in a recursive setting. See lazyV for more information.

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

foldr, applied to a binary operator, a starting value (typically the right-identity of the operator), and a vector, reduces the vector using the binary operator, from right to left:

foldr f z (x1 :> ... :> xn1 :> xn :> Nil) == x1 `f` (... (xn1 `f` (xn `f` z))...)
foldr r z Nil                             == z

>>> foldr (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
1.875

NB: "foldr f z xs" produces a linear structure, which has a depth, or delay, of O(length xs). Use fold if your binary operator f is associative, as "fold f xs" produces a structure with a depth of O(log_2(length xs)).

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

foldl, applied to a binary operator, a starting value (typically the left-identity of the operator), and a vector, reduces the vector using the binary operator, from left to right:

foldl f z (x1 :> x2 :> ... :> xn :> Nil) == (...((z `f` x1) `f` x2) `f`...) `f` xn
foldl f z Nil                            == z

>>> foldl (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
8.333333333333333e-3

NB: "foldl f z xs" produces a linear structure, which has a depth, or delay, of O(length xs). Use fold if your binary operator f is associative, as "fold f xs" produces a structure with a depth of O(log_2(length xs)).

foldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a

foldr1 is a variant of foldr that has no starting value argument, and thus must be applied to non-empty vectors.

foldr1 f (x1 :> ... :> xn2 :> xn1 :> xn :> Nil) == x1 `f` (... (xn2 `f` (xn1 `f` xn))...)
foldr1 f (x1 :> Nil)                            == x1
foldr1 f Nil                                    == TYPE ERROR

>>> foldr1 (/) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
1.875

NB: "foldr1 f z xs" produces a linear structure, which has a depth, or delay, of O(length xs). Use fold if your binary operator f is associative, as "fold f xs" produces a structure with a depth of O(log_2(length xs)).

foldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a

foldl1 is a variant of foldl that has no starting value argument, and thus must be applied to non-empty vectors.

foldl1 f (x1 :> x2 :> x3 :> ... :> xn :> Nil) == (...((x1 `f` x2) `f` x3) `f`...) `f` xn
foldl1 f (x1 :> Nil)                          == x1
foldl1 f Nil                                  == TYPE ERROR

>>> foldl1 (/) (1 :> 5 :> 4 :> 3 :> 2 :> Nil)
8.333333333333333e-3

NB: "foldl1 f z xs" produces a linear structure, which has a depth, or delay, of O(length xs). Use fold if your binary operator f is associative, as "fold f xs" produces a structure with a depth of O(log_2(length xs)).

fold :: (a -> a -> a) -> Vec (n + 1) a -> a

fold is a variant of foldr1 and foldl1, but instead of reducing from right to left, or left to right, it reduces a vector using a tree-like structure. The depth, or delay, of the structure produced by "fold f xs", is hence O(log_2(length xs)), and not O(length xs).

NB: The binary operator "f in fold f xs" must be associative. NB: Not synthesisable

fold f (x1 :> x2 :> ... :> xn1 :> xn :> Nil) == ((x1 `f` x2) `f` ...) `f` (... `f` (xn1 `f` xn))
fold f (x1 :> Nil)                           == x1
fold f Nil                                   == TYPE ERROR

>>> fold (+) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
15

scanl :: (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b

scanl is similar to foldl, but returns a vector of successive reduced values from the left:

scanl f z (x1 :> x2 :> ... :> Nil) == z :> (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil

>>> scanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
<0,5,9,12,14>

NB:

last (scanl f z xs) == foldl f z xs

scanr :: (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b

scanr is similar to foldr, but returns a vector of successive reduced values from the right:

scanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> z :> Nil

>>> scanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
<14,9,5,2,0>

NB:

head (scanr f z xs) == foldr f z xs

sscanl :: (b -> a -> b) -> b -> Vec n a -> Vec n b

sscanl is a variant of scanl where the first result is dropped:

sscanl f z (x1 :> x2 :> ... :> Nil) == (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil

>>> sscanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
<5,9,12,14>

sscanr :: (a -> b -> b) -> b -> Vec n a -> Vec n b

sscanr is a variant of scanr that where the last result is dropped:

sscanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> Nil

>>> sscanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
<14,9,5,2>

mapAccumL :: (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)

The mapAccumL function behaves like a combination of map and foldl; it applies a function to each element of a vector, passing an accumulating parameter from left to right, and returning a final value of this accumulator together with the new vector.

>>> mapAccumL (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
(10,<1,2,4,7>)

mapAccumR :: (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)

The mapAccumR function behaves like a combination of map and foldr; it applies a function to each element of a vector, passing an accumulating parameter from right to left, and returning a final value of this accumulator together with the new vector.

>>> mapAccumR (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
(10,<10,8,5,1>)

Special folds

dfold

Arguments

:: Proxy (p :: TyFun Nat * -> *)

The motive

-> (forall l. Proxy l -> a -> (p $ l) -> p $ (l + 1))

Function to fold

-> (p $ 0)

Initial element

-> Vec k a

Vector to fold over

-> p $ k

A dependently typed fold.

NB: Not synthesisable

Using lists, we can define append (++) using foldr:

>>> import qualified Prelude
>>> let append xs ys = Prelude.foldr (:) ys xs
>>> append [1,2] [3,4]
[1,2,3,4]

However, when we try to do the same for Vec:

append xs ys = foldr (:>) ys xs

We get a type error

>>> let append' xs ys = foldr (:>) ys xs

<interactive>:...
    Occurs check: cannot construct the infinite type: n1 ~ n1 + 1
    Expected type: a -> Vec n1 a -> Vec n1 a
      Actual type: a -> Vec n1 a -> Vec (n1 + 1) a
    Relevant bindings include
      ys :: Vec n1 a (bound at ...)
      append' :: Vec n a -> Vec n1 a -> Vec n1 a
        (bound at ...)
    In the first argument of ‘foldr’, namely ‘(:>)’
    In the expression: foldr (:>) ys xs

The reason is that the type of foldr is:

>>> :t foldr
foldr :: (a -> b -> b) -> b -> Vec n a -> b

While the type of (:>) is:

>>> :t (:>)
(:>) :: a -> Vec n a -> Vec (n + 1) a

We thus need a fold function that can handle the growing vector type: dfold. Compared to foldr, dfold takes an extra parameter, called the motive, that allows the folded function to have an argument and result type that depends on the current index into the vector. Using dfold, we can now correctly define (++):

import Data.Singletons.Prelude
import Data.Proxy

data Append (m :: Nat) (a :: *) (f :: TyFun Nat *) :: *
type instance Apply (Append m a) l = Vec (l + m) a

append' xs ys = dfold (Proxy :: Proxy (Append m a)) (const (:>)) ys xs

We now see that append has the appropriate type:

>>> :t append'
append' :: Vec k a -> Vec m a -> Vec (k + m) a

And that it works:

>>> append' (1 :> 2 :> Nil) (3 :> 4 :> Nil)
<1,2,3,4>

vfold :: (forall l. a -> Vec l b -> Vec (l + 1) b) -> Vec k a -> Vec k b

Specialised version of dfold that builds a triangular computational structure.

NB: Not synthesisable

Example:

cs a b     = if a > b then (a,b) else (b,a)
csRow y xs = let (y',xs') = mapAccumL cs y xs in xs' <: y'
csSort     = vfold csRow

Builds a triangular structure of compare and swaps to sort a row.

>>> csSort (7 :> 3 :> 9 :> 1 :> Nil)
<1,3,7,9>

Indexing Vectors

(!!) :: (KnownNat n, Integral i) => Vec n a -> i -> a

Vector index (subscript) operator.

NB: vector elements have an ASCENDING subscript starting from 0 and ending at maxIndex.

>>> (1:>2:>3:>4:>5:>Nil) !! 4
5
>>> (1:>2:>3:>4:>5:>Nil) !! maxIndex (1:>2:>3:>4:>5:>Nil)
5
>>> (1:>2:>3:>4:>5:>Nil) !! 1
2
>>> (1:>2:>3:>4:>5:>Nil) !! 14
*** Exception: CLaSH.Sized.Vector.(!!): index 14 is larger than maximum index 4

replace :: (KnownNat n, Integral i) => Vec n a -> i -> a -> Vec n a

Replace an element of a vector at the given index (subscript).

NB: vector elements have an ASCENDING subscript starting from 0 and ending at maxIndex.

>>> replace (1:>2:>3:>4:>5:>Nil) 3 7
<1,2,3,7,5>
>>> replace (1:>2:>3:>4:>5:>Nil) 0 7
<7,2,3,4,5>
>>> replace (1:>2:>3:>4:>5:>Nil) 9 7
<1,2,3,4,*** Exception: CLaSH.Sized.Vector.replace: index 9 is larger than maximum index 4

maxIndex :: KnownNat n => Vec n a -> Integer

Index (subscript) of the last element in a Vector

>>> maxIndex (6 :> 7 :> 8 :> Nil)
2

length :: KnownNat n => Vec n a -> Integer

Length of a Vector as an Integer

>>> length (6 :> 7 :> 8 :> Nil)
3

Generating Vectors

replicate :: SNat n -> a -> Vec n a

replicate n a returns a vector that has n copies of a

>>> replicate (snat :: SNat 3) 6
<6,6,6>
>>> replicate d3 6
<6,6,6>

repeat :: KnownNat n => a -> Vec n a

repeat a creates a vector with as many copies of a as demanded by the context

>>> repeat 6 :: Vec 5 Int
<6,6,6,6,6>

iterate :: SNat n -> (a -> a) -> a -> Vec n a

iterate n f x returns a vector starting with x followed by n repeated applications of f to x

iterate (snat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
iterate d4 f x               == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)

>>> iterate d4 (+1) 1
<1,2,3,4>

iterateI :: KnownNat n => (a -> a) -> a -> Vec n a

iterate f x returns a vector starting with x followed by n repeated applications of f to x, where n is determined by the context

iterateI f x :: Vec 3 a == (x :> f x :> f (f x) :> Nil)

>>> iterateI (+1) 1 :: Vec 3 Int
<1,2,3>

generate :: SNat n -> (a -> a) -> a -> Vec n a

generate n f x returns a vector with n repeated applications of f to x

generate (snat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
generate d4 f x               == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)

>>> generate d4 (+1) 1
<2,3,4,5>

generateI :: KnownNat n => (a -> a) -> a -> Vec n a

generate f x returns a vector with n repeated applications of f to x, where n is determined by the context

generateI f x :: Vec 3 a == (f x :> f (f x) :> f (f (f x)) :> Nil)

>>> generateI (+1) 1 :: Vec 3 Int
<2,3,4>

Misc

reverse :: Vec n a -> Vec n a

Returns the elements in a vector in reverse order

>>> reverse (1:>2:>3:>4:>Nil)
<4,3,2,1>

toList :: Vec n a -> [a]

Convert a vector to a list

>>> toList (1:>2:>3:>Nil)
[1,2,3]

NB: Not synthesisable

v :: Lift a => [a] -> ExpQ

Create a vector literal from a list literal

$(v [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)

>>> [1 :: Signed 8,2,3,4,5]
[1,2,3,4,5]
>>> $(v [1::Signed 8,2,3,4,5])
<1,2,3,4,5>

lazyV :: KnownNat n => Vec n a -> Vec n a

For when your vector functions are too strict in their arguments

For example:

-- Bubble sort for 1 iteration
sortV xs = map fst sorted <: (snd (last sorted))
 where
   lefts  = head xs :> map snd (init sorted)
   rights = tail xs
   sorted = zipWith compareSwapL lefts rights

-- Compare and swap
compareSwapL a b = if a < b then (a,b)
                            else (b,a)

Will not terminate because zipWith is too strict in its second argument:

>>> sortV (4 :> 1 :> 2 :> 3 :> Nil)
<*** Exception: <<loop>>

In this case, adding lazyV on zipWiths second argument:

sortVL :: (Ord a, KnownNat (n+1)) => Vec (n + 2)  a -> Vec (n + 2) a
sortVL xs = map fst sorted <: (snd (last sorted))
 where
   lefts  = head xs :> map snd (init sorted)
   rights = tail xs
   sorted = zipWith compareSwapL (lazyV lefts) rights

Results in a successful computation:

>>> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
<1,2,3,4>

NB: There is also a solution using flip, but it slightly obfuscates the meaning of the code:

sortV_flip xs = map fst sorted <: (snd (last sorted))
 where
   lefts  = head xs :> map snd (init sorted)
   rights = tail xs
   sorted = zipWith (flip compareSwapL) rights lefts

>>> sortV_flip (4 :> 1 :> 2 :> 3 :> Nil)
<1,2,3,4>

asNatProxy :: Vec n a -> Proxy n

Vector as a Proxy for Nat

Functions for the BitPack instance

concatBitVector# :: KnownNat m => Vec n (BitVector m) -> BitVector (n * m)

unconcatBitVector# :: (KnownNat n, KnownNat m) => BitVector (n * m) -> Vec n (BitVector m)