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 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]
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]
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.