A Tutorial on Programming Features in ATS:
Prev		Next

Chapter 17. Persistent Arrays-with-size

I use the name array-with-size to refer to a persistent array with attached size information. Given a viewtype VT, the type for an array-with-size that contains N values of viewtype VT is arrszref(VT, N). Essentially, such a value is a boxed pair of two components of types arrayref(VT, N) and size_t(N). The interfaces for various functions on persistent arrays-with-size can be found in prelude/SATS/arrayref.sats.

For creating an array-with-size, the following functions arrszref_make_arrpsz and arrszref_make_arrayref can be called:

fun{}
arrszref_make_arrpsz
  {a:vt0p}{n:int} (arrpsz(INV(a), n)): arrszref(a)
fun{}
arrszref_make_arrayref
  {a:vt0p}{n:int} (arrayref(a, n), size_t(n)): arrszref(a)
// end of [arrszref_make_arrayref]

As an example, the following code creates an array-with-size containing all the decimal digits:

val DIGITS =
  (arrszref)$arrpsz{int}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)

Note that arrszref is overloaded with arrszref_make_arrpsz.

For reading from and writing to an array-with-size, the function templates arrszref_get_at and arrszref_set_at can be used, respectively, which are assigned the following interfaces:

fun{a:t@ype}
arrszref_get_at (A: arrszref(a), i: size_t): (a)
fun{a:t@ype}
arrszref_set_at (A: arrszref(a), i: size_t, x: a): void

Given an array-with-size A, an index i and a value v, arrszref_get_at(A, i) and arrszref_set_at(A, i, v) can be written as A[i] and A[i] := v, respectively. Notice that array-bounds checking is performed at run-time whenever arrszref_get_at or arrszref_set_at is called, and the exception ArraySubscriptExn is raised in case of out-of-bounds array access being detected.

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

fun{a:t@ype}
arrszref_reverse
(
  A: arrszref(a)
) : void = let
//
val n = A.size()
val n2 = half (n)
//
fun loop
  (i: size_t): void = let
in
  if i < n2 then let
    val tmp = A[i]
    val ni = pred(n)-i
  in
    A[i] := A[ni]; A[ni] := tmp; loop (succ(i))
  end else () // end of [if]
end // end of [loop]
//
in
  loop (i2sz(0))
end // end of [arrszref_reverse]

Arrays-with-size can be a good choice over arrays in a prototype implementation as it is often more demanding to program with arrays. Also, for programmers who are yet to become familiar with dependent types, it is definitely easier to work with arrays-with-size than arrays. When programming in ATS, I often start out with arrays-with-size and then replace them with arrays when I can see clear benefits from doing so.

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