Vectors

Basics

The Vector type represents a mathematical vector, or in programming terms can be thought of as a fixed-length 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 out-of-bounds 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:

1. 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 type-checker 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.

2. Therefore the second method is to use the foreach constructor, which is used to provide a value for each index i. 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, and

   myVector3 : 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 are 0.

   When using the foreach to construct a vector of size n` the type of variable i is Index n. See the Index section for more details.

3. 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	!	Vector A d -> Index d -> A	v ! i	Extract the value at a given index of the vector.
Map	map	(A -> B) -> Vector A d -> Vector B d	map f v	Apply the function f to every value in the vector.
Addition	+	Vector A d -> Vector A d -> Vector A d	v1 + v2	Pointwise add the values in two vectors together. Only valid if addition is defined for the type of elements A.
Subtraction	-	Vector A d -> Vector A d -> Vector A d	v1 - v2	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 A.
Fold	fold	(A -> B -> B) -> B -> Vector A d -> B	fold f e v	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, ..., d-1}. 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 type-checker 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	<=	Index d -> Index d -> Bool	x <= y
Less than	<	Index d -> Index d -> Bool	x < y
Greater than or equal	>=	Index d -> Index d -> Bool	x >= y
Greater than	>	Index d -> Index d -> Bool	x >= y

Non-constant 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 length 1 + d.

• Vector Rat (2 * d) is the type of vectors of length 2 * d.

Similarly, the size of the Index type can be any valid expression of type Nat, e.g. Index (1 + d).