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
- (!) :: (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 frommaxIndex
(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
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 Source
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 Vec
tor functions
Extracting sub-Vec
tors
vhead :: Vec (n + 1) a -> a Source
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 Source
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 Source
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 Source
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 Source
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 Source
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 Source
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 Source
vdropI
xs
, returns the suffix of xs
as demanded by the context
>>>
vdropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
<4,5>
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
>>>
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 Source
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 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:>5:>Nil)
<1,3,4>>>>
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
>>>
(3:>4:>5:>Nil) <<+ 1
<4,5,1>>>>
Nil <<+ 1
<>
(<++>) :: 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>
vconcat :: Vec n (Vec m a) -> Vec (n * m) a Source
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) Source
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) Source
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 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
>>>
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) Source
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) Source
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) Source
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 Source
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 Vec
tor elements
vmap :: (a -> b) -> Vec n a -> Vec n b Source
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 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
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:>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 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
>>>
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 Source
Index (subscript) of the head of the Vec
tor
>>>
maxIndex (6 :> 7 :> 8 :> Nil)
2
vlength :: KnownNat n => Vec n a -> Integer Source
Length of a Vec
tor as an Integer
>>>
vlength (6 :> 7 :> 8 :> Nil)
3
Generating Vec
tors
vcopy :: SNat n -> a -> Vec n a Source
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 Source
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 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 list in reverse order
>>>
vreverse (1:>2:>3:>4:>Nil)
<4,3,2,1>
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 = 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 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:
>>>
sortVL (4 :> 1 :> 2 :> 3 :> Nil)
<1,2,3,4>