Persistent Lists


Lists are by far the most commonly used data structure in functional programming. We say that a data structure is persistent if it is heap-allocated and can only be freed by the GC. In contrast, a data structure is said to be linear if it is either stack-allocated or heap-allocated and can be freed by the user as well as by the GC.

The datatype for persistent lists in ATS is declared as follows:

datatype list (a:t@ype+, int) = // t@ype+: covariant
  | list_nil (a, 0)
  | {n:int | n >= 0} list_cons (a, n+1) of (a, list (a, n))
Given a type T and an integer I, the type list(T, I) is for lists of length I in which each element is of type T.

Let us first introduce some abbreviations for the list constructors:

#define nil list_nil
#define cons list_cons
#define :: list_cons
The following syntax creates a list consisting of 1, 2 and 3:
cons (1, cons (2, cons (3, nil ()))) // [nil ()] can be replaced with [nil]
This kind of syntax is a bit unwieldy if longer lists need to be handled, and some alternatives are given as follows:
'[1, 2, 3] // the first character is quote (')
$lst (1, 2, 3) // this is equivalent to '[1, 2, 3]
$lst {Nat} (1, 2, 3) // [Nat] is given as the type for the list elements
The interfaces for various functions on lists can be found in the file prelude/SATS/list.sats.

We now present some simple programs involving lists. The following code implements a function template that computes the length of a given list:

// This implementation is not tail-recursive
fun{a:t@ype} length {n:nat} (xs: list (a, n)): int n =
  case+ xs of _ :: xs => 1 + length xs | nil () => 0
This is a rather poor implementation as it is not tail-recursive. A better one, which is tail-recursive, is given as follows:
// This implementation is tail-recursive
fn{a:t@ype} length {n:nat} (xs: list (a, n)): int n = let
  fun loop {i,j:int} (xs: list (a, i), j: int j): int (i+j) =
    case+ xs of _ :: xs => loop (xs, j+1) | nil () => j
in
  loop (xs, 0)
end // end of [length]

The code used for illustration is available here.