Persistent Arrays and Matrices

Though arrays are widely used in practice, there are many difficult issues involving arrays that seem to have not been adequately addressed in type theory. 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 persistent arrays can be found in the file 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. Internally, a value of the type array(VT, I) is just a pointer to a piece of consecutive memory holding I elements of the type VT. Note that there is no size information directly attached to such an array, that is, no function of the following type is available:

fun{a:viewt@ype} array_size {n:nat} (A: array (a, n)): int n

If the size of such an array is needed, it may be stored somewhere explicitly by the programmer.

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

val digits = array $arrsz{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 $arrsz{digit}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)

Array Subscripting The following two function templates 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: sizeLt n):<!ref> a
fun{a:t@ype} array_set_elt_at {n:nat} (A: array (a, n), i: sizeLt 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), sz: int n): void = loop (0) where {
  fun loop {i:nat | i <= n} .<n-i>. (i: int i):<cloptr1> void =
    if i < sz then
      let val x = A[i] in A[i] := x * x; loop (i+1) end
    else ()
} // 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.

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 often referred to as a square matrix.

The interfaces for various functions on matrices can be found in the file 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. Internally, a value of the type matrix(VT, I, J) is just a pointer to a piece of consecutive memory holding I*J elements of the type VT, where the elements are placed in the row-major format.

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

val mat_10_10 =
  matrix (10, 10) $arrsz {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
) // end of [val]

Matrix Subscripting The following two function templates 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: sizeLt m, n: int n, j: sizeLt n): <!ref> a
fun{a:t@ype} matrix_set_elt_at {m,n:nat} (A: matrix (a,m,n), i: sizeLt m, n: int n, j: sizeLt n, x: a): <!ref> void

Note that the number of columns in a matrix as well as the row and column indices are needed in order to perform matrix subscripting. As an example, the following code implements a function template that transposes a given square matrix in-situ:

fn{a:t@ype} matrix_transpose {n:nat}
  (A: matrix (a, n, n), n: int n): void = let
  fn get {i,j:nat | i < n; j < n}
   (A: matrix (a, n, n), i: int i, j: int j):<cloref1> a =
   matrix_get_elt_at__intsz (A, i, n, j)

  fn set {i,j:nat | i < n; j < n}
   (A: matrix (a, n, n), i: int i, j: int j, x: a):<cloref1> void =
   matrix_set_elt_at__intsz (A, i, n, j, x)

  overload [] with get; overload [] with set

  // [fn*] indicates a request for tail-call optimization
  fn* loop1 {i:nat | i <= n} .< n-i+1, 0 >.
    (i: int i):<cloptr1> void = begin
    if i < n then loop2 (i, 0) else ()
  end

  and loop2 {i,j:nat | i < n; j <= i} .< n-i, i-j+1 >.
    (i: int i, j: int j):<cloptr1> void = begin
    if j < i then
      let val x = A[i,j] in A[i,j] := A[j,i]; A[j,i] := x; loop2 (i, j+1) end
    else begin
      loop1 (i+1)
    end
  end // end of [loop2]
in
  loop1 0
end // end of [matrix_transpose]

fn{a:t@ype} matrix_transpose {n:nat}
  (M: matrix (a, n, n), n: size_t n): void = let
  prval pf = unit_v ()
  val () = matrix_iforeach_clo<a> {unit_v}
    (pf | M, !p_f, n, n) where { 
    var !p_f = @lam
      (pf: !unit_v | i: sizeLt n, j: sizeLt n, _: a): void =<clo,!ref>
      if i > j then let
        val x = M[i, n, j] in M[i, n, j] := M[j, n, i]; M[j, n, i] := x
      end // end of [if]
    // end of [var]
  } // end of [val]
  prval unit_v () = pf
in
  // empty
end // end of [matrix_transpose]

The code used for illustration is available here.