Persistent Arrays and Matrices

Though arrays are widely used in practice, there are many thorny issues involving arrays that seem to have not been adequately addressed in the literature. In particular, programming can become rather tricky when arrays are used to store resources (e.g., pointers to allocated memory).

In ATS, there are two forms of arrays: linear arrays and persistent arrays. On one hand, a linear array cannot be shared but a persistent array can. On the other hand, a linear array can be explicitly freed but a persistent one cannot. However, a persistent array may be freed by GC. Although persistent arrays are built in terms of linear arrays, it seems easier to explain persistent arrays as such arrays are available in probably any programming language that may be considered practical.

Persistent Arrays

The interfaces for various functions on arrays can be found in the file $ATSHOME/prelude/SATS/array.sats . Given a viewtype VT and an integer I, the type array(VT, I) is for persistent arrays of size I in which each element is of viewtype VT.

Array Creation There are several approaches to creating of persistent arrays in ATS. For instance, the following code in ATS creates an array of integers:

val digits = array @[int][ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]

The type assigned to the variable digits is array(int, 10). We can certainly be more precise by stating that digits is indeed an array of digits:

typedef digit = [i:nat | i < 10] int (i)

// digits: array (digit, 10)
val digits = array @[digit][ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]

A more flexible approach to array creation makes use of the function array_make_fun_tsz, which takes three arguments: a natural number representing the size of the array to be created, a function for array initialization, and the size of array elements. For instance, the previous array of digits can also be created as follows:

val digits =
  array_make_fun_tsz {digit} (10, lam (x, i) =<clo> x := i, sizeof<digit>)

As another example, the following function can be used to create a persisent array of doubles that is initialized with zeros:

fn double_array_make (n: int n): array (double, n) =
  array_make_fun_tsz {double} (n, lam (x, i) =<clo> x := 0.0, sizeof<double>)

Array Subscripting The following two (template) functions array_get_elt_at and array_set_elt_at are for accessing and updating a persistent array, respectively:

fun{a:t@ype} array_get_elt_at {n:nat} (A: array (a, n), i: natLt n):<!ref> a
fun{a:t@ype} array_set_elt_at {n:nat} (A: array (a, n), i: natLt n, x: a):<!ref> void

The symbol [] is overloaded with both array_get_elt_at and array_set_elt_at:

overload [] with array_get_elt_at
overload [] with array_set_elt_at

As an example, we implement as follows a function that squares each element in a given array of doubles:

fn array_square {n:nat} (A: array (double, n)): void = let
  val sz = length A // sz: int n
  fun loop {i:nat | i <= n} .< n-i >. (i: int i): void =
    if i < sz then
      let val x = A[i] in A[i] := x * x; loop (i+1) end
    else ()
in
  loop (0)
end // end of [array_square]

In this code, A[i] and A[i] := x * x are shorthands for array_get_elt_at(A, i) and array_set_elt_at(A, i, x * x), respectively.

There are also library (template) functions foreach_array and iforeach_array for iteration over persistent arrays, which are assigned the following interfaces:

fun{a:t@ype} foreach_array {f:eff} {n:nat}
  (f: a -<f> void, A: array (a, n)):<f,!ref> void

fun{a:t@ype} iforeach_array {f:eff} {n:nat}
  (f: (natLt n, a) -<f> void, A: array (a, n)):<f,!ref> void

For instance, the previous function array_square can be implemented as follows by calling iforeach_array:

fn array_square {n:nat} (A: array (double, n)): void =
  iforeach_array (lam (i, x) =<!ref> A[i] := x * x, A)

Persistent Matrices

A matrix is an array of 2 dimensions. Note that the 2 dimensions of a matrix are not necessarily the same. If they are the same, then the matrix is referred to as a square matrix.

The interfaces for various functions on arrays can be found in the file $ATSHOME/prelude/SATS/matrix.sats . Given a viewtype VT and an integer I and another integer J, the type matrix(VT, I, J) is for persistent matrices of dimensions I (row) and J (column) in which each element is of type VT.

Matrix Creation The approaches to creating matrices resemble those to creating arrays. For instance, the following code creates a square matrix of dimensions 10 by 10:

val mat_10_10 = matrix(10, 10) @[int][
   0,  1,  2,  3,  4,  5,  6,  7,  8,  9
, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19
, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29
, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39
, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49
, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59
, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69
, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79
, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89
, 90, 91, 92, 93, 94, 99, 96, 97, 98, 99
]

This matrix can also be created by calling the function matrix_make_fun_tsz, which is parallel to the function array_make_fun_tsz:

val mat_10_10 =
  matrix_make_fun_tsz {int} (10, 10, lam (x, i, j) =<clo> x := 10 * i + j, sizeof<int>)

Matrix Subscripting The following two (template) functions matrix_get_elt_at and matrix_set_elt_at are for accessing and updating a persistent matrix, respectively:

fun{a:t@ype} matrix_get_elt_at {m,n:nat} (A: matrix (a,m,n), i: natLt m, j:natLt n): <!ref> a
fun{a:t@ype} matrix_set_elt_at {m,n:nat} (A: matrix (a,m,n), i: natLt m, j:natLt n, x: a): <!ref> void

The symbol [] is overloaded with both matrix_get_elt_at and matrix_set_elt_at:

overload [] with matrix_get_elt_at
overload [] with matrix_set_elt_at

As an example, the following code implements a (template) function that transposes a given square matrix in-situ.

fn{a:t@ype} matrix_transpose {n:nat} (M: matrix (a, n, n)): void = let
  val n = matrix_size_row M // n: int n

  // [fn*] indicates a request for tail-call optimization
  fn* loop1 {i:nat | i <= n} .< n-i+1, 0 >. (i: int i): void =
    if i < n then loop2 (i, 0) else ()
  and loop2 {i,j:nat | i < n; j <= i} .< n-i, i-j+1 >. (i: int i, j: int j): void =
    if j < i then
      let val x = M[i,j] in M[i,j] := M[j,i]; M[j,i] := x; loop2 (i, j+1) end
    else begin
      loop1 (i+1)
    end
in
  loop1 0
end // end of [matrix_transpose]

There are also library (template) functions foreach_matrix and iforeach_matrix for iteration over persisten matrices, which are given the following interfaces:

fun{a:t@ype} foreach_matrix {f:eff} {m,n:nat}
  (f: a -<f> void, M: matrix (a, m, n)):<f,!ref> void

fun{a:t@ype} iforeach_matrix {f:eff} {m,n:nat}
  (f: (natLt m, natLt n, a) -<f> void, M: matrix (a, m, n)):<f,!ref> void

For instance, the previous function matrix_transpose can be implemented as follows by calling iforeach_matrix:

fn{a:t@ype} matrix_transpose {n:nat} (M: matrix (a, n, n)): void =
  iforeach_matrix (lam (i,j, x) =<!ref> if i > j then (M[i,j] := M[j,i]; M[j,i] := x), M)

The code used for illustration is available here.