Vectors
Basics
The Vector
type represents a mathematical vector, or in programming
terms can be thought of as a fixedlength array.
One potentially unusual aspect in Vehicle is that the size of the vector
(i.e the number of items it contains) must be known statically
at compile time. This allows Vehicle to check for the presence of
outofbounds errors at compile time rather than run time.
The full type is therefore written as Vector A n
, which
represents the type of vectors with n
elements of type A
.
For example, Vector Rat 10
is a vector of length 10 that contains
rational numbers, and Vector (List Nat) 2
is a vector of length 2
that contains lists of natural numbers.
Creation
There are three ways to create an instance of a vector:
Use the same syntax as when creating a
List
, i.e.[x_1, ..., x_n]
. For example:myVector1 : Vector Rat 3 myVector1 = [ 0.1, 0.3, 0.1 ]
The typechecker will ensure that all vectors written in this way are of the correct size. For example the following would result in an error:
myBadVector : Vector Rat 3 myBadVector = [ 0.1, 0.3 ]
as the size of the vector is
3
but only 2 elements have been provided.While it is possible to use this method to write out small vectors, writing out large vectors this way is clearly impractical.
Therefore the second method is to use the
foreach
constructor, which is used to provide a value for each indexi
. This method is useful if the vector has some regular structure. For example:myVector2 : Vector Rat 100 myVector2 = foreach i . 0
constructs a vector of 100 rationals all of which are
0
, andmyVector3 : Vector Rat 100 myVector3 = foreach i . if i < 20 then 1 else 0
constructs a vector of 100 rationals where the first 20 elements are
1
and the remaining are0
.When using the
foreach
to construct a vector of sizen`
the type of variablei
isIndex n
. See the Index section for more details.The final way vectors can be created is to load them as a
dataset
, e.g.@dataset myVector4 : Vector Rat 10000
which allows the loading of large vectors with no regular structure. See the section on datasets for more details.
Operations
The following operations over vectors are currently supported:
Operation 
Symbol 
Type 
Example 
Description 

Lookup 



Extract the value at a given index of the vector. 
Map 



Apply the function 
Addition 



Pointwise add the values in two vectors together. Only valid
if addition is defined for the type of elements 
Subtraction 



Pointwise subtract the values in the first vector from the values
in the second. Only valid if subtraction is defined for the type of
elements 
Fold 



Reduce the vector to a single value by iterating the function f repeatedly with the head of the vector. 
Indexing
The type of the lookup operator !
given above requires that it
takes a value of type Index d
as its second argument.
The set of valid instances of this type are the natural numbers
{0, 1, ..., d1}
.
This therefore eliminates out of bounds errors by ensuring that
one can never index into a vector using a value greater than its
size.
Indices can be written as any other natural number would be, and
the typechecker will automatically infer they should be of type
Index
from their use.
For example:
@dataset
myVector : Vector Rat [10]
firstElement : Rat
firstElement = myVector ! 0
is valid but the following is not as 10
is out of bounds:
invalidElement : Rat
invalidElement = myVector ! 10
Most arithmetic operations over Index
type are not closed with
respect to the type, e.g. adding 3 : Index 5
and 4 : Index 5
results in 7
which is not a member of Index 5
. Consequently
the set of operations supported by Index
types is extremely limited:
Operation 
Symbol 
Type 
Example 

Less than or equal 



Less than 



Greater than or equal 



Greater than 



Nonconstant sizes
Although the size of a vector is usually a constant (e.g. 10
),
Vehicle allows them to be any valid expression of type Nat
.
For example if d
is some other variable then:
Vector Rat (1 + d)
is the type of vectors of length1 + d
.
Vector Rat (2 * d)
is the type of vectors of length2 * d
.
Similarly, the size of the Index
type can be any valid expression of
type Nat
, e.g. Index (1 + d)
.