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
//
val nrow = mtrxszref_get_nrow (M)
//
fnx loop1
  (i: size_t): void =
  if i < nrow then loop2 (i, 0) 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 (0)
end // end of [mtrxszref_transpose]