5  Specializing U for exhaustiveness check

Programmers sometimes are quite upset in front of “non-exhaustive match” warnings. An example of a “non-matching value” helps a lot not only in convincing them that they indeed wrote a non-exhaustive match, but also in correcting their code.

Such an example (or counter-example) is best expressed as a pattern representing a set of non-matching instances. Then, programmers can add this “counter-example” at the end of their matching, hoping this will make it exhaustive. Consider an easy example.

let nilp = function [] -> true
Warning: this pattern-matching is not exhaustive.
Here is an example of a non-matching value:
_::_

The given pattern matching is not exhaustive and all instances of the pattern _::_ (a list cell) are non-matching. Here, one achieves exhaustive match by adding a clause with pattern _::_.

Examples of non-matching values are easily computed by a slight extension of algorithm U. Indeed, algorithm U shows that M(P, q^→ ) is not empty by implicitly computing a witness of that fact.

The new algorithm I takes a matrix P and an integer n as arguments, since I is used in a context where the pattern vector q^→ of Section 3.1 is a vector of n wildcards. Algorithm I normally returns a pattern vector p^→ of size n such that all the instances of p^→ are non-matching values. Or, if no such vector exists (i.e. if P is exhaustive), I returns the distinguished constant ⊥.

Base case

If n = 0, we define:

I(

⎛ ⎝

⎞ ⎠

, 0) = ⊥          I(∅, 0) = ().

More generally, one can observe that I(∅, n) is a vector consisting of n wildcards.

Induction

If n > 0, then let Σ be the set of constructors that appear at the root of the patterns (and of or-pattern alternatives) in the first column of P.

1. We first assume that Σ is a complete signature. Then, we should perform the recursive calls I(S(c_k,P), a_k + n − 1), for all c_k taken from Σ.

   If all those computations return ⊥, then I(P,n) also is ⊥. Otherwise, if one of the calls I(S(c_k,P), a_k + n − 1) returns pattern vector (r₁⋯ r_ak   p₂⋯ p_n), we can define I(P,n) = (c_k(r₁, … , r_ak) p₂⋯p_n). Of course, in practice, we stop performing recursive calls as soon as one such call is discovered. As there can be others c_k′ such that I(S(c_k′,P),a_k′+n−1) returns a pattern vector, algorithm I is non-deterministic.

2. If Σ is not a complete signature, we only perform the recursive call I(D(P), n−1) and we define I(P,n) = ⊥ when the recursive call returns ⊥. Otherwise, I(D(P), n−1) returns the vector (p₂⋯p_n), and the result of I(P, n) depends on whether Σ is empty or not. If Σ is empty, then we define I(P, n) = (_ p₂⋯p_n). If Σ is not empty, then we define I(P,n) = (c(_, … , _) p₂⋯p_n), where c is a constructor from the signature of the c_k’s without being a c_k. If the the signature of the c_k’s is finite and not too big, one can even use an or-pattern that includes all the extra constructors.

It should be clear that I(P, n) = ⊥, if and only if P is exhaustive. Otherwise, I(P, n) is some pattern vector p^→ and all the instances of p^→ are non-matching values.

A simple example will demonstrate algorithm I at work. Let us check the exhaustiveness of the following matching that acts on values of type mylist (Section 2).

match … with  One 1 -> ⋯

We thus compute I((One 1), 1).

One may think that algorithm I should make an additional effort to provide more non-matching values, by systematically computing recursive calls on specialized matrices when possible, and by returning a list of all pattern vectors returned by recursive calls. We can first observe that it is not possible in general to supply the users with all non-matching values, since the signature of integers is (potentially) infinite. Furthermore, we claim that supplying one of the non-matching patterns is enough. Correcting the source that triggers the warning is a programmer’s job, and we intentionally limit the task of the compiler to supplying a precise (and not too costly) warning, justified by a concrete example. In our example, the answer (Nil|Cons (_,_)) points out the most obvious forgotten pattern. Furthermore, if the programmers write a clause for the flagged pattern and recompile the corrected program, then the compiler will flag other non-matching patterns such as One 0. Hence, the whole information is available to programmers, if they want it.