CLaSH.Sized.Vector

Vector constructors

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

Fixed size vectors

• Lists with their length encoded in their type
• Vector elements have a descending subscript starting from maxIndex (vlength - 1) and ending at 0

>>> (3:>4:>5:>Nil)
<3,4,5>
>>> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 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)

Foldable (Vec n)

Eq a => Eq (Vec n a)

Show a => Show (Vec n a)

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

Pack (Vec n a)

CPack (Vec n a)

type CSignalP t (Vec n a) = Vec n (CSignal t a)

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

type SignalP (Vec n a) = Vec n (Signal a)

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

Add an element to the tail of the vector

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

Standard Vector functions

Extracting sub-Vectors

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

Extract the first element of a vector

>>> vhead (1:>2:>3:>Nil)
1
>>> vhead 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 ‘vhead’, namely ‘Nil’
      In the expression: vhead Nil

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

Extract the elements after the head of a vector

>>> vtail (1:>2:>3:>Nil)
<2,3>
>>> vtail 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 ‘vtail’, namely ‘Nil’
      In the expression: vtail Nil

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

Extract the last element of a vector

>>> vlast (1:>2:>3:>Nil)
3
>>> vlast 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 ‘vlast’, namely ‘Nil’
      In the expression: vlast Nil

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

Extract all the elements of a vector except the last element

>>> vinit (1:>2:>3:>Nil)
<1,2>
>>> vinit 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 ‘vinit’, namely ‘Nil’
      In the expression: vinit Nil

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

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

>>> vtake (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
<1,2,3>
>>> vtake d3               (1:>2:>3:>4:>5:>Nil)
<1,2,3>
>>> vtake d0               (1:>2:>Nil)
<>
>>> vtake 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 ‘vtake’, namely ‘(1 :> 2 :> Nil)’
      In the expression: vtake d4 (1 :> 2 :> Nil)
      In an equation for ‘it’: it = vtake d4 (1 :> 2 :> Nil)

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

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

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

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

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

>>> vdrop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
<4,5>
>>> vdrop d3               (1:>2:>3:>4:>5:>Nil)
<4,5>
>>> vdrop d0               (1:>2:>Nil)
<1,2>
>>> vdrop 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

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

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

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

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

vexact n xs returns n'th element of xs

NB: vector elements have a descending subscript starting from maxIndex and ending at 0

>>> vexact (snat :: SNat 1) (1:>2:>3:>4:>5:>Nil)
4
>>> vexact d1               (1:>2:>3:>4:>5:>Nil)
4

vselect :: ((f + (s * n)) + 1) <= i => SNat f -> SNat s -> SNat (n + 1) -> Vec i a -> Vec (n + 1) a

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

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

vselectI :: (((f + (s * n)) + 1) <= i, KnownNat (n + 1)) => SNat f -> SNat s -> Vec i a -> Vec (n + 1) a

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

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

Combining Vectors

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

Add an element to the head of the vector, and extract all elements of the resulting vector except the last element

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

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

Add an element to the tail of the vector, and extract all elements of the resulting vector except the first element

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

(<++>) :: 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>

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

Concatenate a vector of vectors

>>> vconcat ((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>

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

vzip takes two lists and returns a list of corresponding pairs.

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

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

vunzip transforms a list of pairs into a list of first components and a list of second components.

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

Splitting Vectors

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

Split a vector into two vectors at the given point

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

vsplitI :: 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

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

vunconcat :: 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

>>> vunconcat 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>>

vunconcatI :: (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

>>> vunconcatI (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>>

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

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

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

Applying functions to Vector elements

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

vmap f xs is the list obtained by applying f to each element of xs, i.e.,

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

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

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

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

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

vfoldr, 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:

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

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

vfoldl, 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:

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

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

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

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

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

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

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

Indexing Vectors

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

Vector index (subscript) operator, descending from maxIndex, where the last element has subscript 0.

>>> (1:>2:>3:>4:>5:>Nil) ! 4
1
>>> (1:>2:>3:>4:>5:>Nil) ! maxIndex
1
>>> (1:>2:>3:>4:>5:>Nil) ! 1
4
>>> (1:>2:>3:>4:>5:>Nil) ! 14
*** Exception: index out of bounds

vreplace :: (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 a descending subscript starting from maxIndex and ending at 0

>>> vreplace (1:>2:>3:>4:>5:>Nil) 3 7
<1,7,3,4,5>
>>> vreplace (1:>2:>3:>4:>5:>Nil) 0 7
<1,2,3,4,7>
>>> vreplace (1:>2:>3:>4:>5:>Nil) 9 7
<*** Exception: index out of bounds

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

Index (subscript) of the head of the Vector

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

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

Length of a Vector as an Integer

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

Generating Vectors

vcopy :: SNat n -> a -> Vec n a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Misc

vreverse :: Vec n a -> Vec n a

Returns the elements in a list in reverse order

>>> vreverse (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]

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 = vmap fst sorted <: (snd (vlast sorted))
 where
   lefts  = vhead xs :> vmap snd (vinit sorted)
   rights = vtail xs
   sorted = vzipWith compareSwapL lefts rights

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

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

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

In this case, adding lazyV on vzipWiths second argument:

sortVL xs = vmap fst sorted <: (snd (vlast sorted))
 where
   lefts  = vhead xs :> vmap snd (vinit sorted)
   rights = vtail xs
   sorted = vzipWith compareSwapL (lazyV lefts) rights

Results in a successful computation:

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

asNatProxy :: Vec n a -> Proxy n

Vector as a Proxy for Nat

Alternative Vector functions

vhead' :: 1 <= n => Vec n a -> a

Same as vhead, but with a "(1 <= n)" constraint and "Vec n a" argument, instead of a "Vec (n + 1) a" argument