I use the name *matrix-with-size* to refer to a persistent
matrix with attached dimension information (that is, number of rows and
number of columns). Given a viewtype VT, the type for a matrix-with-size
that contains M rows and N columns of elements of viewtype VT is
mtrxszref(VT, M, N). Essentially, such a value is a boxed
record of three components of types arrayref(VT, N),
size_t(M) and size_t(N). The interfaces for various
functions on persistent matrices-with-size can be found in
prelude/SATS/matrixref.sats.

The following function is commonly used to create a matrix-with-size:

fun{a:t0p} mtrxszref_make_elt (m: size_t, n: size_t, x0: a): mtrxref(a) // end of [mtrxszref_make_elt]

For accessing and updating the content of a matrix-cell, the following two functions mtrxszref_get_at and mtrxszref_set_at can be called:

fun{a:t0p} mtrxszref_get_at (M: mtrxszref(a), i: size_t, j: size_t): (a) fun{a:t0p} mtrxszref_set_at (M: mtrxszref(a), i: size_t, j: size_t, x: a): void

As a simple example, the following code implements a function that transpose the content of the matrix inside a given matrix-with-size:

// extern fun{a:t0p} mtrxszref_transpose (M: mtrxszref(a)): void // implement {a}(*tmp*) mtrxszref_transpose (M) = let // val n = M.nrow() // val () = assertloc(M.nrow() = M.ncol()) // fun loop ( i: size_t, j: size_t ) : void = ( if (j < n) then let val x = M[i,j] val () = M[i,j] := M[j,i] val () = M[j,i] := x in loop(i, succ(j)) end // end of [then] else let val i1 = succ(i) in if i1 < n then loop(i1, succ(i1)) else () end // end of [else] // ) (* end of [loop] *) // in if (n > 0) then loop(i2sz(0), i2sz(1)) else () end // end of [mtrxszref_transpose]

Like arrays-with-size, matrices-with-size are easier to program with than dependently typed matrices. However, the latter can not only lead to more effective error detection at compile-time but also more efficent code execution at run-time. For someone programming in ATS, it is quite reasonable to start out with matrices-with-size and then replace them with matrices when there are clear benefits from doing so.

Please find on-line the entirety of the code used in this chapter.