Introduction to Programming in ATS:
<<< PreviousModularityNext >>>

Abstract Types

The name abstract type refers to a type such that values of the type are represented in a way that is completely hidden from users of the type. This form of information-hiding attempts to ensure that changes to the implementation of an abstract type cannot introduce type-errors into well-typed code that makes use of the abstract type. In ATS as well as in many other programming languages, abstract types play a pivotal role in support of modular programming. I will present as follows a concrete example to illustrate a typical use of abstract types in practice.

Suppose that we are to implement a package to provide various funtionalities on finite sets of integers. We first declare an abstract type intset as follows for values representing finite sets of integers: 

abstype intset // a boxed abstract type

The keyword abstype indicates that the declared abstract type intset is boxed, that is, the size of intset is the same as a pointer. There is a related keyword abst@ype for introducing unboxed abstract types, which will be explained elsewhere. We next present an interface for each function or value that we want to implement in the package: 

// empty set
val intset_empty : intset

// singleton set of [x]
fun intset_make_sing (x: int): intset

// turning a list into a set
fun intset_make_list (xs: list0 int): intset

// turning a set into a list
fun intset_listize (xs: intset): list0 (int)

// membership test
fun intset_ismem (xs: intset, x: int): bool

// computing the size of [xs]
fun intset_size (xs: intset): size_t

// adding [x] into [xs]
fun intset_add (xs: intset, x: int): intset

// deleting [x] from [xs]
fun intset_del (xs: intset, x: int): intset

// union of [xs1] and [xs2]
fun intset_union (xs1: intset, xs2: intset): intset

// intersection of [xs1] and [xs2]
fun intset_inter (xs1: intset, xs2: intset): intset

// difference between [xs1] and [xs2]
fun intset_differ (xs1: intset, xs2: intset): intset

Let us now suppose that the declaration for intset and the above interfaces are all stored in a file named intset.sats (or any other legal name for a static file).

Usually, a realistic implementation for finite sets is based on some kind of balanced trees (e.g., AVL trees, red-black trees). For the purpose of illustration, we give an implementation in which finite sets of integers are represented as ordered lists of integers. This implementation is contained in a file named intset.dats, which is available on-line. In order to construct values of an abstract type, we need to concretize it temporarily by using the following form of declaration: 

assume intset = list0 (int)

where assume is a keyword. This assume-declaration equates intset with the type list0 (int) and this equation is valid until the end of the scope in which it is introduced. As the assume-declaration is at the toplevel in intset.dats, the assumption that intset equals list0 (int) is valid until the end of the file. There is a global restriction in ATS that allows each abstract type to be concretized by an assume-declaration at most once. More specifically, if an abstract type is concretized in two files foo1.dats and foo2.dats, then these two files cannot be used together to generate an executable. The rest of implementation in intset is all standard. For instance, the union operation on two given sets of integers is implemented as follows: 

implement
intset_union (xs1, xs2) =
  case+ (xs1, xs2) of
  | (list0_cons (x1, xs11), list0_cons (x2, xs21)) =>
      if x1 < x2 then
        list0_cons (x1, intset_union (xs11, xs2))
      else if x1 > x2 then
        list0_cons (x2, intset_union (xs1, xs21))
      else list0_cons (x1, intset_union (xs11, xs21))
  | (list0_nil (), _) => xs2
  | (_, list0_nil ()) => xs1
// end of [intset_union]

There is also some testing code available on-line that makes use of some functions declared in intset.sats. Often testing code as such is constructed immediately after the interfaces for various functions and values in a package are declared. This allows these interfaces to be tried before they are actually implemented so that potential flaws can be exposed in a timely fashion.

<<< PreviousHomeNext >>>
Generic Template ImplementationUpExample: A Package for Rationals