More intelligent match warnings

More intelligent match warnings

[David Allsopp]

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. However, it's not really incomplete because
the branch cannot be hit if x = A so the warning is "sort of" incorrect. In
fact, it would also be good if one wrote:

type t = A | B | C
let f x =
  match x with
    A -> 1
  | _ -> match x with
           A -> 1 (* XX *)
         | B -> 2
         | C -> 3

to get a warning that the branch marked XX cannot be reached.

Are these two cases decidable in the general case? 


David

Re: [Caml-list] More intelligent match warnings

[Jon Harrop]

On Thursday 08 February 2007 18:01, David Allsopp wrote:
> Are these two cases decidable in the general case?

It depends how general you make your proposal. In this case, the error can be 
avoided by writing better code, using a single pattern match. When does "in 
general" make that impossible?

You can also do something similar using polymorphic variants to implement 
unions of sum types:

# type a = [`A]
  type bc = [`B | `C];;

  let f : [ a | bc ] -> int = function
    | `A -> 0
    | #bc as b -> match b with
        | `B -> 1
        | `C -> 2;;
val f : [< `A | `B | `C ] -> int = <fun>

Here, the value matching #bc is known to be either `B or `C but not `A.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] More intelligent match warnings

[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