# 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:

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:

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:

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:

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:

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.