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:

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.