A functional list is just a singly-linked list that is immutable after its construction. The following datatype declaration introduces a type list for functional lists:

// datatype list(a:t@ype, int) = | list_nil(a, 0) of () | {n:nat} list_cons(a, n+1) of (a, list(a, n)) //

There are various functions in ATSLIB for list construction. In practice, a list is usually built by making direct use of the constructors list_nil and list_cons. For instance, the following function fromto builds a list of integers between two given ones:

// fun fromto {m,n:int | m <= n} ( m: int(m), n: int(n) ) : list(int, n-m) = if m < n then list_cons(m, fromto(m+1, n)) else list_nil() //

// fun {a:t@ype} list_length {n:nat} ( xs: list(a, n) ) : int(n) = let // fun loop {i,j:nat} ( xs: list(a, i), j: int(j) ) : int(i+j) = ( case+ xs of | list_nil () => j | list_cons (_, xs) => loop(xs, j+1) ) // in loop (xs, 0) end // end of [list_length] //

// fun {a,b:t@ype} list_foldleft {n:nat} ( f: (a, b) -> a, ini: a, xs: list(b, n) ) : a = if iseqz(xs) then ini else list_foldleft(f, f(ini, xs.head()), xs.tail()) // end of [if] //

// fun {a,b:t@ype} list_foldright {n:nat} ( f: (a, b) -> b, xs: list(a, n), snk: b ) : b = if iseqz(xs) then snk else f(xs.head(), list_foldright(f, xs.tail(), snk)) // end of [if] //

As an application of list_foldleft, the following code implements a function for reversing a given list:

fun {a:t@ype} list_reverse ( xs: List0(a) ) : List0(a) = ( list_foldleft<List0(a),a> (lam (xs, x) => list_cons(x, xs), list_nil, xs) )

fun {a:t@ype} list_reverse {n:nat} ( xs: list(a, n) ) : list(a, n) = let // fun loop{i,j:nat} ( xs: list(a, i), ys: list(a, j) ) : list(a, i+j) = case+ xs of | list_nil () => ys | list_cons (x, xs) => loop (xs, list_cons (x, ys)) // in loop (xs, list_nil) end // end of [list_reverse]

As an application of list_foldright, the following code implements a function for concatenating two given lists:

// fun {a:t@ype} list_append ( xs: List0(a), ys: List0(a) ) : List0(a) = list_foldright<a, List0(a)>(lam (x, xs) => list_cons(x, xs), ys, xs) //

// fun {a:t@ype} list_append {m,n:nat} ( xs: list(a,m), ys: list(a,n) ) : list(a,m+n) = ( case+ xs of | list_nil () => ys | list_cons (x, xs) => list_cons (x, list_append (xs, ys)) ) //

One may think of a functional list as a representation for the finite mapping that maps each natural number i less than the length of the list to element i in the list. The following function list_get_at is for accessing a list element at a given position:

// fun {a:t@ype} list_get_at {n:nat} ( xs: list(a, n), i: natLt(n) ) : a = if i > 0 then list_get_at(xs.tail(), i-1) else xs.head() //

There is no destructive update on a functional list as it is immutable. The following function list_set_at can be called to construct a list that differs from a given one only at a given position:

// fun {a:t@ype} list_set_at {n:nat} ( xs: list(a, n), i: natLt(n), x0: a ) : list(a, n) = if i > 0 then list_cons(xs.head(), list_set_at(xs.tail(), i-1, x0)) else list_cons(x0, xs.tail()) // end of [if] //

Functional lists are by far the most widely used data structure in functional programming. However, one should not attempt to use a functional list like an array as doing so is inefficient both time-wise and memory-wise.

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