Introduction to Programming in ATS:
PrevChapter 10. Datatype RefinementNext

Sequentiality of Pattern Matching

In ATS, pattern matching is performed sequentially at run-time. In other words, a clause is selected only if a given value matches the pattern guard associated with this clause but the value fails to match the pattern associated with any clause ahead of it. Naturally, one may expect that the following implementation of list_zipwith also typechecks: 

fun{
a,b:t@ype
}{c:t@ype
} list_zipwith
  {n:nat}
(
  xs: list(a, n)
, ys: list(b, n)
, f: (a, b) -<cloref1> c
) : list(c, n) = (
//
case+ (xs, ys) of
| (
    list_cons(x, xs)
  , list_cons(y, ys)) =>
  (
    list_cons(f(x, y), list_zipwith<a,b><c>(xs, ys, f))
  )
| (_, _) => list_nil((*void*))
//
) (* end of [list_zipwith] *)

This, however, is not the case. In ATS, typechecking clauses is done nondeterministically (rather than sequentially). In this example, the second clause fails to typecheck as it is done without the assumption of the given pair (xs, ys) failing to match the pattern guard associated with the first clause. The second clause can be modified slightly as follows to pass typechecking: 

  | (_, _) =>> list_nil((*void*))

The use of the symbol =>> (in place of =>) indicates to the typechecker that this clause needs to be typechecked under the sequentiality assumption that the given value matching it does not match the pattern guards associated with any previous clauses. Therefore, when the modified second clause is typechecked, it can be assumed that the pair (xs, ys) matching the pattern (_, _) must match one of the following three patterns:

Given that xs and ys are of the same length, the typechecker can readily infer that (xs, ys) can only match the first of the above three patterns. After the last two patterns are ruled out, typechecking is essentially done as if the second clause was written as follows: 

  | (list_nil(), list_nil()) => list_nil((*void*))

One may be wondering why typechecking clauses is not required to be done sequentially by default. The simple reason is that this requirement, if fully enforced, can have a great negative impact on the efficiency of typechecking. Therefore, it is a reasonable design to provide the programmer with an explict means to occasionally make use of the sequentiality assumption needed for typechecking a particular clause.

PrevHomeNext
Example: Mergesort on Lists (Redux)UpExample: Functional Red-Black Trees