Pattern Matching

Pattern Matching

[Ernesto Posse]

Hello everyone.

I have a question about pattern matching. I need a function which 
binds an identifier to a value in certain data structure (which is
called "heap" here). This is actually a (string * record) list. It is
not suppose to be a mutable data structure, so the binding just creates
a
new list copying the same values as the old one with the exception of
the
record to be changed. For this purpose I am using List.map (I am using
O'Caml 1.01 for Windows 95):

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. 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".

Can anyone tell me what is wrong with this possibilities and how could
I solve the problem ?  

Thank you very much.

-- 
Ernesto Posse
Estudiante de Ingenieria de Sistemas y Computacion
(Systems and Computing Engineering student)
Universidad de los Andes
Santafe de Bogota
Colombia
e-mail: e-posse@uniandes.edu.co

Re: Pattern Matching

[Pierre Weis]

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

Re: Pattern Matching

[Frank Christoph]

> I have a question about pattern matching. I need a function which 
> binds an identifier to a value in certain data structure (which is
> called "heap" here). This is actually a (string * record) list. It is
> not suppose to be a mutable data structure, so the binding just creates
> a
> new list copying the same values as the old one with the exception of
> the
> record to be changed. For this purpose I am using List.map (I am using
> O'Caml 1.01 for Windows 95):

 ...

> 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.

  There is no equality relationship between pattern variables and identifiers
in enclosing scopes unless you make it explicit with a boolean guard.

> 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".

  It's probably because the compiler doesn't know that ((x = y) or (x <> y))
is always true.  The following function definition also generates a complaint:

#let f = function x when x = 1 -> x | x when x <> 1 -> x+1;;
Warning: this pattern-matching is not exhaustive
val f : int -> int = <fun>

  In every compiler I know of, patterns are matched sequentially.  So if you
drop the guard and change the second match to:

 (name,_) as r -> r

it should compile without a warning and have the same semantics, unless you
add a new match case.

------------------------------------------------------------------------
Frank Christoph                 Next Solution Co.      Tel: 0424-98-1811
christo@nextsolution.co.jp                             Fax: 0424-98-1500

stderr

[David Monniaux]

Bonjour,

deux petites remarques en passant:

Contrairement aux usages habituels sur Unix pour les compilateurs, ocamlc
sort ses erreurs sur stdout et non stderr. Ce n'est pas bien grave, a part
que cela met les warnings au debut de la sortie demandee par -i (qui,
elle, devrait rester sur stdout).

Par ailleurs, il arrive quelquefois que l'on fasse volontairement des
pattern-matching incomplets, parce que le programme est tel que les cas
non fournis ne peuvent arriver. ocamlc produit une warning dans ce cas, ce
qui d'ailleurs aide largement a eviter des erreurs de programmation.
Le probleme est que lorsque l'on utilise cette facilite de "warnings" pour
detecter des cas "oublies", on est "parasite" par les pattern-matching
incomplets tout a fait normaux que l'on a laisses. De meme que certains
compilateurs C acceptent des #pragma supprimant un certain avertissement
une fois, que l'on place avant un endroit où l'on a fait volontairement
une construction declenchant cet avertissemment, afin de n'etre pas
derange apres, serait-il possible de mettre un tel systeme dans ocaml?

-- David

"Si l'informatique marchait, cela se saurait."
Computer science student at ENS, Lyon, France
http://www.ens-lyon.fr/~dmonniau

Re: pattern matching

[Olivier Montanuy]

> Par ailleurs, il arrive quelquefois que l'on fasse volontairement des
> pattern-matching incomplets, parce que le programme est tel que les
> cas non fournis ne peuvent arriver. 

 Un programme, ca evolue, et ce qui est vrai aujourd'hui risque de
 ne plus l'etre si une autre personne doit retoucher le code.

 OCAML est ou sera utilise dans des codes ecrits par plusieurs
 personnes, il ne me parait pas judicieux de donner a quiconque un
 moyen de supprimer certains warning en douce. On fait pas du C++.


 match machin-bidule with
   case_normal -> bof
   _           -> failwith "y a un bug"


-- 
Olivier Montanuy  FT/CNET/DES/GRL
montanuy@lannion.cnet.fr

Re: pattern matching

[Stefan Monnier]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1367 bytes --]

Olivier Montanuy <montanuy@lannion.cnet.fr> writes:
> > Par ailleurs, il arrive quelquefois que l'on fasse volontairement des
> > pattern-matching incomplets, parce que le programme est tel que les
> > cas non fournis ne peuvent arriver. 
> Un programme, ca evolue, et ce qui est vrai aujourd'hui risque de
> ne plus l'etre si une autre personne doit retoucher le code.

Pour ces cas là, il serait bien d'avoir une analyse suffisante qui détermine
"oh, ben, dit donc, il manque un cas dans le pattern-matching, mais c'est un
cas impossible alors j'vais rien dire". Comme ça, on évite les warnings (pour
autant que l'analyse est suffisamment maline) mon on a quand même
l'avertissement si qqun change le code.

Un tel système avait plus ou moins été développé pour SML/NJ sous le nom de
refinement-types (quoi que c'était pas tout à fait automatique).

Le compilateur Scheme "Stalin" utilise aussi un système similaire pour
déterminer quelle représentation choisir (éviter les tags quand ils ne
sont pas nécessaires).


        Stefan

-------------------
Version anglophone:

Freeman's refinement-types and other less-sophisticated analysis can get you
the best of both worlds by figuring out that a warning is not necessary
(because the case cannot happen) so that if you change the code, the warning
will reappear if the case becomes possible.


        Stefan