Safe Haskell | None |
---|---|

Language | Haskell2010 |

- data Vec :: Nat -> * -> * where
- (<:) :: Vec n a -> a -> Vec (n + 1) a
- vhead :: Vec (n + 1) a -> a
- vtail :: Vec (n + 1) a -> Vec n a
- vlast :: Vec (n + 1) a -> a
- vinit :: Vec (n + 1) a -> Vec n a
- vtake :: SNat m -> Vec (m + n) a -> Vec m a
- vtakeI :: KnownNat m => Vec (m + n) a -> Vec m a
- vdrop :: SNat m -> Vec (m + n) a -> Vec n a
- vdropI :: KnownNat m => Vec (m + n) a -> Vec n a
- vexact :: SNat m -> Vec (m + (n + 1)) a -> a
- vselect :: ((f + (s * n)) + 1) <= i => SNat f -> SNat s -> SNat (n + 1) -> Vec i a -> Vec (n + 1) a
- vselectI :: (((f + (s * n)) + 1) <= i, KnownNat (n + 1)) => SNat f -> SNat s -> Vec i a -> Vec (n + 1) a
- (+>>) :: a -> Vec n a -> Vec n a
- (<<+) :: Vec n a -> a -> Vec n a
- (<++>) :: Vec n a -> Vec m a -> Vec (n + m) a
- vconcat :: Vec n (Vec m a) -> Vec (n * m) a
- vzip :: Vec n a -> Vec n b -> Vec n (a, b)
- vunzip :: Vec n (a, b) -> (Vec n a, Vec n b)
- vsplit :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
- vsplitI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)
- vunconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)
- vunconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)
- vmerge :: Vec n a -> Vec n a -> Vec (n + n) a
- vmap :: (a -> b) -> Vec n a -> Vec n b
- vzipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- vfoldr :: (a -> b -> b) -> b -> Vec n a -> b
- vfoldl :: (b -> a -> b) -> b -> Vec n a -> b
- vfoldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a
- vfoldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a
- vscanl :: KnownNat n => (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
- vscanr :: KnownNat n => (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
- vscanl1 :: KnownNat n => (a -> a -> a) -> Vec n a -> Vec n a
- vscanr1 :: KnownNat n => (a -> a -> a) -> Vec n a -> Vec n a
- vmapAccumL :: KnownNat n => (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
- vmapAccumR :: KnownNat n => (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
- (!) :: (KnownNat n, Integral i) => Vec n a -> i -> a
- vreplace :: (KnownNat n, Integral i) => Vec n a -> i -> a -> Vec n a
- maxIndex :: KnownNat n => Vec n a -> Integer
- vlength :: KnownNat n => Vec n a -> Integer
- vcopy :: SNat n -> a -> Vec n a
- vcopyI :: KnownNat n => a -> Vec n a
- viterate :: SNat n -> (a -> a) -> a -> Vec n a
- viterateI :: KnownNat n => (a -> a) -> a -> Vec n a
- vgenerate :: SNat n -> (a -> a) -> a -> Vec n a
- vgenerateI :: KnownNat n => (a -> a) -> a -> Vec n a
- vreverse :: Vec n a -> Vec n a
- toList :: Vec n a -> [a]
- v :: Lift a => [a] -> ExpQ
- lazyV :: KnownNat n => Vec n a -> Vec n a
- asNatProxy :: Vec n a -> Proxy n
- vhead' :: 1 <= n => Vec n a -> a

`Vec`

tor constructors

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

Fixed size vectors

- Lists with their length encoded in their type
`Vec`

tor elements have a DESCENDING subscript starting from`maxIndex`

(`vlength`

- 1) and ending at 0

`>>>`

<3,4,5>`(3:>4:>5:>Nil)`

`>>>`

(3:>4:>5:>Nil) :: Num a => Vec 3 a`:t (3:>4:>5:>Nil)`

Functor (Vec n) | |

KnownNat n => Applicative (Vec n) | |

Foldable (Vec n) | |

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

Add an element to the tail of the vector

`>>>`

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

`>>>`

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

# Standard `Vec`

tor functions

## Extracting sub-`Vec`

tors

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

Extract the first element of a vector

`>>>`

1`vhead (1:>2:>3:>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`vhead Nil`

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

Extract the elements after the head of a vector

`>>>`

<2,3>`vtail (1:>2:>3:>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`vtail Nil`

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

Extract the last element of a vector

`>>>`

3`vlast (1:>2:>3:>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`vlast Nil`

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

Extract all the elements of a vector except the last element

`>>>`

<1,2>`vinit (1:>2:>3:>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`vinit Nil`

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

`vtake`

`n`

, applied to a vector `xs`

, returns the `n`

-length prefix of `xs`

`>>>`

<1,2,3>`vtake (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)`

`>>>`

<1,2,3>`vtake d3 (1:>2:>3:>4:>5:>Nil)`

`>>>`

<>`vtake d0 (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)`vtake d4 (1:>2:>Nil)`

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

`vtakeI`

`xs`

, returns the prefix of `xs`

as demanded by the context

`>>>`

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

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

`vdrop`

`n xs`

returns the suffix of `xs`

after the first `n`

elements

`>>>`

<4,5>`vdrop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)`

`>>>`

<4,5>`vdrop d3 (1:>2:>3:>4:>5:>Nil)`

`>>>`

<1,2>`vdrop d0 (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`vdrop d4 (1:>2:>Nil)`

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

`vdropI`

`xs`

, returns the suffix of `xs`

as demanded by the context

`>>>`

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

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

`vselect`

`f s n xs`

selects `n`

elements with stepsize `s`

and
offset `f`

from `xs`

`>>>`

<2,4,6>`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)`

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

`vselectI`

`f s xs`

selects as many elements as demanded by the context
with stepsize `s`

and offset `f`

from `xs`

`>>>`

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

## Combining `Vec`

tors

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

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

`>>>`

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

`>>>`

<>`1 +>> Nil`

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

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

`>>>`

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

`>>>`

<>`Nil <<+ 1`

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

Append two vectors

`>>>`

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

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

Concatenate a vector of vectors

`>>>`

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

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

`vzip`

takes two vectors and returns a vector of corresponding pairs.

`>>>`

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

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

`vunzip`

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

`>>>`

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

## Splitting `Vec`

tors

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

Split a vector into two vectors at the given point

`>>>`

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

`>>>`

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

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

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

`>>>`

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

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

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

`>>>`

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

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

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

`>>>`

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

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

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

`>>>`

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

## Applying functions to `Vec`

tor elements

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

`vmap`

`f xs`

is the vector 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 Source

`vzipWith`

generalises `vzip`

by zipping with the function given
as the first argument, instead of a tupling function.
For example,

is applied to two vectors to produce the
vector of corresponding sums.`vzipWith`

(+)

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 Source

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

`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

vmapAccumL :: KnownNat n => (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y) Source

vmapAccumR :: KnownNat n => (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y) Source

## Indexing `Vec`

tors

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

Vector index (subscript) operator, DESCENDING from `maxIndex`

, where the
last element has subscript 0.

`>>>`

1`(1:>2:>3:>4:>5:>Nil) ! 4`

`>>>`

1`(1:>2:>3:>4:>5:>Nil) ! maxIndex`

`>>>`

4`(1:>2:>3:>4:>5:>Nil) ! 1`

`>>>`

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

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

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

`>>>`

<1,7,3,4,5>`vreplace (1:>2:>3:>4:>5:>Nil) 3 7`

`>>>`

<1,2,3,4,7>`vreplace (1:>2:>3:>4:>5:>Nil) 0 7`

`>>>`

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

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

Index (subscript) of the head of the `Vec`

tor

`>>>`

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

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

Length of a `Vec`

tor as an Integer

`>>>`

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

## Generating `Vec`

tors

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

`vcopy`

`n a`

returns a vector that has `n`

copies of `a`

`>>>`

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

`>>>`

<6,6,6>`vcopy d3 6`

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

`vcopyI`

`a`

creates a vector with as many copies of `a`

as demanded by the
context

`>>>`

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

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

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

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

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

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

Returns the elements in a vector in reverse order

`>>>`

<4,3,2,1>`vreverse (1:>2:>3:>4:>Nil)`

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

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,2,3,4,5]`[1 :: Signed 8,2,3,4,5]`

`>>>`

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

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

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:

`>>>`

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

In this case, adding `lazyV`

on `vzipWith`

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

`>>>`

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