Introduction to Programming in ATS:
PrevChapter 4. DatatypesNext

Exhaustiveness of Pattern-Matching

Given a type T and a set of patterns, if for any given value of the type T there is always at least one pattern in the set such that the value matches the pattern, then pattern-matching values of the type T against the set of patterns is exhaustive. Given a case-expression of the form (case exp0 of clseq), where exp0 is assumed to be of some type T, if pattern-matching values of the type T against the guards of the matching clauses in clseq is exhaustive, then the case-expression is said to be pattern-matching-exhaustive.

The following code implements a function that finds the last character in a non-empty character list: 

fun
charlst_last
  (cs: charlst): char =
(
  case cs of
  | charlst_cons (c, charlst_nil ()) => c
  | charlst_cons (_, cs1) => charlst_last (cs1)
)
// end of [charlst_last]

The body of charlst_last is a case-expression, which is not pattern-matching-exhaustive: If cs is bound to the value charlst_nil(), that is, the empty character list, than none of the matching clauses in the case-expression can be chosen. When the code is typechecked by atsopt, a warning message is issued to indicate the case-expression being non-pattern-matching-exhaustive. If the programmer wants an error message instead, the keyword case should be replaced with case+. If the programmer wants to suppress the warning message, the keyword case should be replaced with case-. I myself mostly use case+ when coding in ATS.

The function charlst_last can also be implemented as follows: 

fun
charlst_last
  (cs: charlst): char =
(
  case cs of
  | charlst_cons (c, cs1) =>
    (
      case+ cs1 of
      | charlst_nil () => c | charlst_cons _ => charlst_last (cs1)
    ) // end of [charlst_cons]
) // end of [charlst_last]

In this implementation, the outer case-expression is not pattern-matching-exhaustive while the inner one is. Note that the pattern charlst_cons _ is just a shorthand for charlst_cons(_, _). In general, a pattern of the form C _, where C is a constructor (associated with some datatype), can be matched by any value that is constructed by applying C to some values. For instance, the pattern charlst_nil() can also be written as charlst_nil _.

Suppose we have a case-expression containing only one matching clause, that is, the case-expression is of the form [case exp0 of pat => exp]. Then we can also write this case-expression as a let-expression: (let val pat = exp0 in exp end). For instance, we give another implementation of the function charlst_last as follows: 

fun
charlst_last
  (cs: charlst): char = let
  val charlst_cons (c, cs1) = cs in case+ cs1 of
  | charlst_nil () => c | charlst_cons _ => charlst_last (cs1)
end // end of [charlst_last]

When this implementation is typechecked by atsopt, a warning message is issued to indicate the val-declaration being non-pattern-matching-exhaustive. If the programmer wants an error message instead, the keyword val should be replaced with val+. If the programmer wants to suppress the warning message, the keyword val should be replaced with val-.

As values formed by the constructors charlst_nil and charlst_cons are assigned the same type charlst, it is impossible to rely on typechecking to prevent the function charlst_last from being applied to an empty character list. This is a serious limitation. With dependent types, which allow data to be described much more precisely, we can ensure at the level of types that a function finding the last element of a list can only be applied to a non-empty list.

PrevHomeNext
Recursively Defined DatatypesUpExample: Binary Search Tree