Matrices

A matrix in ATS is just a two-dimensional array but it is represented by a one-dimensional array and the representation is of the row-major style (in contrast to the column-major style). Given a type T, the type mtrxszref(T) is for a matrix combined with its number of rows and number of columns such that each element stored in the matrix is of the type T. I will loosely refer to values of the type mtrxszref(T) as matrices from now on. If there is a clear need to avoid potential confusion, I may also refer to them as matrix0-values.

Given a matrix M of dimension m by n, the expression M[i,j] means to fetch the content of the cell in M that is indexed by (i, j), where i and j are natural numbers strictly less than m and n, respectively. The expression M[i,j] can also be used as a left value. For instance, the assignment (M[i,j] := exp) means to evaluate exp to a value and then store the value into the cell in M that is indexed by (i, j).

Various functions and function templates on matrix0-values are declared in the file matrixref.sats, which is automatically loaded by atsopt. For instance, three function templates and two polymorphic functions on matrices are depicted by the following interfaces:

// fun{a:t@ype} mtrxszref_make_elt // template (row: size_t, col: size_t, x: a): mtrxszref (a) // fun mtrxszref_get_nrow{a:t@ype}(M: mtrxszref a): size_t // polyfun fun mtrxszref_get_ncol{a:t@ype}(M: mtrxszref a): size_t // polyfun // fun{a:t@ype} mtrxszref_get_elt_at // template (M: mtrxszref a, i: size_t, j: size_t): a // M[i,j] fun{a:t@ype} mtrxszref_set_elt_at // template (M: mtrxszref a, i: size_t, j: size_t, x: a): void // M[i,j] := x //

Given a type T and three values nrow, ncol and init of the types size_t, size_t and T, respectively, mtrxszref_make_elt<T> (row, col, init) returns a matrix of the type mtrxszref(T) such that the dimension of the matrix is nrow by ncol and each cell in the matrix is initialized with the value init. Given a matrix M of the type mtrxszref(T) for some T, mtrxszref_get_nrow(M) and mtrxszref_get_ncol(M) return the number of rows and the number of columns of M, respectively, which are both of the type size_t. For convenience, mtrxszref_get_nrow(M) and mtrxszref_get_ncol(M) can also be written as M.nrow and M.ncol, respectively. As for matrix access and update, the function templates mtrxszref_get_elt_at and mtrxszref_set_elt_at can be called, respectively. For convenience, bracket notation can used for these functions.

Let us now take a look at an example. The following defined function mtrxszref_transpose turns a given matrix into its transpose:

fun{a:t@ype} mtrxszref_transpose (M: mtrxszref a): void = let // postfix sz #define sz(x) i2sz(x) // val nrow = mtrxszref_get_nrow(M) // fnx loop1 (i: size_t): void = if i < nrow then loop2(i, 0sz) else () // and loop2 (i: size_t, j: size_t): void = if j < i then let val tmp = M[i,j] in M[i,j] := M[j,i]; M[j,i] := tmp; loop2(i, j+1) end else loop1(i+1) // end of [if] // in loop1 (0sz) end // end of [mtrxszref_transpose]

Note that 0sz expands to i2sz(0), which casts 0 of int into 0 of size_t. The matrix M is assumed to be a square, that is, its number of rows equals its number of columns. Note that the two functions loop1 and loop2 are defined mutually tail-recursively, and the keyword fnx indicates the need to combine the bodies of loop1 and loop2 so that mutual recursive tail-calls in these function bodies can be compiled into direct local jumps.