Re: Pattern Matching

[Pierre Weis <Pierre.Weis@inria.fr>]

Hi,

> let assign heap id obj = 
>   List.map
>     ( function 
>         (id,{ vartype = vt; contents = v; 
>               constraints = c; dependencies = d }) -> 
>             (id,{ vartype = vt; contents = obj; 
>                   constraints = c; dependencies = d })
>       | r -> r )    (* 1 *)
>     heap;;
> 
> However the compiler tells me that line marked (* 1 *) is an unused case
> of the match expression. I thought that maybe the problem was that the
> inner id variables (the ones in the function passed to map) are
> identifier patterns therefor they are different from the parameter
> of the assign function.

That's true: variables introduced by patterns are always ``new'' ones,
in the sense that these variables binds new parts of values that are
not related to previous names.

> So I tried to fix it like this:
> 
> let assign heap id obj = 
>   List.map
>     ( function 
>         (name,{ vartype = vt; contents = v; 
>                 constraints = c; dependencies = d }) 
>           when name = id -> 
>             (name,{ vartype = vt; contents = obj; 
>                     constraints = c; dependencies = d })
>       | (name,_) as r when name <> id -> r )
>     heap;;
> 
> And now I get the warning "this pattern-matching is not exhaustive".

Your first pattern is now correct, since you use an explicit equality
test in the ``when'' part of the clause (also called the guard of the
clause). The compiler's warning for the second pattern is also normal,
although it may appear a bit strange at first glance, since your
pattern matching is in fact exhaustive. You may get a better program
by removing the second guarded clause, and using the clause
``| r -> r'' which is equivalent; then, your pattern matching is
properly handled by the compiler that emits no warning no more.

This problem of spurious warnings is that the proof of exhaustivity of
the original guarded pattern matching is far beyond the scope of a
compiler, since it involves to prove that a boolean formula is not
refutable: your pattern matching was exhaustive not only because the
patterns were exhaustive (which is a syntactic condition that can be
checked by the compiler), but also because the boolean conditions of
the when parts were exhaustive, in the sens that the second condition
``name <> id'' were the negation of the first one ``name = id''. This
second part of the proof is much more difficult to tackle, since the
expressions involved in the guards can be arbitrarily complex
expressions e1 and e2, and you get to prove that e1 is equivalent to
(not e2).

Thus, given some guarded clauses
     | pat when condition ->
the compiler performs the ``exhaustive match'' detection as if the
condition can evaluate to false, thus assuming that the guarded clause
is not exhaustive. This is particularly evident if the condition is
reduced to the boolean true:

#function x when true -> 1;;
Toplevel input:
>function x when true -> 1;;
>^^^^^^^^^^^^^^^^^^^^^^^^^
Warning: this matching is not exhaustive.
- : 'a -> int = <fun>
#


Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis