Type-level representation of zero.

Type-level representation of successor.

The natural number 1 as a type.

The natural number 2 as a type.

The natural number 3 as a type.

The natural number 4 as a type.

The natural number 5 as a type.

The natural number 6 as a type.

The natural number 7 as a type.

The natural number 8 as a type.

The natural number 9 as a type.

The natural number 10 as a type.

The 10th successor of a natural number type. For example, the natural number 18 as a type is

Ten_and Eight

A data type for the natural numbers. Specifically, if n is a type-level natural number, then

NNat n

is a singleton type containing only the natural number n.

Convert an NNat to an Integer.

A type class for the natural numbers. The members are exactly the type-level natural numbers.

Addition of type-level natural numbers.

Multiplication of type-level natural numbers.

Vector n a is the type of lists of length n with elements from a. We call this a "vector" rather than a tuple or list for two reasons: the vectors are homogeneous (all elements have the same type), and they are strict: if any one component is undefined, the whole vector is undefined.

Construct a vector of length 1.

Return the length of a vector. Since this information is contained in the type, the vector argument is never evaluated and can be a dummy (undefined) argument.

Convert a fixed-length list to an ordinary list.

Zip two equal length lists.

Map a function over a fixed-length list.

Create the vector (0, 1, …, n-1).

Create the vector (f(0), f(1), …, f(n-1)).

Construct a vector from a list. Note: since the length of the vector is a type-level integer, it cannot be inferred from the length of the input list; instead, it must be specified explicitly in the type. It is an error to apply this function to a list of the wrong length.

Return the ith element of the vector. Counting starts from 0. Throws an error if the index is out of range.

Return a fixed-length list consisting of a repetition of the given element. Unlike replicate, no count is needed, because this information is already contained in the type. However, the type must of course be inferable from the context.

Turn a list of columns into a list of rows.

Left strict fold over a fixed-length list.

Right fold over a fixed-length list.

Return the tail of a fixed-length list. Note that the type system ensures that this never fails.

Return the head of a fixed-length list. Note that the type system ensures that this never fails.

Append two fixed-length lists.

Version of sequence for fixed-length lists.

An m×n-matrix is a list of n columns, each of which is a list of m scalars. The type of square matrices of any fixed dimension is an instance of the Ring class, and therefore the usual symbols, such as "+" and "*" can be used on them. However, the non-square matrices, the symbols ".+." and ".*." must be used.

Decompose a matrix into a list of columns.

Return the size (m, n) of a matrix, where m is the number of rows, and n is the number of columns. Since this information is contained in the type, the matrix argument is not evaluated and can be a dummy (undefined) argument.

Addition of m×n-matrices. We use a special symbol because m×n-matrices do not form a ring; only n×n-matrices form a ring (in which case the normal symbol "+" also works).

Subtraction of m×n-matrices. We use a special symbol because m×n-matrices do not form a ring; only n×n-matrices form a ring (in which case the normal symbol "-" also works).

Map some function over every element of a matrix.

Create the matrix whose i,j-entry is (i,j). Here i and j are 0-based, i.e., the top left entry is (0,0).

Create the matrix whose i,j-entry is f i j. Here i and j are 0-based, i.e., the top left entry is f 0 0.

Multiplication of a scalar and an m×n-matrix.

Division of an m×n-matrix by a scalar.

Multiplication of m×n-matrices. We use a special symbol because m×n-matrices do not form a ring; only n×n-matrices form a ring (in which case the normal symbol "*" also works).

Return the 0 matrix of the given dimension.

Take the transpose of an m×n-matrix.

Take the adjoint of an m×n-matrix. Unlike adj, this can be applied to non-square matrices.

Return the element in the ith row and jth column of the matrix. Counting of rows and columns starts from 0. Throws an error if the index is out of range.

Return a list of all the entries of a matrix, in some fixed but unspecified order.

Version of sequence for matrices.

Return the trace of a square matrix.

Return the square of the Hilbert-Schmidt norm of an m×n-matrix, defined by ‖M‖² = tr M^†M.

Stack matrices vertically.

Stack matrices horizontally.

Repeat a matrix vertically, according to some vector of scalars.

Vertically concatenate a vector of matrices.

Repeat a matrix horizontally, according to some vector of scalars.

Horizontally concatenate a vector of matrices.

Kronecker tensor of two matrices.

Form a diagonal block matrix.

Form a controlled gate.

A convenient abbreviation for the type of 2×2-matrices.

A convenient abbreviation for the type of 3×3-matrices.

A convenience constructor for matrices: turn a list of columns into a matrix.

Note: since the dimensions of the matrix are type-level integers, they cannot be inferred from the dimensions of the input; instead, they must be specified explicitly in the type. It is an error to apply this function to a list of the wrong dimension.

A convenience constructor for matrices: turn a list of rows into a matrix.

Note: since the dimensions of the matrix are type-level integers, they cannot be inferred from the dimensions of the input; instead, they must be specified explicitly in the type. It is an error to apply this function to a list of the wrong dimension.

A synonym for matrix_of_rows.

Turn a matrix into a list of columns.

Turn a matrix into a list of rows.

A convenience constructor for 2×2-matrices. The arguments are by rows.

A convenience destructor for 2×2-matrices. The result is by rows.

A convenience constructor for 3×3-matrices. The arguments are by rows.

A convenience constructor for 4×4-matrices. The arguments are by rows.

A convenience constructor for 3-dimensional column vectors.

A convenience destructor for 3-dimensional column vectors. This is the inverse of column3.

A convenience constructor for turning a vector into a column matrix.

Controlled-not gate.

Swap gate.

A z-rotation gate, Rsub /z/ = e^−iθZ/2.