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:
The keyword abstype indicates that the declared abstract type intset is boxed, that is, the size of intset is the same as that of 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
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, I hereby 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:
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)) => let val sgn = compare (x1, x2) in case+ 0 of | _ when sgn < 0 => list0_cons{int}(x1, intset_union (xs11, xs2)) | _ when sgn > 0 => list0_cons{int}(x2, intset_union (xs1, xs21)) | _ (* sgn = 0 *) => list0_cons{int}(x1, intset_union (xs11, xs21)) // end of [case] end // end of [(cons, cons)] | (list0_nil (), _) => xs2 | (_, list0_nil ()) => xs1 ) (* end of [intset_union] *)