Re: [Caml-list] More intelligent match warnings

[maranget@yquem.inria.fr (Luc Maranget)]

> Say I write the following rather pointless piece of code:
> 
> type t = A | B | C
> let f x =
>   match x with
>     A -> 1
>   | _ -> match x with
>            B -> 2
>          | C -> 3
> 
> The compiler emits Warning P for the second match because it's incomplete
> over the constructors of type t.
Indeed it does.


> However, it's not really incomplete
Well I guess that completeness is in the eye of the viewer,
you and the compiler do not have the same eye.
The compiler is shortsighted...

> .. SNIP... <

> 
> Are these two cases decidable in the general case? 
> 
What are you asking for exactly ?

If you give one example of which all computations terminate
well, exhautiveness is indeed decidable.

More seriously, PM checks are performed independently, and at times
sometimes quite unexpected, due to interaction with typing.

It is a pity not to consider interaction beetween PM
expressions.  However consider that it makes the compiler simpler,
safer and faster.



More generally if you have

match x with
| p_1 -> ... | p_{n-1} -> ..
| p_n ->HERE ... THERE

Then, at point HERE (just after ->, we also assume no where clauses)
we have some information about x :

  x does not match all the pattern [p_1 ; ... ; p_{n-1} ]
  x matchs the pattern p_n

In your example we know that x does not match [A] and that it matches _

This information is complete for performing PM checks (and optimized
compilation).  In fact, warnings and compilation of one PM expression,
compute and use exactly that information (compilation sometimes
forget  it for the sake of not having too big data structures).

Later, at point THERE, well it depends, especially if
matched x has mutable subcomponents.

Now consider variations on your example

(*1*)
type t = A | B | C

let f x =
  match x with
    A -> 1
  | _ -> let y = x in
         match y with (* exhaustive *)
           B -> 2
         | C -> 3

Of even worse

(*2*)
let f x =
  match x with
    A -> 1
  | _ -> let y = match x with B -> C | C -> B in (* exhaustive *)
         match y with (* exhaustive *)
           B -> 2
         | C -> 3

I guess (just a guess) that saved from running the program for all
possible value, a compiler can decide statically that the matches
are exhaustive.

1. Keep track of variable values (I mean
   associate pairs [p1.. pn-1], pn to variables), consider aliases.
2. Also consider information infeered from performing PM
   more involved but doable.
    a - since x is [A],_ the first match is exhaustive,
        one of the two clauses matches.
    b - The result is the union of [], C and [],B, that is
        [],(B|C)
    c - y is bound to  [],(B|C)
    d - the second match is exhaustive.



I am sure that implementing even 1, is a some amount of work,
I am not sure that users would even notice the difference...


> David
> 

-- 
Luc Maranget