Introduction to Programming in ATS:
PrevNext

Chapter 15. Dataviewtypes as Linear Datatypes

Table of Contents
Linear Optional Values
Linear Lists
Example: Merge-Sort on Linear Lists
Example: Insertion Sort on Linear Lists
Example: Quick-Sort on Linear Lists
Linear Binary Search Trees
Transition from Datatypes to Dataviewtypes

A dataviewtype can be thought of as a linear version of datatype. To a large extent, it is a combination of a datatype and a dataview. This programming feature is primarily introduced into ATS for the purpose of providing in the setting of manual memory management the kind of convenience brought by pattern matching. In a situation where GC must be reduced or even completely eliminated, dataviewtypes can often be chosen as a replacement for datatypes. I now present in this chapter some commonly encountered dataviewtypes and their uses.

Linear Optional Values

When an optional value is created, the value is most likely to be used immediately and then discarded. If such a value is assigned a linear type, then the memory allocated for storing it can be efficiently reclaimed. The dataviewtype option_vt for linear optional values is declared as follows: 

//
datavtype
option_vt (a:t@ype+, bool) =
  | Some_vt (a, true) of a | None_vt (a, false) of ()
// end of [option_vt]
//
vtypedef Option_vt (a:t@ype) = [b:bool] option_vt(a, b)
//

Note that datavtype is just the short version of dataviewtype. The introduced dataviewtype option_vt is covariant in its first argument and there are two data constructors Some_vt and None_vt associated with it. In the following example, find_rightmost tries to find the rightmost element in a list that satisfies a given predicate: 

fun{a:t@ype}
find_rightmost
  {n:nat} .<n>.
(
  xs: list (a, n), P: (a) -<cloref1> bool
) : Option_vt (a) =
(
  case+ xs of
  | list_cons (x, xs) => let
      val opt = find_rightmost (xs, P)
    in
      case opt of
      | ~None_vt () => if P (x) then Some_vt (x) else None_vt ()
      | _ (*Some_vt*) => opt
    end // end of [list_cons]
  | list_nil () => None_vt ()
) (* end of [find_rightmost] *)

Note that the tilde symbol (~) in front of the pattern None_vt() indicates that the memory for the node that matches the pattern is freed before the body of the matched clause is evaluated. In this case, no memory is actually freed as None_vt is mapped to the null pointer. I will soon give more detailed explanation about freeing memory allocated for constructors associated with dataviewtypes.

As another example, the following function template list_optcons tries to construct a new list with its head element extracted from a given optional value: 

fn{a:t@ype}
list_optcons
  {b:bool}{n:nat}
(
  opt: option_vt (a, b), xs: list (a, n)
) : list (a, n+bool2int(b)) =
  case+ opt of
  | ~Some_vt (x) => list_cons (x, xs) | ~None_vt () => xs
// end of [list_optcons]

The symbol bool2int stands for a built-in static function in ATS that maps true and false to 1 and 0, respectively. What is special here is that the first argument of list_optcons, which is linear, is consumed after a call to list_optcons returns and the memory it occupies is reclaimed.

PrevHomeNext
Proof Functions for View-ChangesUpLinear Lists