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

NB: Not synthesisable

Foldable (Vec n)

Traversable (Vec n)

NB: Not synthesisable

Eq a => Eq (Vec n a)

Show a => Show (Vec n a)

(Default a, KnownNat n) => Default (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 (CSignal 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 4 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 ‘vhead’, namely ‘Nil’
      In the expression: vhead 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 ‘vtail’, namely ‘Nil’
      In the expression: vtail 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 ‘vlast’, namely ‘Nil’
      In the expression: vlast 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 ‘vinit’, namely ‘Nil’
      In the expression: vinit 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 ‘vtake’, namely ‘(1 :> 2 :> Nil)’
      In the expression: vtake d4 (1 :> 2 :> Nil)
      In an equation for ‘it’: it = vtake 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>

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

exact n xs returns n'th element of xs

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

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

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

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

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

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

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

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

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

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:

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.

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

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
5
>>> (1:>2:>3:>4:>5:>Nil) !! 1
2
>>> (1:>2:>3:>4:>5:>Nil) !! 14
*** Exception: (!!): Index 14 is out of bounds [0..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
<*** Exception: replace: Index 9 is out of bounds [0..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 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)