A Tutorial on Programming Features in ATS:
PrevNext

Chapter 24. Linearly Typed Lists

A linearly typed list in ATS is also referred to as a linear list, which essentially corresponds to a singly-linked list in C. The following linear datatype declaration introduces a linear type list_vt for linear lists: 

//
datavtype
list_vt(a:vt@ype, int) =
| list_vt_nil(a, 0) of ()
| {n:nat}
  list_vt_cons(a, n+1) of (a, list_vt(a, n))
//

Note that the keyword datavtype can also be written as dataviewtype. Given a (possibly linear) type T and an integer N, the type list_vt(T,N) is for a list of length N that contains elements of type T. The interfaces for various functions on linear lists can be found in the SATS file prelude/SATS/list_vt.sats, which is automatically loaded by atsopt.

The following function list_vt_length shows a typical way of handling a linear list in a read-only situation: 

//
fun
{a:vt@ype}
list_vt_length
  (xs: !list_vt(a, n)): int(n) =
(
case+ xs of
| list_vt_nil() => 0
| list_vt_cons(x, xs2) => 1 + list_vt_length<a> (xs2)
)
//

When xs is matched with the pattern list_vt_nil(), the type of xs is list_vt(a, 0). When xs is matched with the pattern list_vt_cons(x, xs2), the type of xs is list_vt(a, N+1) for some natural number N and the types of x and xs2 are a and list_vt(a, N), respectively. Note that both x and xs2 are names for values, and their types are required to stay unchanged.

The following function list_vt_foreach shows a typical way of modifying elements stored in a linear list: 

//
fun
{a:vt@ype}
list_vt_foreach
(
  xs: !list_vt(a, n)
, fwork: (&(a) >> _) -<cloref1> void
) : void =
(
case+ xs of
| list_vt_nil() => ()
| @list_vt_cons(x, xs2) => (fwork(x); list_vt_foreach<a> (xs2, fwork); fold@(xs))
)
//

When xs is matched with the pattern @list_vt_cons(x,xs2), the type of xs is list_vt(a, N+1) for some natural number N and the types of x and xs2 are a and list_vt(a, N), respectively. Note that both x and xs2 are variables (that are a form of left-values). At the beginning of the body following the pattern @list_vt_cons(x,xs2), the type of xs is assumed to be list_vt_cons_unfold(L0, L1, L2), which is a viewtype for a list-node created by a call to list_vt_cons such that the node is located at L0 and the two arguments of list_vt_cons are located at L1 and L2 while the proofs for the at-views associated with L1 and L2 are put in the store for currently available proofs. Therefore, as left-values, x and xs2 have addresses L1 and L2, respectively, and the views of the proofs associated with L1 and L2 are a@L1 and list_vt_cons(a, N)@L2, respectively. The application fold@(xs) turns xs into a value of the type list_vt(a, N+1) while consuming the proofs associated with L1 and L2. Please notice that the type of xs can be different from the original one assigned to it after folding. For instance, the following example shows a case as such: 

//
fun
{a:vt@ype}
list_vt_append
  {m,n:nat}
(
  xs: list_vt(a, m), ys: list_vt(a, n)
) : list_vt(a, m+n) = let
//
fun
loop{m:nat}
(
  xs: &list_vt(a, m) >> list_vt(a, m+n), ys: list_vt(a, n)
) : void =
(
case+ xs of
| ~list_vt_nil() => (xs := ys)
| @list_vt_cons(x, xs2) => (loop(xs2, ys); fold@(xs))
)
//
in
  case+ xs of
  | ~list_vt_nil () => ys
  | @list_vt_cons (x, xs2) => (loop(xs2, ys); fold@(xs); xs)
end // end of [list_vt_append]
//

The meaning of the symbol ~ in front of a pattern is to be explained below. The implementation of list_vt_append exactly corresponds to the standard implementaion of concatenating two singly-linked lists in C: Let xs and ys be two given lists; if xs is empty, then ys is returned; otherwise, the last node in xs is located and ys is stored in the field of the node reserved for the next node.

The following function list_vt_free frees a given linear list containing non-linear elements: 

//
fun
{a:vt@ype}
list_vt_free
  {n:nat}
(
  xs: list_vt(a?, n)
) : void =
(
case+ xs of
| ~list_vt_nil() => ()
| ~list_vt_cons(x, xs2) => list_vt_free<a> (xs2)
)
//

When xs is matched with the pattern ~list_vt_nil(), the type of xs changes to a special one indicating that xs is no longer available for subsequent use. When xs is matched with the pattern ~list_vt_cons(x,xs2), the type of xs changes again to a special one indicating that xs is no longer available for subsequent use. In the latter case, the two values representing the head and tail of the list referred to as xs can be subsequently referred to as x and xs2, respectively. So what is really freed here is the memory for the first list-node in the list referred to as xs.

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

PrevHomeNext
Stream-Based Lazy EvaluationUpAdvanced Tutorial Topics