Linear Lists

A linear list is essentially the same as a singly-linked list depicted by the dataview sllst_v. However, memory allocation and deallocation of list nodes that were not handled previously are handled this time. The following declaration introduces a dataviewtype list_vt, which forms a boxed type (of the sort viewtype) when applied to a type and an integer:

dataviewtype
list_vt (a:t@ype+, int) =
  | {n:nat}
    list_vt_cons (a, n+1) of (a, list_vt (a, n))
  | list_vt_nil (a, 0) of ()
// end of [list_vt]

Assume that a data constructor named foo is associated with a dataviewtype. Then there is a viewtype construtor of the name foo_unfold that takes n addresses to form a viewtype, where n is the arity of foo. For instance, there is a viewtype constructor list_vt_cons_unfold that takes two address L0 and L1 to form a viewtype list_vt_cons_unfold(L0, L1). This viewtype is for a list node created by a call to list_vt_cons such that the two arguments of list_vt_cons are located at L0 and L1 while the proofs for the at-views associated with L0 and L1 are put in the store for currently available proofs.

Given a type T and an integer I, the viewtype list_vt(T, I) is for linear lists of length I in which each element is assigned the type T. The following function template length computes the length of a given linear list:

fn{a:t@ype}
length {n:nat}
  (xs: !list_vt (a, n)): int n = let
  fun loop
    {i,j:nat | i+j==n} .<i>.
    (xs: !list_vt (a, i), j: int j): int (n) =
    case+ xs of
    | list_vt_cons (_, !p_xs1) => let
        val n = loop (!p_xs1, j+1); val () = fold@ (xs) in n
      end // end of [list_vt_cons]
    | list_vt_nil () => (fold@ (xs); j)
  // end of [loop]
in
  loop (xs, 0)
end // end of [length]

The interface of length indicates that length<T> returns an integer equal to I when applied to a list of the type list_vt(T, I), where T and I are a type and an integer, respectively. Note that the symbol ! in front of the type of a function argument indicates that the argument is call-by-value and it is preserved after a call to the function.

What is particularly interesting here is the way in which pattern matching on a value of a dataviewtype works. In the body of the inner function loop, the type of xs changes to list_vt_cons_unfold(L1, L2) for some addresses L1 and L2 when it matches the pattern list_vt_cons(_, !p_xs1), and p_xs1 is bound to a value of the type ptr(L2), and a proof of the at-view a@L1 and another proof of the at-view list_vt(a,n-1)@L2 are automatically put into the store for the currently availble proofs. Note that the symbol ! in front of the variable p_xs1 indicates that p_xs1 is bound to the pointer to the tail of the list referred to by xs1 (rather than the tail itself). In order to change the type of xs back to the type list_vt(a, n), we can apply fold@ to xs and this application implicitly consumes a proof of the at-view a@L1 and another proof of the at-view list_vt(a, n-1)@L2. Note that fold@ is a keyword in ATS, and an application of fold@ is treated as a proof and it is erased after typechecking. In the case where xs matches the pattern list_vt_nil(), the type of xs changes into list_vt_nil() while there is no proof added to the store for the currently available proofs, and the type of xs restores to list_vt(a, 0) when fold@ is applied to it.

Let us now see an example involving a linear list being freed manually:

fun{a:t@ype}
list_vt_free
  {n:nat} .<n>. (xs: list_vt (a, n)): void =
  case+ xs of
  | ~list_vt_cons (x, xs1) => list_vt_free (xs1) // [x] can be replaced with [_]
  | ~list_vt_nil () => ()
// end of [list_vt_free]

In the case where xs matches the pattern list_vt_cons(x, xs1), the names x and xs1 are bound to the head and the tail of the list referred to by xs, respectively, and the type of xs changes to list_vt_cons(L1, L2) for some addresses while a proof of the at-view a@L1 and another proof of the at-view list_vt(a, n-1)?!@L2 are put into the store for currently available proofs. Note that the symbol ?! indicates that the tail of the list, which is linear, is already taken out (as it is now referred by xs1). The special symbol ~ in front of the pattern list_vt_cons(x, xs1) indicates that the list node referred to by xs after xs matches the pattern is freed immediately.

It is also possible to use the special function free@ to explicitly free a node (also called a skeleton) left in a linear variable after the variable matches a pattern formed with a constructor associated with a dataviewtypes. For instance, the following code gives another implementation of list_vt_free:

fun{a:t@ype}
list_vt_free
  {n:nat} .<n>. (xs: list_vt (a, n)): void =
  case+ xs of
  | list_vt_cons (x, xs1) => (free@ {a}{0} (xs); list_vt_free (xs1))
  | list_vt_nil () => free@ {a} (xs)
// end of [list_vt_free]

As using free@ is a bit tricky in practice, I present more details as follows. First, let us note that the constructors list_vt_nil and list_vt_cons associated with list_vt are assigned the following types:

list_vt_nil : // one quantifier
  {a:t@ype} () -> list_vt (a, 0)
list_vt_cons : // two quantifiers
  {a:t@ype} {n:nat} (a, list_vt (a, n)) -> list_vt (a, n+1)

If free@ is applied to a node of the type list_vt_nil(), it needs one static argument. which is a type, to instantiate the quantifier in the type of the constructor list_vt_nil. If free@ is applied to a node of the type list_vt_cons_unfold(L1, L2), then it needs two static arguments, which are a type and an integer, to instantiate the two quantifiers in the type of the constructor list_vt_cons. In the case where the type of xs is list_vt_cons_unfold(L1, L2), typechecking the call free@ {a}{0} (xs) implicitly consumes a proof of the at-view a?@L1 and another proof of the at-view list_vt(a, 0)?. As there is no difference between list_vt(T, 0)? and list_vt(T, I)? for any T and I, the static argument 0 is supplied here. As a matter of fact, any natural number can be used in place of 0 as the second static argument of free@.

The next example I present is a function template that turns a linear list into its reverse:

fn{a:t@ype}
reverse {n:nat}
  (xs: list_vt (a, n)): list_vt (a, n) = let
  fun revapp
    {i,j:nat | i+j==n} .<i>.
    (xs: list_vt (a, i), ys: list_vt (a, j)): list_vt (a, n) =
    case+ xs of
    | list_vt_cons (_, !p_xs1) => let
        val xs1 = !p_xs1; val () = !p_xs1 := ys; val () = fold@ (xs)
      in
        revapp (xs1, xs)
      end // end of [list_vt_cons]
    | ~list_vt_nil () => ys
  // end of [revapp]
in
  revapp (xs, list_vt_nil)
end // end of [reverse]

This implementation of list reversal directly corresponds to the one presented previously that is based the dataview slseg_v (for singly-linked list segments). Comparing the two implementations, we can see that the above one is significantly simplified at the level of types. For instance, there is no explicit mentioning of pointers in the types assigned to reverse and revapp.

The following implementation of list append makes use of the feature of call-by-reference:

fn{a:t@ype}
append {m,n:nat} (
  xs: list_vt (a, m), ys: list_vt (a, n)
) : list_vt (a, m+n) = let
  fun loop {m,n:nat} .<m>. // [loop] is tail-recursive
    (xs: &list_vt (a, m) >> list_vt (a, m+n), ys: list_vt (a, n)): void =
    case+ xs of
    | list_vt_cons (_, !p_xs1) => let
        val () = loop (!p_xs1, ys) in fold@ (xs)
      end // end of [list_vt_cons]
    | ~list_vt_nil () => xs := ys // [xs] is a left-value
  // end of [loop]
  var xs: List_vt (a) = xs // creating a left-value for [xs]
  val () = loop (xs, ys)
in
  xs
end // end of [append]

As the call fold@(xs) in the body of the function loop is erased after typechecking, loop is a tail-recursive function. Therefore, append can be called on lists of any length without the concern of possible stack overflow. The type for the first argument of loop begins with the symbol &, which indicates that this argument is call-by-reference. The type of loop simply means that its first argument is changed from a list of length m into a list of length m+n while its second argument is consumed. Again, this implementation of list append essentially corresponds to the one presented previously that is based on the dataview slseg_v. Comparing these two, we can easily see that the above one is much simpler and cleaner, demonstrating concretely some advantage of dataviewtypes over dataviews.

Lastly in this section, I mention a closely related issue involving (functional) list construction and tail-recursion. Following is a typical implementation of functioal list concatenation:

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

Clearly, append1 is not tail-recursive, which means that it may cause stack overflow at run-time if its first argument is very long (e.g., containing 1 million elements). There is, however, a direct and type-safe way in ATS to implement functional list concatenation in a tail-recursive manner, thus eliminating the concern of potential stack overflow. For instance, the following implementation of append2 returns the concatenation of two given lists while being tail-recursive:

fun{a:t@ype}
append2 {m,n:nat} (
  xs: list (a, m)
, ys: list (a, n)
) : list (a, m+n) = let
  fun loop
    {m,n:nat} .<m>. (
    xs: list (a, m)
  , ys: list (a, n)
  , res: &(List a)? >> list (a, m+n)
  ) :<> void = begin case+ xs of
    | list_cons (x, xs) => let
        val () = (
          res := list_cons {a}{0} (x, ?) // a partially initialized list
        ) // end of [val]
        val+ list_cons (_, !p) = res // [p] points to the tail of the list
        val () = loop (xs, ys, !p)
      in
        fold@ res // this is a no-op at run-time
      end // end of [list_cons]
    | list_nil () => (res := ys)
  end // end of [loop]
  var res: List a // uninitialized variable
  val () = loop (xs, ys, res)
in
  res
end // end of [append2]

During typechecking, the expression list_cons {a}{0} (x, ?), is assigned the (linear) type list_cons(L1, L2) for some addresses L1 and L2 while a proof of the at-view a@L1 and another proof of the at-view list(a, 0)?@L2 are put into the store for the currently available proofs. Note that the special symbol ? here simply indicates that the tail of the newly constructed list is uninitialized. A partially initialized list of the type list_cons(L1, L2) is guaranteed to match the pattern list_cons(_, !p), yielding a bindng between p and the (possibly uninitialized) tail of the list. When fold@ is called on a variable of the type list_cons(L1, L2), it changes the type of the variable to list(T, N+1) by consuming a proof of the view T@L1 and another proof of the view list(T, N), where T and N are a type and an integer, respectively.

In summary, dataviewtypes can largely retain the convenience of pattern matching associated with datatypes while requiring no GC support at run-time. Compared to dataviews, dataviewtypes are less general. However, if a dataviewtype can be employed to solve a problem, then the solution is often significantly simpler and cleaner than an alternative dataview-based one.