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]

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

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]