Previous Up Next

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 (p1p2), the left alternative p1 has a higher priority than the right alternative p2. 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.

Lemma 4 (Utility of expansion)   For all three definitions of pattern matching, we have:
U(P, ((r1r2q2qn)) = U(P, (r1 q2qn)) ∨ U(P@(r1 q2qn), (r2 q2qn)).
Where P@p means matrix P with row p added at the bottom.
Proof: For Haskell matching, the equality follows from definitions — H((r1r2), v1) = T, if and only if H(r1, v1) = T or H(r1, v1) = FH(r2, v1) = T. □

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 q1 being the or-pattern (r1r2). We wish to make a distinction between four possibilities, r1 and r2 are both useful, r1 alone is useless, r2 alone is useless, and both r1 and r2 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, {r1} in the second case, {r2} in the third case, and the distinguished set ⊤ in the fourth case.

From P and q we define two expanded matchings

P′ = P,   
q
 
 ′ = (r1 q2qn)   and   P″ = P @ 
q
 
 ′,   
q
 
 ″ = (r2 q2qn).

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 Er1 and Er2 for the results of these computations, logically encoding True by ∅ and False by ⊤ (E sets are sets of useless patterns). Then we combine Er1 and Er2 into Eq1 by the rules given in the left table of Figure 1.


Figure 1: Rules for combining the utility of or-pattern arguments
Er1Er2E(r1∣r2) 
∅ 
{r2}
{r1}
    
Er1Er2E(r1∣r2) 
{r″,…}{r″,…}  
{r′,…}{r′,…}  
{r″,…}{r1r″,…}  
{r′,…}{r′,…, r2}  
{r′,…}{r″,…}{r′,…, r″ …}

If r1 and r2 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 r1 or r2 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 q1 = ((r1r2)∣(r3r4)), the utility of r4 is computed on the expansion consisting of matrixP @ ((r1r2q2qn) @ (r3 q2qn) and vector (r4 q2qn).

If several components of q are or-patterns, we perform several independent expansions. For instance, let us assume that both q1 and q2 are or-patterns, we first proceed as described above, yielding one result Eq1. 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 Eq2.

We now need to combine the two results Eq1 and Eq2. Let us first consider the case when neither Eq1 nor Eq2 is ⊤. Then, those two results are (possibly empty) sets of useless patterns which we combine by set union, yielding the new result Eq1Eq2. Let us now consider the case when Eq1 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, Eq1 is ⊤ implies U(P, q ) is Falsei.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 Eq2 = ⊤. Conversely, if Eq2 is ⊤, then Eq1 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 Eq1Eq2, 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 PQR and pqr. 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 PQRrow(s) in S(c,PQR)
c(t1, … , ta)pniq1iqkir1irzi t1ta p2ipniq1iqkir1irzi
_pniq1iqkir1irzi __ p2ipniq1iqkir1irzi
c′(t1, … , ta)pniq1iqkir1irzi    no row
(t1t2)pniq1iqkir1irzi 
S

c,

t1pniq1iqkir1irzi 
t2pniq1iqkir1irzi




(b) Right shifts
row in PQR
p1ipniq1iqkir1irzi









row in ⇒1(PQR)
p2ipnip1i q1iqkir1irzi
 
row in ⇒2(PQR)
p2ipniq1iqkip1i r1irzi

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 ⇒2), ready for the expansion phase. Other columns are transferred to the Q subpart (using ⇒1).

To compute the utility of clause number i in match … with p1 -> e1 | p2 -> e2 | … | pm -> em, we perform the initial call

U′(



p1 
p2 
⋮ 
pi−1




•   •  , (pi) •   •  ).

The typical call U′(PQR, pqr) yields four situations. First three situations are the “search for or-patterns” phase and apply when P has columns.

  1. If p1 is a constructed pattern c(t1, … , ta), we define:
    U′(P • Q • R, (c(t1, … , tap2pn) • 
    q
     
     • 
    r
     
    ) = 
             U′(S(c,P • Q • R), (t1⋯ ta   p2⋯ pn) • 
    q
     
     • 
    r
     
    ).
  2. If p1 is a wildcard, we transfer P’s first column into Q:
    U′(P • Q • R, (_ p2pn) • 
    q
     
     • 
    r
     
    ) = U′(⇒1(P • Q • R),⇒1(
    p
     
     • 
    q
     
     • 
    q
     
    )).
  3. If p1 is an or-pattern, we transfer P’s first column into R:
    U′(P • Q • R, ((t1t2p2pn) • 
    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 rj for the vector build from r by suppressing component rj. Similarly we write Rj for matrix R with column j erased. Finally [R]j is the matrix R reduced to its column j. By hypothesis, rj is an or-pattern (t1t2), 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 rj 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 Et1 and Et2 by the rules of Figure 1, yielding Erj. 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.

Proposition 5   Let P be a pattern matrix and q be a pattern vector. Then, U′(P •   •  , p •   •  ) = ⊤ is equivalent to U(P, p) = False.
Proof: We prove the following stronger property.
U′(P • Q • R
p
 
 • 
q
 
 • 
r
 
) = ⊤  ⇐⇒ U(P &Q &R
p
 
 &
q
 
 &
r
 
) = False
Proof is by induction on the definition of U′. Most cases are obvious, case 4-(a) is the base case, inductive cases 2. and 3. follow from Lemma 3 on the irrelevance of column order, while inductive case 1. is like inductive case 1. in Proposition 2.

Case 4-(b) (P is empty, R is not empty) is the most interesting. We first consider one expansion. In order to simplify notations a bit, we define S = Q &R and s = q &r. Furthermore, we express the expansion of rj = (t1t2) as follows.

Et1 = U′(P′ • Q′ •  , (t1) • 
q
 
 ′ •  ),      Et2 = U′(P″ • Q″ •  , (t2) • 
q
 
 ′ •  )

Where it should be clear that P″ is P′@(t1) and Q″ is Q′ @ q ′. We further define S′ to be P′ &Q′ and S″ to be P″ &Q″. Notice that S″ is S′ with the row (t1) &q ′ added. Let also s ′ be the vector (t1t2) &q ′. Matrix S′ and vector s ′ are the images of S and s by the same permutation of columns. By lemmas 3 and 4, we have:

U(S,
s
 
 ) = U(S′, 
s
 
 ′) = U(S′, (t1) &
q
 
 ′) ∨ U(S″, (t2) &
q
 
 ′).

By induction, we have the following two equivalences.

Et1 = ⊤  ⇐⇒ U(S′, (t1) &
q
 
 ′) = False      Et2 = ⊤  ⇐⇒ U(S″, (t2) &
q
 
 ′) = False

Then, since E(t1∣t2) = ⊤ if and only if Et1 = ⊤ and Et2 = ⊤, we have:

Erj = ⊤  ⇐⇒ U(S
s
 
 ) = False.

And we can conclude, since U′(  • QR,   • qr) = Er1 ∪ ⋯ ∪ Erz. □

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


Previous Up Next