6  Specializing U for the useless clause problem

At first sight, it seems that plain algorithm U suffices in flagging useless clauses. Indeed, one hardly sees what additional, concise and useful, information could be given to programmers, whose expected reaction is to suppress the useless clause before recompiling. However or-patterns introduce their specific anomaly, which is related to the useless clause anomaly but does not reduce to it.

6.1  Useless clause is (almost) enough

Let us assume that we write a function to detect lists of type mylist (Section 2) whose first element is 1.

let f = function
| One x | Cons (x,_) -> x=1
| Nil | One _ | Cons (_,_) -> false

Intuitively, something is wrong: the last pattern looks too complicated. Indeed, the following code is more concise and equivalent.

let f = function
| One x | Cons (x,_) -> x=1
| Nil  -> false

Unfortunately, algorithm U silently accepts the first, “bad”, code. A good compiler should suggest that we might replace this bad code by the second, “good”, code.

In fact, algorithm U already does such a suggestion in the case of the following, “bad”, code, where the or-pattern is expanded.

let f = function
| One x | Cons (x,_) -> x=1
| Nil -> false
| One _ -> false
| Cons (_,_) -> false

Here, the compiler can tell us that the last two clauses are useless and we normally react by deleting them.

The discussion shows what is wrong with our example.

let f = function
| One x | Cons (x,_) -> x=1
| Nil | One _ | Cons (_,_) -> false

Clause Nil | One _ | Cons (_,_) -> false is useful because of pattern Nil. However, patterns One _ and Cons (_,_) are useless, since they can be deleted without altering f behavior. Moreover, a more positive definition of useless patterns is easily built upon the standard notion of useless clause by expanding or-patterns.

On the practical side, the Objective Caml compiler will here flag two useless patterns (and no useless clause):

let f = function
| One x | Cons (x,_) -> x=1
| Nil | One _ | Cons (_,_) -> false
Warning: this pattern is unused.
Warning: this pattern is unused.

6.2  Expansion of or-patterns

Because there can be many or-patterns, it is our interest to consider the expansion of exactly one or-pattern amongst many, so as to avoid producing code of exponential size. Consider function f below.

let f = function
| (1|2), (3|4), (5|6), …, (2k−1|2k) -> true
| _ -> false

To check the arguments of or-pattern (2k-1|2k), one expansion suffices.

let f = function
| (1|2), (3|4), (5|6), …, 2k−1 -> true
| (1|2), (3|4), (5|6), …, 2k   -> true
| _ -> false

And we can safely assert that patterns 2k−1 and 2k are useful by using known algorithm U, which does not exhibit exponential behavior here, provided that we compute disjunctions sequentially.

Expansion considers that, in or-pattern (p₁∣p₂), the left alternative p₁ has a higher priority than the right alternative p₂. This left-to-right bias allows a clear decision in the following boundary examples.

let f1 = function (1|_) -> true
and f2 = function (_|1) -> true
and f3 = function (1|1) -> true
and f4 = function (_|_) -> true

Expansion shows in what sense the right alternative of or-patterns is useful for f1 and useless in the remaining cases.

let f1 = function 1 -> true | _ -> true
and f2 = function _ -> true | 1 -> true
and f3 = function 1 -> true | 1 -> true
and f4 = function _ -> true | _ -> true

It may seem that giving good diagnostics forces us into reconsidering the definition of matching, which does not specify any order for trying to match or-pattern arguments (except for Haskell matching). In fact, for strict and Laville’s matching, we still can avoid specifying such an order: those definitions of pattern matching rely on what row is matched and not on how it is matched. However, in practice, for the sake of consistency between diagnostics and produced code (because of variables in or-patterns, execution can indeed reveal the matched alternative), the pattern matching compiler must take left-to-right order into account. This is easily done by the (strict) compiler of Le Fessant & Maranget [2001], which performs the expansion during pattern matching compilation, as by any compiler that features or-patterns by performing expansion before pattern matching compilation such as the SML/NJ compiler Appel and MacQueen [1991].

In the next section we describe a refinement of our algorithm U. This refinement aims at finding useless patterns and relies on the expansion of or-patterns. As a preliminary, we first note that expansion does not alter the output of algorithm U.

6.3  Rules for finding  useless patterns

It is certainly easier to first consider finding useless sub-patterns in the case of one or-pattern. Let P be a pattern matrix and let q^→ be a pattern vector, with q₁ being the or-pattern (r₁∣r₂). We wish to make a distinction between four possibilities, r₁ and r₂ are both useful, r₁ alone is useless, r₂ alone is useless, and both r₁ and r₂ are useless. More concretely, we design a new function U′(P,q^→ ) that returns a set of useless patterns (more exactly a set of useless pattern positions); that is, ∅ in the first case, {r₁} in the second case, {r₂} in the third case, and the distinguished set ⊤ in the fourth case.

From P and q^→ we define two expanded matchings

Where P @ q^→ ′ means adding row q^→ ′ to the bottom of matrix P. Then, we use U to compute the utility of both expansions and we write E_r1 and E_r2 for the results of these computations, logically encoding True by ∅ and False by ⊤ (E sets are sets of useless patterns). Then we combine E_r1 and E_r2 into E_q1 by the rules given in the left table of Figure 1.

---

Figure 1: Rules for combining the utility of or-pattern arguments

Er1 Er2 E(r1∣r2)  ∅ ∅ ∅  ⊤ ⊤ ⊤ ∅ ⊤ {r2} ⊤ ∅ {r1}

Er1 Er2 E(r1∣r2)  ∅ {r″,…} {r″,…}   {r′,…} ∅ {r′,…}   ⊤ {r″,…} {r1, r″,…}   {r′,…} ⊤ {r′,…, r2}   {r′,…} {r″,…} {r′,…, r″ …}

---

If r₁ and r₂ are themselves or-patterns, we would like to compute the utility of their arguments. To do so, U′ is called recursively. As a consequence, results other than ∅ and ⊤ are possible, when r₁ or r₂ are partially useless. We combine those new results as described in the second table of figure 1. Those extra rules complete the definition of pattern utility by expansion. As an example of such nested expansions, assume q₁ = ((r₁∣r₂)∣(r₃∣r₄)), the utility of r₄ is computed on the expansion consisting of matrixP @ ((r₁∣r₂) q₂⋯q_n) @ (r₃ q₂⋯q_n) and vector (r₄ q₂⋯q_n).

If several components of q^→ are or-patterns, we perform several independent expansions. For instance, let us assume that both q₁ and q₂ are or-patterns, we first proceed as described above, yielding one result E_q1. Then, we expand P and q^→ along their second column. Such an expansion can be defined easily as the composition of swapping the first two columns of P and q^→ and of the expansion introduced at the beginning of this section. This process yields another result E_q2.

We now need to combine the two results E_q1 and E_q2. Let us first consider the case when neither E_q1 nor E_q2 is ⊤. Then, those two results are (possibly empty) sets of useless patterns which we combine by set union, yielding the new result E_q1 ∪ E_q2. Let us now consider the case when E_q1 is ⊤. We assume, as we show later, that U′ is a conservative extension of U. That is U′(P, q^→ ) = ⊤, if and only if U(P, q^→ ) = False. Hence, E_q1 is ⊤ implies U(P, q^→ ) is False — i.e. q^→ is useless w.r.t. P. However, swapping two columns in P (and q^→) does not change U result (Lemma 3). Thus we also have E_q2 = ⊤. Conversely, if E_q2 is ⊤, then E_q1 necessarily is ⊤. Overall, whether expansion is performed along first or second column does not matter and the value of U′(P, q^→ ) should be ⊤. As a conclusion, we can define the combination of the utility of two disjoint or-patterns to be E_q1 ∪ E_q2, provided we adopt the extra definition ⊤ ∪ ⊤ = ⊤.

6.4  Computation of useless patterns

We now give a precise description of algorithm U′, as implemented in the Objective Caml compiler. The key idea is to use specialization (S(c, P) of Section 3.1) as a tool to discover or-patterns, before performing expansions as we did in the previous section. In practice, it is convenient to partition the columns of matrices and vectors into three subparts. We note those separations with “•”. That is, U′ takes such “dotted” matrices and vectors as arguments, written P • Q • R and p^→ • q^→ • r^→. Dotted matrices and vectors stand for triples of matrices and vectors. Later in this section, component q^→ will hold patterns that cannot contain or-patterns (i.e. wildcards), while all the components of r^→ will be or-patterns.

Dotted matrices and vectors define matchings in the ordinary sense, provided we erase the dots. More precisely we concatenate the subparts column-wise, written “&”, and consider U(P &Q & R, p^→ &q^→ &r^→). This new notation emphasizes the distinction between column-wise (or vertical) concatenation and row-wise (or horizontal) concatenation, which we write “@”.

Figure 2 defines some useful operations on dotted matrices. It is assumed that sub-matrix P has n columns (n > 0).

---

Figure 2: Operations on dotted matrices

(a) Specialization by constructor c row in P • Q • R row(s) in S(c,P • Q • R) c(t1, … , ta) ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi   t1 ⋯ ta p2i ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi _ ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi   _ ⋯ _ p2i ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi c′(t1, … , ta′) ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi      no row (t1∣t2) ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi   S ⎛ ⎜ ⎝ c, ⎛ ⎜ ⎝ t1 ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi  t2 ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi ⎞ ⎟ ⎠ ⎞ ⎟ ⎠

(b) Right shifts row in P • Q • R p1i ⋯ pni • q1i ⋯ qki • r1i ⋯ rzi ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ row in ⇒1(P • Q • R) p2i ⋯ pni • p1i q1i ⋯ qki • r1i ⋯ rzi   row in ⇒2(P • Q • R) p2i ⋯ pni • q1i ⋯ qki • p1i r1i ⋯ rzi

---

Informally, the first phase of algorithm U′ destructures the patterns of p^→ (using S from figure 2), looking for or-patterns. When or-patterns are found, the corresponding columns are transferred to the R subpart (using ⇒₂), ready for the expansion phase. Other columns are transferred to the Q subpart (using ⇒₁).

To compute the utility of clause number i in match … with p₁ -> e₁ | p₂ -> e₂ | … | p_m -> e_m, we perform the initial call

The typical call U′(P • Q • R, p^→ • q^→ • r^→) yields four situations. First three situations are the “search for or-patterns” phase and apply when P has columns.

1. If p₁ is a constructed pattern c(t₁, … , t_a), we define:

   U′(P • Q • R, (c(t1, … , ta) p2⋯pn) •  → q    •  → r   ) =           U′(S(c,P • Q • R), (t1⋯ ta   p2⋯ pn) •  → q    •  → r   ).

2. If p₁ is a wildcard, we transfer P’s first column into Q:

   U′(P • Q • R, (_ p2⋯pn) •

   → q

   •

   → r

   ) = U′(⇒1(P • Q • R),⇒1(

   → p

   •

   → q

   •

   → q

   )).

3. If p₁ is an or-pattern, we transfer P’s first column into R:

   U′(P • Q • R, ((t1∣t2) p2⋯pn) •

   → q

   •

   → r

   ) = U′(⇒2(P • Q • R),⇒2(

   → p

   •

   → q

   •

   → q

   )).

4. If P has no columns, there are two sub-cases depending on whether there are columns in R or not.
   1. If there were no or-patterns inside initial p^→ (r^→ = ()), we simply call U.

      U′(  • Q •  ,  •  → q    •  )   =   ∅ if U(Q,q→ ) = True U′(  • Q •  ,  •  → q    •  )   =   ⊤ if U(Q,q→ ) = False

   2. Otherwise R and r^→ possess z columns (z > 0) and all the components of r^→ are or-patterns. For a given column index j in r^→, we write r^→∖ j for the vector build from r^→ by suppressing component r_j. Similarly we write R∖ j for matrix R with column j erased. Finally [R]_j is the matrix R reduced to its column j. By hypothesis, r_j is an or-pattern (t₁∣t₂), and we perform the following two recursive calls.

      Et1   =   U′([R]j • (R∖ j)&Q •  , (t1) • ( → r   ∖ j)& → q    •  ) Et2   =   U′([R]j@(t1) • ((R∖ j)&Q)@(( → r   ∖ j)& → q    ) •  , (t2) • ( → r   ∖ j)& → q    •  )

      This formulas may be a bit complicated, they simply express the expansion of pattern r_j in a general setting (see the beginning of Section 6.3 for the particular case of exactly one or-pattern). One should notice that columns j′ of R and r^→ with j′ ≠ j get transfered to subpart Q and will not be expanded by further calls to U′. That is, expansion of one or-pattern is performed exactly once.

      Then, we combine E_t1 and E_t2 by the rules of Figure 1, yielding E_rj. Finally, we define:

      U′(  • Q • R,   •

      → q

      •

      → r

      ) =

      z ∪ j=1

      Erj.

We now prove that the new algorithm U′ is a conservative extension of the original algorithm U.

One can make the computation of U′ slightly more efficient by the following two techniques:

• At inductive step 2, if all patterns in the first column of P are wildcards, we delete this column in place of transferring it into Q. This will avoid repeated deletion by U.
• At inductive step 4-(b), if E_r1 is ⊤, we can immediately return ⊤.