Previous Up Next

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:
, 0) = ⊥          I(∅, 0) = ().
More generally, one can observe that I(∅, n) is a vector consisting of n wildcards.
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(ck,P), ak + n − 1), for all ck taken from Σ.

    If all those computations return ⊥, then I(P,n) also is ⊥. Otherwise, if one of the calls I(S(ck,P), ak + n − 1) returns pattern vector (r1rak   p2pn), we can define I(P,n) = (ck(r1, … , rakp2pn). Of course, in practice, we stop performing recursive calls as soon as one such call is discovered. As there can be others ck such that I(S(ck,P),ak+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 (p2pn), and the result of I(P, n) depends on whether Σ is empty or not. If Σ is empty, then we define I(P, n) = (_ p2pn). If Σ is not empty, then we define I(P,n) = (c(_, … , _) p2pn), where c is a constructor from the signature of the ck’s without being a ck. If the the signature of the ck’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).

I(∅, 0)=()By base-2.
One 1

, 1)
=(Nil|Cons (_, _))By induction-2, Σ = { One }.

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.

Previous Up Next