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_consThe 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.