clash-prelude-0.7.2: CAES Language for Synchronous Hardware - Prelude library

Copyright(C) 2013-2015, University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellNone
LanguageHaskell2010
Extensions
  • UndecidableInstances
  • MonoLocalBinds
  • TemplateHaskell
  • ScopedTypeVariables
  • BangPatterns
  • TypeFamilies
  • GADTs
  • GADTSyntax
  • DataKinds
  • FlexibleContexts
  • MagicHash
  • KindSignatures
  • TupleSections
  • RankNTypes
  • TypeOperators
  • ExplicitNamespaces
  • ExplicitForAll

CLaSH.Sized.Vector

Contents

Description

 

Synopsis

Vector constructors

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

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) Source 
KnownNat n => Applicative (Vec n) Source

NB: Not synthesisable

Foldable (Vec n) Source 
Traversable (Vec n) Source

NB: Not synthesisable

Eq a => Eq (Vec n a) Source 
Ord a => Ord (Vec n a) Source 
Show a => Show (Vec n a) Source 
(Default a, KnownNat n) => Default (Vec n a) Source 
Lift a => Lift (Vec n a) Source 
(KnownNat n, KnownNat (BitSize a), BitPack a) => BitPack (Vec n a) Source 
KnownNat n => Bundle (Vec n a) Source 
type Unbundled' t (Vec n a) = Vec n (Signal' t a) Source 
type BitSize (Vec n a) = * n (BitSize a) Source 

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

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 Source

Create a vector of one element

>>> singleton 5
<5>

Standard Vector functions

Extracting sub-Vectors

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

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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

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

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 Source

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 Source

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 Source

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 Source

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

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

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

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

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

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

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

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 Source

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 Source

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 Source

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 Source

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 Source

Index (subscript) of the last element in a Vector

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

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

Length of a Vector as an Integer

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

Generating Vectors

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

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

Returns the elements in a vector in reverse order

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

toList :: Vec n a -> [a] Source

Convert a vector to a list

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

NB: Not synthesisable

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

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 Source

Vector as a Proxy for Nat

Functions for the BitPack instance