* Re: [Caml-list] GADT exhaustiveness check
2012-11-17 12:44 [Caml-list] GADT exhaustiveness check Kaspar Rohrer
@ 2012-11-17 17:45 ` Jacques Le Normand
2012-11-17 18:20 ` Jeremy Yallop
1 sibling, 0 replies; 3+ messages in thread
From: Jacques Le Normand @ 2012-11-17 17:45 UTC (permalink / raw)
To: Kaspar Rohrer; +Cc: caml-list caml-list
[-- 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 --]
^ permalink raw reply [flat|nested] 3+ messages in thread* Re: [Caml-list] GADT exhaustiveness check
2012-11-17 12:44 [Caml-list] GADT exhaustiveness check Kaspar Rohrer
2012-11-17 17:45 ` Jacques Le Normand
@ 2012-11-17 18:20 ` Jeremy Yallop
1 sibling, 0 replies; 3+ messages in thread
From: Jeremy Yallop @ 2012-11-17 18:20 UTC (permalink / raw)
To: Kaspar Rohrer; +Cc: caml-list
Dear Kaspar,
On 17 November 2012 12:44, Kaspar Rohrer <kaspar.rohrer@gmail.com> wrote:
> 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.
[...]
> 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)
> *)
Here's how you know that the offending pattern can never match a value: the
ANil constructor would constrain "r" and "a" to denote the same type, and the
arguments of the FLambda constructor would have types "'a T.t" and "('a -> 'b,
'b) fun'" (for suitable 'a and 'b). It's then sufficient to show that at
least one of these types is not inhabited. However, in order to show this you
need to use information about the possible ways of building values of those
types: for example, you need to know that there's no polymorphic value of type
"'a t". If you add such a value to the T module:
module T :
sig
type 'a t
val int : int t
val poly : 'a t
end
=
struct
type 'a t = ()
let int = ()
let poly = ()
end
then you *can* build values that match the missing patterns:
# apply (FLambda (T.int, FVoid T.poly), ANil)
Exception: Match_failure ("//toplevel//", 113, 9).
I don't think that the exhaustiveness checker has any information available
regarding the possible ways of constructing values of an abstract type.
Here's an example without GADTs illustrating the same issue. Suppose we have
your original definition of the T module:
module T :
sig
type 'a t
val int : int t
end
=
struct
type 'a t = ()
let int = ()
end
We can define a datatype with two constructors using T.t:
type s =
Int of int T.t
| Float of float T.t
Since there is no value of type "float T.t", patterns involving the Float
constructor are redundant. However, the exhaustiveness checker doesn't know
that, so you'll still get a warning for omitting the Float case:
Characters 8-28:
let f = function Int _ -> ();;
^^^^^^^^^^^^^^^^^^^^
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Float _
Hope that helps a bit,
Jeremy.
^ permalink raw reply [flat|nested] 3+ messages in thread