3  The useful clause problem

We express pattern matching anomalies in the matrix framework.

Useless clauses are sometimes called redundant. In our opinion, “useless” is more precise, since it conveys the semantical nature of the concept better.

Because we use the ML definition of pattern matching (Definition 2) we claim that the two definitions above express what is generally understood by “an exhaustive match” and “an useless clause”, However it is intuitively clear that the two questions are quite similar, and in fact they can be expressed using the following definition.

Our framework of two separate definitions 2 and 3 exposes that, as far as pattern matching anomalies are concerned, the matching predicate can be simplified. More precisely, it is important to notice that v^→ matches some row in P (Definition 2) is equivalent to P ≼ v^→ (Definition 3). In other words, the order of rows in P is irrelevant while computing U(P,q^→ ).

3.1  Solving the useful clause problem

In this section we compute U recursively. We proceed by first defining a recursive function U_rec and then showing U = U_rec. The definition of U_rec owes much to the traditional compilation of ML pattern matching to decision trees — Pettersson [1992] gives a modern presentation of this quite ancient compilation scheme.

Let thus P be a pattern matrix of size m × n and q^→  be a pattern vector of size n. Induction proceeds by decomposing P and q^→ along first column.

Base case

If there is no column (i.e. n=0), then the value of U_rec(P, ()) depends upon the number of rows m of matrix P.

1. If P has some rows (i.e. m > 0), we define U_rec(( ), ()) to be false.
2. If m is zero, then we define U_rec(∅,()) to be true. More generally, although not really necessary, we can define U_rec(∅,q^→ ) to be true for any vector q^→ of any size n.

Base cases are summarized as follows:

Urec(

⎛ ⎝

⎞ ⎠

, ()) = False          Urec(∅ ,

→ q

) = True.

Induction

If there are columns (n > 0), then there are three sub-cases depending upon the nature of pattern q₁.

1. Pattern q₁ is a constructed pattern, that is q₁ = c(r₁, … , r_a). From matrix P, we extract the new specialized matrix S(c,P). The new matrix S(c,P) is of width a+n−1 and its rows are defined from the rows of P, according to the first component of these rows.

   p1i S(c,P)   c(r1, … , ra) r1 ⋯ ra p2i ⋯ pni  c′(r1, … , ra′)   (c′ ≠ c) No row _ _ ⋯ _ p2i ⋯ pni (r1∣r2) S(c, ⎛ ⎜ ⎝ r1 p2i ⋯ pni r2 p2i ⋯ pni ⎞ ⎟ ⎠ )

   Notice that a given row p^→ i, may induce one, none or several rows in S(c, P). In the following, we note S(c, q^→ ) the application of S to a vector, when it yields a vector.

   S(c, (c(r1, … , ra) q2⋯qn)) = (r1⋯ ra   q2⋯ qn) S(c, (_ q2⋯qn)) = (     _⋯ _ ◥ ▼ ◤ a times    q2⋯ qn)

   We also consider specialization of value vectors when relevant, that is when v₁ = c(w₁, … , w_a).

   Finally, in the case where q₁ is c(r₁, … , r_a), we define:

   Urec(P,

   → q

   ) = Urec(S(c,P), S(c,

   → q

   )).

2. Pattern q₁ is a wildcard. Let Σ = {c₁, c₂, … , c_z} be the set of constructors that appear as root constructors of the patterns of P’s first column (and also as root constructors of their arguments when they are or-patterns). The computation of U_rec depends on whether set Σ is a complete signature or not. In the former case, any instance v^→ of q^→  necessarily possesses a first component whose root constructor belongs to Σ. In the latter case, it turns out that it suffices to examine those constructors that do not belong to Σ. Here, computing U_rec significantly departs from compilation to decision trees, which of course has to take all constructors into account.
   1. Set Σ constitutes a complete signature. Then we define:

      Urec(P,

      → q

      )  =

      z ∨ k=1

      Urec(S(ck,P),S(ck,

      → q

      )).

   2. Set Σ is not a complete signature. From P, we extract the new default matrix D(P) of width n−1.

      p1i D(P)   ck(t1, … , tak) No row _ p2i  ⋯  pni (r1∣r2) D( ⎛ ⎜ ⎝ r1 p2i  ⋯  pni r2 p2i  ⋯  pni ⎞ ⎟ ⎠ )

      Matrix D(P) is defined in all situations, whether Σ is a complete signature or not. However, D(P) is useful for computing U_rec only in the latter case. We define:

      Urec(P, (_ q2⋯qn)) = Urec(D(P), (q2⋯qn)).

      Observe that when Σ is empty, i.e. when the first column of P is made of wildcards and of or-patterns thereof, then Σ is not a complete signature. Thus the definition above also apply.
3. When pattern q₁ is an or-pattern (r₁∣r₂), we define:

   Urec(P,((r1∣r2) q2⋯qn)) = Urec(P,(r1 q2⋯qn)) ∨ Urec(P,(r2 q2⋯qn)).

We now establish a few “key” properties of matrix specialization (1 below) and of the default matrix (2 to 4 below). Basically, the key property of specialization expresses that matching by P and S(c, P) are equivalent for value vectors whose first component admits c as a root constructor; while the key properties of the default matrix express the equivalence of matching by P and D(P) in more detailed situations.

We could of course have formulated the key properties by reversing implications and by using ≼ in place of ⋠. However, we adopt the negated formulation, to match Definition 2. Nevertheless, we shall also consider (1) when P has exactly one row. In that case, for any value vector v^→ such that v₁ = c(w₁, … , w_a), we write more directly:

3.2  Detecting the anomalies

Since we know how to compute U, we can detect pattern matching anomalies. Given some expression match … with p₁ -> e₁ | p₂ -> e₂ | … | p_m -> e_m, exhaustiveness is checked by computing:

while the usefulness of clause number i is checked by computing: