Re: [Caml-list] GADT exhaustiveness check

[Jacques Le Normand <rathereasy@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3224 bytes --]

The exhaustiveness check problem IS fundamental to GADTs. The problem is
similar to one of theorem proving:
given theorems t1, t2, ..., tn, all of the form forall a1, ..., an. e,
where e does not contain any existential or universal quantifiers, is a
quantifier free theorem Z provable using intuitionistic logic.
I believe that the problem I just stated is semi decidable: if it is
provable, then you will find a proof if you search enough. If there is no
proof, then you are doomed to search forever. Someone please correct me if
I'm wrong.

In our case, t1, t2, ..., tn are the constructors and Z is the type of the
guard. Our problem is simpler because the type of our constructors are of a
simpler form: forall a1, ..., an . e -> (b1, b2, ..., bn) C where C is our
type constructor and b1, ..., bn are arbitrary quantifier free formulae. If
anyone knows anything about the decidability of this potentially simpler
problem, I'd very much like to know.

The way O'Caml currently handles GADT exhaustiveness is like so: it
searches for non exhaustive patterns in the same manner as before and
whatever it finds it tries to type. However, these patterns may contain
wildcards.

--Jacques

On Sat, Nov 17, 2012 at 4:44 AM, Kaspar Rohrer <kaspar.rohrer@gmail.com>wrote:

> Hi List
>
> I'm messing around with the new GADT feature in OCaml 4.0, trying to write
> a (more or less) strongly typed EDSL. And I've run into non-exhaustive
> pattern-matching warnings (see below for an example). I'm pretty sure that
> it is just an inherent shortcoming of GADTs, not a bug. The workaround is
> easy as well, simply add a catch all clause with a runtime error to silence
> the warning, and prove manually that the offending patterns can not occur.
>
> I tried to find more information on this topic, but without getting all
> academic, documentation on GADT seems sparse at best. The description of
> the original implementation at https://sites.google.com/site/ocamlgadt/seems to be the most comprehensive I've found so far. And I'm not sure the
> information about exhaustiveness is still up to date.
>
> It would be nice if somebody could maybe shed some more light on this.
>
> Cheers
>         Kaspar
>
>
> Code that illustrates the problem:
>
> module T :
>     sig
>       type 'a t
>       val int : int t
>     end
>     =
>   struct
>     type 'a t = ()
>     let int = ()
>   end
>
> type ('r,_) args =
>   | ANil : ('r,'r) args
>   | ACons : 'a * ('r,'b) args -> ('r,'a -> 'b) args
>
> let a = ANil
> let b = ACons (3, ANil)
>
> type ('r,'a) fun' =
>   | FVoid : 'r T.t -> ('r,'r) fun'
>   | FLambda : 'a T.t * ('r,'b) fun' -> ('r,'a -> 'b) fun'
>
> let f = FVoid T.int
> let g = FLambda (T.int, f)
>
> let rec apply : type r a . (r,a) fun' * (r,a) args -> unit = function
>   | FVoid t, ANil -> ()
>   | FLambda (t,f), ACons (_,a) -> apply (f,a)
> (*
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> (FLambda (_, _), ANil)
>  *)
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

[-- Attachment #2: Type: text/html, Size: 4262 bytes --]