Datatypes

The feature of datatypes in ATS is directly adopted from ML. In addition to what is available in ML, we can also form in ATS dependent datatypes and guarded recursive datatypes (GRDTs), also known as generalized algebraic datatypes (GADTs). There is also a form of linear datatypes (dataviewtypes) available in ATS, which is to be explained elsewhere.

A Simple Datatype

In the first example given below, a datatype type intlst0 is declared to represent lists of integers and a function length_intlst0 for computing the length of a given list is implemented:

datatype intlst0 = // simple datatype
  | INTLST0nil // the first bar (|) is optional
  | INTLST0cons of (int, intlst0)

fun length_intlst0 (xs: intlst0): int =
  case+ xs of // [case+] demands exhaustive pattern matching
  // the bar (|) in the first clause is optional
  | INTLST0cons (_, xs) => 1 + length_intlst0 (xs)
  | INTLST0nil () => 0
// end of [length_intlst0]

Please note that any valid identifiers for variables can also be used as identifiers for constructors. The pattern for a constructor C with no arguments is C( ). If we write C instead of C( ), then C is assumed to be a variable pattern, which matches any value.

A Dependent Datatype

In ATS, we can form a dependent datatype intlst1 as follows to represent integer lists:

datatype intlst1 (int) = // dependent datatype
  | INTLST1nil (0) // the first bar (|) is optional
  | {n:nat} INTLST1cons (n+1) of (int, intlst1 n)
// end of [intlst1]

We may see intlst1 as a refinement of intlst0. Given an integer n, intlst1(n) is a type for integer lists of length n. The syntax for declaring intlst1 introduces two constructors of the following types:

INTLST1nil : intlst1 0
INTLST1cons : {n:nat} (int, intlst1 n) -> intlst (n+1)

So INTLST1nil is a list of length 0 and INTLST1cons constructs a list of length n+1 if given an integer and an integer list of length n.

The function for computing the length of a given integer list can now be implemented as follows:

fun length_intlst1 {n:nat} (xs: intlst1 n): int n =
  case+ xs of // the bar (|) in the first clause is optional
  // the bar (|) in the first clause is optional
  | INTLST1cons (_, xs) => 1 + length_intlst1 (xs)
  | INTLST1nil () => 0
// end of [length_intlst1]

Note that length_intlst1 is assigned the following type:

{n:nat} intlst1 n -> int n

which clearly indicates that the returned value of a call to length_intlst1 is the length of the argument of the call.

As another example, the following code implements the list subscripting function:

// the index is a natural number less than the size of the indexed length
fun nth_intlst1 {n,i:int | 0 <= i; i < n} (xs: intlst1 n, i: int i): int =
  // [val+] demands exhaustive pattern matching
  let val+ INTLST1cons (x, xs) = xs in
    if i > 0 then nth_intlst1 (xs, i-1) else x
  end // end of [let]
// end of [nth_intlst1]

Note that the pattern matching involved in the value declaration val+ INTLST1cons (x, xs) = xs is guaranteed to be exhaustive as n is positive. As a consequence, there is no tag checking in the C code generated from the compilation of nth_intlst. This simple example demonstrates that safety can actually enhance efficiency.

A Polymorphic Datatype

We can declare a datatype list as follows for representing polymorphic lists:

// [t@ype] is a sort for types of unrestricted size
datatype list (a:t@ype+, int) = // polymorphic datatype
  | nil (a, 0)
  | {n:nat} cons (a, n+1) of (a, list (a, n))

The syntax used for declaring list introduces two constructors of the following types:

nil : {a:t@ype} list (a, 0)
cons : {a:t@ype} {n:nat} (a, list (a, n)) -> list (a, n+1)

We use a:t@ype+ (instead of a:t@ype) to indicate that the type constructor list is covariant at this argument, that is, list (T1, n) is considered to be a subtype of list (T2, n) whenever T1 is a subtype of T2.

The function for appending two polymorphic lists can be implemented as follows:

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

This function definition is a template. It can be typechecked but cannot be compiled until the type variable a is instantiated with a type of known size. The feature of templates in ATS is to be explained elsewhere.

As another example, the following code implements a (template) function that zips together two given lists of the same length:

fun{a1,a2:t@ype}
zip_list {n:nat}
  (xs1: list (a1, n), xs2: list (a2, n)): list ('(a1, a2), n) =
  case+ (xs1, xs2) of
  | (cons (x1, xs1), cons (x2, xs2)) => cons ('(x1, x2), zip_list (xs1, xs2))
  | (nil (), nil ()) => nil ()
  | (_, _) =/=>> () // none of these cases can occur
// end of [zip_list]

Note that the last clause in the definition of zip_list is presented only for the purpose of illustration, and it can simply be omitted.

The code used for illustration is available here.