Tensors
Basics
Tensors are the basic abstraction underlying most neural network libraries.
If the Vector
type can be thought of as representing a fixedlength
array, then the Tensor
type can be thought of as a multidimensional 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 24by24 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:
A tensor type with an empty list of dimensions is equivalent to its element type, e.g.
Tensor Rat []
is equivalent toRat
.A tensor type with an nonempty list of dimensions
d :: ds
is equivalent to a vector of lengthd
whose elements are tensors of dimensionsds
, e.g.Tensor Rat [2,3,4]
is equivalent toVector (Tensor Rat [3,4]) 2
(and thereforeVector (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 toTensor Rat [100, 24, 20]
.
Creation
As tensors are really just vectors underneath the hood, they can be created by the same three mechanisms:
Use the same syntax as lists, e.g. the 2by2 identity matrix can be defined as follows:
identity : Tensor Rat [2, 2] identity = [ [1, 0], [0, 1] ]
Again the typechecker 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.The
foreach
syntax:identity : Tensor Rat [1000,1000] identity = foreach i j . if i == j then 1 else 0
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 



Extract the value at a given index of the tensor. 
Map 



Apply the function 
Addition 



Pointwise add the values in two tensors together. Only valid
if addition is defined for the type of elements 
Subtraction 



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 
Fold 



Reduce the tensor to a single value by iterating the function f repeatedly with the head of the tensor. 
Nonconstant 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 length2 + d
.
Tensor Rat (10 :: ds)
is the type of tensors whose first dimension is of size 10 and then has remaining dimensionsds
.