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 orpatterns 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 orpattern 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 orpatterns.
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 orpatterns
Because there can be many orpatterns, it is our interest to consider
the expansion of exactly one orpattern amongst many, so as to
avoid producing code of exponential size.
Consider function f below.
let f = function
 (12), (34), (56), …, (2k−12k) > true
 _ > false
To check the arguments of orpattern (2k12k), one
expansion suffices.
let f = function
 (12), (34), (56), …, 2k−1 > true
 (12), (34), (56), …, 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 orpattern (p_{1}∣p_{2}),
the left alternative p_{1} has a
higher priority than the right alternative p_{2}.
This lefttoright bias allows a clear decision
in the following boundary examples.
let f1 = function (1_) > true
and f2 = function (_1) > true
and f3 = function (11) > true
and f4 = function (__) > true
Expansion shows in what sense the right alternative of orpatterns 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 orpattern 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 orpatterns, execution can indeed reveal the
matched alternative), the pattern matching compiler must take
lefttoright 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
orpatterns 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 orpatterns.
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, ((r_{1}∣r_{2}) q_{2}⋯q_{n})) =
U(P, (r_{1} q_{2}⋯q_{n})) ∨
U(P@(r_{1} q_{2}⋯q_{n}), (r_{2} q_{2}⋯q_{n})).

Where
P@
p^{→} means matrix
P with row
p^{→} added at the bottom.
Proof:
For Haskell matching, the equality follows
from definitions — H((r_{1}∣r_{2}), v_{1}) = T, if and only if
H(r_{1}, v_{1}) = T or
H(r_{1}, v_{1}) = F ∧ H(r_{2}, v_{1}) = T.
□
6.3 Rules for finding useless patterns
It is certainly easier to first consider finding useless subpatterns
in the case of one orpattern. Let P be a pattern matrix and let
q^{→} be a pattern vector, with q_{1} being the orpattern
(r_{1}∣r_{2}). We wish to make a distinction between four
possibilities, r_{1} and r_{2} are both useful, r_{1} alone is
useless, r_{2} alone is useless, and both r_{1} and r_{2} 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_{1}} in the second case, {r_{2}}
in the third case, and the distinguished set ⊤ in the fourth
case.
From P and q^{→} we define two expanded matchings
P′ = P,   ′ = (r_{1} q_{2}⋯q_{n})
and
P″ = P @   ′,   ″ = (r_{2} q_{2}⋯q_{n}).

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
orpattern arguments 
E_{r1}  E_{r2}  E_{(r1∣r2)} 
∅  ∅  ∅ 
⊤  ⊤  ⊤ 
∅  ⊤  {r_{2}} 
⊤  ∅  {r_{1}} 

  E_{r1}  E_{r2}  E_{(r1∣r2)} 
∅  {r″,…}  {r″,…} 
{r′,…}  ∅  {r′,…} 
⊤  {r″,…}  {r_{1}, r″,…} 
{r′,…}  ⊤  {r′,…, r_{2}} 
{r′,…}  {r″,…}  {r′,…, r″ …} 


If r_{1} and r_{2} are themselves orpatterns, 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_{1} or r_{2} 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_{1} =
((r_{1}∣r_{2})∣(r_{3}∣r_{4})), the utility of r_{4} is computed
on the expansion consisting of matrixP @ ((r_{1}∣r_{2}) q_{2}⋯q_{n}) @ (r_{3} q_{2}⋯q_{n}) and
vector (r_{4} q_{2}⋯q_{n}).
If several components of q^{→} are
orpatterns, we perform several independent expansions.
For instance, let us assume that both q_{1} and q_{2}
are orpatterns, 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 orpatterns 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
orpatterns, 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 orpatterns
(i.e. wildcards), while all the components of r^{→} will be
orpatterns.
Dotted matrices and vectors
define matchings in the ordinary sense, provided we
erase the dots. More precisely we concatenate the subparts
columnwise, written “&”, and consider U(P &Q &
R, p^{→} &q^{→} &r^{→}). This new notation
emphasizes the distinction between columnwise (or vertical)
concatenation and rowwise (or horizontal) concatenation, which we
write “@”.
Figure 2 defines some useful operations
on dotted matrices. It is assumed that submatrix 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(t_{1}, … , t_{a})  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i}    t_{1}  ⋯  t_{a}   p_{2}^{i}  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i} 
_  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i}    _  ⋯  _   p_{2}^{i}  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i} 
c′(t_{1}, … , t_{a′})  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i}    no row 
(t_{1}∣t_{2})  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i}   
 S  ⎛
⎜
⎝  c,
 ⎛
⎜
⎝  t_{1}  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i} 
t_{2}  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i} 
 ⎞
⎟
⎠ 
 ⎞
⎟
⎠ 



(b) Right shifts 
row in P • Q • R 

p_{1}^{i}  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i}  
 ⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪ 
 row in ⇒_{1}(P • Q • R) 

p_{2}^{i}  ⋯  p_{n}^{i}  •  p_{1}^{i}   q_{1}^{i}  ⋯  q_{k}^{i}  •  r_{1}^{i}  ⋯  r_{z}^{i}  


row in ⇒_{2}(P • Q • R) 

p_{2}^{i}  ⋯  p_{n}^{i}  •  q_{1}^{i}  ⋯  q_{k}^{i}  •  p_{1}^{i}   r_{1}^{i}  ⋯  r_{z}^{i}  




Informally, the first phase of algorithm U′ destructures the patterns
of p^{→} (using S from figure 2), looking for
orpatterns.
When orpatterns 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 p_{1} > e_{1} 
p_{2} > e_{2}  …  p_{m} >
e_{m}, we perform the initial call
U′(
 ⎛
⎜
⎜
⎜
⎝   ⎞
⎟
⎟
⎟
⎠  • • ,
(p_{i}) • • ).

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

If p_{1} is a constructed pattern c(t_{1}, … , t_{a}),
we define:
U′(P • Q • R,
(c(t_{1}, … , t_{a}) p_{2}⋯p_{n}) •   •   ) = 

U′(S(c,P • Q • R),
(t_{1}⋯ t_{a} p_{2}⋯ p_{n}) •   •   ). 


 If p_{1} is a wildcard, we transfer P’s first column into Q:
U′(P • Q • R, (_ p_{2}⋯p_{n}) •   •   ) =
U′(⇒_{1}(P • Q • R),⇒_{1}(   •   •   )).

 If p_{1} is an orpattern, we transfer P’s first column into R:
U′(P • Q • R, ((t_{1}∣t_{2}) p_{2}⋯p_{n}) •   •   ) =
U′(⇒_{2}(P • Q • R),⇒_{2}(   •   •   )).

 If P has no columns, there are two subcases depending on whether
there are columns in R or not.

If there were no orpatterns inside initial p^{→} (r^{→} =
()), we simply call U.
  =   ∅  if U(Q,q^{→} ) = True 
  =   ⊤  if U(Q,q^{→} ) = False 

 Otherwise R and r^{→} possess z columns (z > 0) and
all the components of r^{→} are orpatterns.
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 orpattern (t_{1}∣t_{2}), and
we perform the following two recursive calls.
E_{t1}   =   U′([R]_{j} • (R∖ j)&Q • ,
(t_{1}) • (   ∖ j)&   • ) 

E_{t2}   =   U′([R]_{j}@(t_{1}) • ((R∖ j)&Q)@((   ∖ j)&   ) • ,
(t_{2}) • (   ∖ j)&   • ) 


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
orpattern).
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 orpattern 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, •   •   ) =
  E_{rj}.

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,   •   •   ) = ⊤
⇐⇒ U(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 r_{j} = (t_{1}∣t_{2}) as follows.
E_{t1} = U′(P′ • Q′ • , (t_{1}) •   ′ • ),
E_{t2} =
U′(P″ • Q″ • ,
(t_{2}) •   ′ • )

Where it should be clear that P″ is P′@(t_{1}) 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 (t_{1}) &q^{→} ′ added.
Let also s^{→} ′ be the vector (t_{1}∣t_{2}) &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,   ) = U(S′,   ′) = U(S′, (t_{1}) &   ′) ∨
U(S″, (t_{2}) &   ′).

By induction, we have the following two equivalences.
E_{t1} = ⊤ ⇐⇒ U(S′, (t_{1}) &   ′) = False
E_{t2} = ⊤ ⇐⇒ U(S″, (t_{2}) &   ′) = False

Then, since E_{(t1∣t2)} = ⊤ if and
only if E_{t1} = ⊤ and E_{t2} = ⊤, we have:
E_{rj} = ⊤ ⇐⇒ U(S,   ) = False.

And we can conclude, since U′( • Q • R,
• q^{→} • r^{→}) = E_{r1} ∪ ⋯ ∪ E_{rz}.
□
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 ⊤.