Pattern Matching

The feature of pattern matching in ATS is adopted from ML. However, this feature becomes much more elaborated in the presence of dependent types as well as linear types. We present as follows several examples to illustrate some typical uses of pattern matching in ATS.

Let us first declare a polymorphic datatype list0 as follows for representing lists:

datatype list0 (a:t@ype) = nil0 (a) | cons0 (a) of (a, list0 a)

Notice that this is not a dependent datatype. Suppose we need to implement a function zip0 that should only zip together two lists of the same length. This may be done as follows:

fun{a1,a2:t@ype} // [zip0] is a template
zip0 (xs: list0 a1, ys: list0 a2): list0 '(a1, a2) =
  case+ (xs, ys) of // [case+] indicates the exhaustiveness of pattern matching
  | (cons0 (x, xs), cons0 (y, ys)) => cons0 ('(x, y), zip0 (xs, ys))
  | (nil0 (), nil0 ()) => nil0 ()

The problem with this implementation is that a pattern matching failure occurs if the function zip0 is mistakenly applied to two lists of unequal length, resulting in a run-time exception. In practice, a special exception is often declared as follows to handle the case of pattern matching failure, enabling more accurate run-time information to be reported.

exception ZipException

fun{a1,a2:t@ype} // [zip0] is a template
zip0 (xs: list0 a1, ys: list0 a2): list0 '(a1, a2) =
  case+ (xs, ys) of // [case+] indicates the exhaustiveness of pattern matching
  | (cons0 (x, xs), cons0 (y, ys)) => cons0 ('(x, y), zip0 (xs, ys))
  | (nil0 (), nil0 ()) => nil0 ()
  | (_, _) => $raise ZipException

We can also declare a polymorphic dependent datatype list1 as follows for representing lists:

datatype list1 (a:t@ype, int) =
  | nil1 (a, 0)
  | {n:nat} cons1 (a, n+1) of (a, list1 (a, n))

Given a type T and an integer I, the type list1(T, I) is for lists of length I in which each element is of type T. The function for zipping two lists of the same length can now be implemented as follows:

fun{a1,a2:t@ype} // [zip1] is a template
zip1 {n:nat} (xs: list1 (a1, n), ys: list1 (a2, n)): list1 ('(a1, a2), n) =
  case+ (xs, ys) of // [case+] indicates the exhaustiveness of pattern matching
  | (cons1 (x, xs), cons1 (y, ys)) => cons1 ('(x, y), zip1 (xs, ys))
  | (nil1 (), nil1 ()) => nil1 ()

Note that the typechecker can verify that pattern matching in this implementation is exhaustive.

Given that pattern matching in ATS is done sequentially, that is, from left to right in a given row and from top to bottom for all the clauses in a given case-expression, it is natural to expect that the following code gives an equivalent implementation of zip1:

fun{a1,a2:t@ype}
zip1 {n:nat} (xs: list1 (a1, n), ys: list1 (a2, n)): list1 ('(a1, a2), n) =
  case+ (xs, ys) of // [case+] indicates the exhaustiveness of pattern matching
  | (cons1 (x, xs), cons1 (y, ys)) => cons1 ('(x, y), zip1 (xs, ys))
  | (_, _) => nil1 ()

This, however, is not the case as typechecking in ATS does not assume the sequentiality of pattern matching. In this example, the second pattern matching clause is typechecked indepenent of the first one, resulting in a type error. In order to demand that the second clause be typechecked under the assumption that the first clause is not chosen at run-time, the following special syntax is needed:

    | (_, _) =>> nil1 ()

The special arrow =>> indicates that a clause formed with this arrow needs to be typechecked under the assumption that all of the previous clauses (in the same case-expression) are not chosen at run-time.

In the C code generated from compiling the function zip1, there are two tag checkes: they check whether the first and the second arguments of zip1 are empty. Clearly, only one tag check is necessary as both arguments are of the same length. We can modify the implementation of zip1 as follows so as to use only one check:


fun{a1,a2:t@ype} // only one tag check
zip1 {n:nat} (xs: list1 (a1, n), ys: list1 (a2, n))
  : list1 ('(a1, a2), n) = begin case+ xs of
  | cons1 (x, xs) => begin
      let val+ cons1 (y, ys) = ys in cons1 ('(x, y), zip1 (xs, ys)) end
    end
  | _ =>> nil1 ()
end // end of [zip1]

Note that the keyword val+ indicates that the patthern matching following it is exhaustive and thus needs no tag check. This simple example demonstrates in concrete terms that safety can enhance efficiency.

The code used for illustration is available here.