Tensors

Basics

Tensors are the basic abstraction underlying most neural network libraries. If the Vector type can be thought of as representing a fixed-length array, then the Tensor type can be thought of as a multi-dimensional array.

Tensor types are written as Tensor A ds where A is the type of data stored within the tensor and ds is a list of natural numbers that represent its dimensions. For example Tensor Real [24, 24] would be a 24-by-24 matrix of real numbers.

Note that a 0-dimensional tensor is equivalent to the raw value in Vehicle, e.g. the type Tensor Real [] can be used interchangably as Real.

Creation

As tensors are really just vectors underneath the hood, they can be created by the same three mechanisms:

1. Use the same syntax as lists, e.g. the 2-by-2 identity matrix can be defined as follows:

   identity : Tensor Real [2, 2]
   identity = [ [1, 0], [0, 1] ]
   

   As with the Vector type, the type-checker will ensure that all tensors are of the correct size. For example, the following would result in an error:

   identity : Tensor Real [2, 2]
   identity = [ [1, 0, 1] , [0, 1, 1] ]
   

   as the second dimension is 2 but three elements have been provided.

2. The foreach syntax:

   identity : Tensor Real [1000,1000]
   identity = foreach i j . if i == j then 1 else 0
   

3. The final way tensors can be created is to load them as a dataset, e.g.

   @dataset
   myLargeTensor : Tensor Real [10000, 10000]
   

   See the section on datasets for more details.

Operations

The following operations over tensors are currently supported:

Operation	Syntax	Type	Support
Lookup	e ! i	Tensor A [d, ds] → Index d → Tensor A ds
Foreach	foreach i . e	(Index d → Tensor A ds) → Tensor A [d, ds]
Comparisons	x < y x > y x <= y x >= y x == y x != y	Tensor A ds → Tensor A ds → Bool (if A supports comparisons)
Pointwise comparisons	x .< y x .> y x .<= y x .>= y x .== y x .!= y	Tensor A ds → Tensor A ds → Tensor Bool ds (if A supports comparisons)
Pointwise and	t1 and t2	Tensor Bool ds → Tensor Bool ds → Tensor Bool ds
Pointwise or	t1 or t2	Tensor Bool ds → Tensor Bool ds → Tensor Bool ds
Reduce and	reduceAnd e t	Bool → Tensor Bool ds → Bool
Reduce or	reduceOr e t	Bool → Tensor Bool ds → Bool
Pointwise add	t1 + t2	Tensor A ds → Tensor A ds → Tensor A ds (if A supports +)
Pointwise subtract	t1 - t2	Tensor A ds → Tensor A ds → Tensor A ds (if A supports -)
Pointwise multiply	t1 * t2	Tensor A ds → Tensor A ds → Tensor A ds (if A supports *)
Pointwise divide	t1 / t2	Tensor A ds → Tensor A ds → Tensor A ds (if A supports /)
Reduce add	reduceAdd e t	A → Tensor A ds → A (if A supports +)
Reduce multiply	reduceMul e t	A → Tensor A ds → A (if A supports *)
Reduce min	reduceMin e t	A → Tensor A ds → A (if A supports min)
Reduce max	reduceMax e t	A → Tensor A ds → A (if A supports max)

Non-constant dimensions

As with vectors, although the dimensions of a tensor are usually a list of constants (e.g. [1, 2, 3]), in practice they can be any valid expression of type List Nat. For example:

• Tensor Real [2 + d] is the type of vectors of length 2 + d.

• Tensor Real (10 :: ds) is the type of tensors whose first dimension is of size 10 and then has remaining dimensions ds.