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 Rat [24, 24] would be a 24-by-24 matrix of rational numbers.

As might be expected, the Tensor is really just a convenient wrapper around multiple Vector types, and therefore obeys the following laws:

1. A tensor type with an empty list of dimensions is equivalent to its element type, e.g. Tensor Rat [] is equivalent to Rat.

2. A tensor type with an non-empty list of dimensions d :: ds is equivalent to a vector of length d whose elements are tensors of dimensions ds, e.g. Tensor Rat [2,3,4] is equivalent to Vector (Tensor Rat [3,4]) 2 (and therefore Vector (Vector (Vector Rat 4) 3) 2)).

Other laws follow directly from these two. For example:

• The type of a tensor of tensors is equivalent to a type of tensors with the dimensions concatenated, e.g. Tensor (Tensor Rat [24, 20]) [100] is equivalent to Tensor Rat [100, 24, 20].

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 Rat [2, 2]
   identity = [ [1, 0], [0, 1] ]
   

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

   identity : Tensor Rat [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 Rat [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 Rat [10000, 10000]
   

   See the section on datasets for more details.

Operations

The following operations over tensors are currently supported:

Operation	Symbol	Type	Example	Description
Lookup	!	Tensor A (d :: ds) -> Index d -> Tensor A ds	t ! i	Extract the value at a given index of the tensor.
Map	map	(Tensor A ds -> Tensor B ds) -> Tensor A (d :: ds) -> Vector B (d :: ds)	map f t	Apply the function f to every value in the tensor.
Addition	+	Tensor A ds -> Tensor A ds -> Tensor A ds	t1 + t2	Pointwise add the values in two tensors together. Only valid if addition is defined for the type of elements A.
Subtraction	-	Tensor A ds -> Tensor A ds -> Tensor A ds	t1 - t2	Pointwise subtract the values in the first tensor from the values in the second. Only valid if subtraction is defined for the type of elements A.
Fold	fold	(Tensor A ds -> B -> B) -> B -> Tensor A (d : ds) -> B	fold f e v	Reduce the tensor to a single value by iterating the function f repeatedly with the head of the tensor.

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 Rat [2 + d] is the type of vectors of length 2 + d.

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