Persistent Arrays

A persistent array of size n is just n heap-allocated cells (or references) in a row. It is persistent in the sense that the memory allocated for the array cannot be freed manually. Instead, it can only be reclaimed through garbage collection (GC).

Given a viewtype VT, the type for arrays containing n values of viewtype VT is array(VT, n). Note that arrays in ATS are the same as those in C: There is no size information attached them. The interfaces for various functions on references can be found in prelude/SATS/array.sats.

There are various functions for array creation. For instance, the following two are commonly used:

fun{a:t@ype}
array_make_elt
  {n:nat} (asz: size_t n, elt: a):<> array (a, n)
// end of [array_make_elt]

fun{a:t@ype}
array_make_lst {n:nat}
  (asz: size_t n, xs: list (a, n)):<> array (a, n)
// end of [array_make_lst]

Applied to a size and an element, array_make_elt returns an array of the given size in which each cell is initialized with the given element. Applied to a size and a list of elements, array_make_lst returns an array of the given size in which each cell is initialized with the corresponding element in the given list.

For reading from and writing to an array, the function templates array_get_elt and array_set_elt can be used, respectively, which are assigned the following interfaces:

fun{a:t@ype}
array_get_elt_at {n:int}
  {i:nat | i < n} (A: array (a, n), i: size_t i):<!ref> a

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

Given an array A, an index i and a value v, array_get_elt_al(A, i) and array_set_elt_at(A, i, v) can be written as A[i] and A[i] := v, respectively.

As an example, the following function template reverses the content of a given array:

fun{a:t@ype}
array_reverse {n:nat} (
  A: array (a, n), n: size_t (n)
) : void = let
  fun loop {i: nat | i <= n} .<n-i>.
    (A: array (a, n), n: size_t n, i: size_t i): void =
    if i < n/2 then let
      val tmp = A[i]
    in
      A[i] := A[n-1-i]; A[n-1-i] := tmp; loop (A, n, i+1)
    end else () // end of [if]
  // end of [loop]
in
  loop (A, n, 0)
end // end of [array_reverse]

If the test i < n/2 is changed to i <= n/2, a type-error is to be reported. Why? The reason is that A[n-1-i] becomes out-of-bounds array subscripting in the case where n and i both equals zero. Given that it is very unlikely to encounter a case where an array of size 0 is involved, a bug like this, if not detected early, can be buried so scarily deep!

The careful reader may have already noticed that the sort t@ype is assigned to the template parameter a. In other words, the above implementation of array_reverse cannot handle a case where the values stored in a array are of a linear type. The reason for choosing the sort t@ype is that both array_get_elt_at and array_set_elt_at can only be applied an array containing values of a nonlinear type. In the following implementation, the template parameter is given the sort viewt@ype so that an array containing values of a linear type can be handled:

fun{a:viewt@ype}
array_reverse {n:nat} (
  A: array (a, n), n: size_t (n)
) : void = let
  fun loop {i: nat | i <= n} .<n-i>.
    (A: array (a, n), n: size_t n, i: size_t i): void =
    if i < n/2 then let
      val () = array_exch (A, i, n-1-i) in loop (A, n, i+1)
    end else () // end of [if]
  // end of [loop]
in
  loop (A, n, 0)
end // end of [array_reverse]

The interface for the function template array_exch is given below:

fun{a:viewt@ype}
array_exch {n:nat}
  (A: array (a, n), i: sizeLt n, j: sizeLt n):<!ref> void
// end of [array_exch]

Note that array_exch can not be implemented in terms of array_get_elt_at and array_set_elt_at (unless some form of type-unsafe coding is empolyed). The curious reader can find its type-safe implementation in prelude/DATS/array.dats, which is based on a corresponding operation for linear arrays.