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].


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.

    myLargeTensor : Tensor Rat [10000, 10000]

    See the section on datasets for more details.


The following operations over tensors are currently supported:








Tensor A (d :: ds) -> Index d -> Tensor A ds

t ! i

Extract the value at a given index of the tensor.



(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.



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.



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.



(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.