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 matrix0(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 matrix0(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 prelude/SATS/matrix0.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} // template
matrix0_make_elt
  (row: size_t, col: size_t, x: a): matrix0 (a)

fun matrix0_row {a:t@ype} (M: matrix0 a): size_t // polyfun
fun matrix0_col {a:t@ype} (M: matrix0 a): size_t // polyfun

fun{a:t@ype}
matrix0_get_elt_at // template
  (M: matrix0 a, i: size_t, j: size_t): a // M[i,j]

fun{a:t@ype}
matrix0_set_elt_at // template
  (M: matrix0 a, i: size_t, j: size_t, x: a): void // M[i,j] := x

Given a type T and three values row, col and init of the types size_t, size_t and T, respectively, matrix0_make_elt<T> (row, col, init) returns a matrix of the type matrix0(T) such that the dimension of the matrix is row by col and each cell in the matrix is initialized with the value init. Given a matrix M of the type matrix0(T) for some T, matrix0_row(M) and matrix0_col(M) return the number of rows and the number of columns of M, respectively, which are both of the type size_t. Also, matrix access and update can be done by calling the function templates matrix0_get_elt_at and matrix0_set_elt_at, respectively.

As an example, the following defined function matrix0_transpose turns a given matrix into its transpose:

fun{a:t@ype}
matrix0_transpose
  (M: matrix0 a): void = let
//
  val nrow = matrix0_row (M)
//
  fn* loop1
    (i: size_t):<cloref1> void =
    if i < nrow then loop2 (i, 0) else ()
  and loop2
    (i: size_t, j: size_t):<cloref1> 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 [matrix0_transpose]