From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id 4AF847EE20 for ; Sat, 17 Nov 2012 18:46:13 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rathereasy@gmail.com) identity=pra; client-ip=209.85.214.180; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="rathereasy@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of rathereasy@gmail.com designates 209.85.214.180 as permitted sender) identity=mailfrom; client-ip=209.85.214.180; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="rathereasy@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ob0-f180.google.com) identity=helo; client-ip=209.85.214.180; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="postmaster@mail-ob0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AikCACjNp1DRVda0k2dsb2JhbABFsBqJNwGJVAgjAQEBAQkJCwkUBCOCHgEBBAEnGQEbEgsBAwELBgULGiEhAQERAQUBChIGEwgKh2gBAwkGC6EAjDOCeIQzChknAwpZiHUBBQyLP2mFDQOIWotNgVWBHIoWgzAWKYQy X-IronPort-AV: E=Sophos;i="4.83,270,1352070000"; d="scan'208";a="162845461" Received: from mail-ob0-f180.google.com ([209.85.214.180]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 17 Nov 2012 18:45:44 +0100 Received: by mail-ob0-f180.google.com with SMTP id wd20so5128584obb.39 for ; Sat, 17 Nov 2012 09:45:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=eLFu2HJaJhNAsVO/slsDn/DAIsiVrdOwBFHBnIFweO4=; b=rOqSDRQUTh7jQwBrlV6SoFYd3RqSSxLOupLw5pFCmycnq9C2yJliZQycpK4h3J4h9M /RWUWNOm5sa5S1cv4bhKAoT5lNzt1LEpniisDziGI8fxVrptFMuy/zhJI2dmDB0+PQJs sfsR4GjWYqdAsnz9cfiglR746q9Z6Y6ynBfggeyabBTFkwikDO5Dz/K7Iv8Grb3NzSKK oS2jzme8yRyUHZhddlUtvbsg/HHh+lAtW+xvQT4GZu+KT3nyBsl7zAvpm6f3e106sMLI vPzoSB4DVHl56Di0jru9Fj06C4jkkuzffmhCRa9ONwle1zCBqS6b9ISp20IceoE9ArpD N8qw== MIME-Version: 1.0 Received: by 10.60.31.177 with SMTP id b17mr6689794oei.77.1353174343428; Sat, 17 Nov 2012 09:45:43 -0800 (PST) Received: by 10.76.97.107 with HTTP; Sat, 17 Nov 2012 09:45:43 -0800 (PST) In-Reply-To: <6E1FE11E-72C5-4AA7-B24A-7E83E139F30C@gmail.com> References: <6E1FE11E-72C5-4AA7-B24A-7E83E139F30C@gmail.com> Date: Sat, 17 Nov 2012 09:45:43 -0800 Message-ID: From: Jacques Le Normand To: Kaspar Rohrer Cc: caml-list caml-list Content-Type: multipart/alternative; boundary=e89a8f8388cb0f2aae04ceb474ee Subject: Re: [Caml-list] GADT exhaustiveness check --e89a8f8388cb0f2aae04ceb474ee Content-Type: text/plain; charset=ISO-8859-1 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 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 --e89a8f8388cb0f2aae04ceb474ee Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable The exhaustiveness check problem IS fundamental to GADTs. The problem is si= milar 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 o= r universal quantifiers, is a quantifier free theorem Z provable using intu= itionistic logic.
I believe that the problem I just stated is semi decidable: if it is p= rovable, then you will find a proof if you search enough. If there is no pr= oof, then you are doomed to search forever. Someone please correct me if I&= #39;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 c= onstructors are of a simpler form: forall a1, ..., an . e -> (b1, b2, ..= ., bn) C where C is our type constructor and b1, ..., bn are arbitrary quan= tifier free formulae. If anyone knows anything about the decidability of th= is potentially simpler problem, I'd very much like to know.

The way O'Caml currently handles GADT exhaustivenes= s 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.=A0

--Jacques

On Sat, Nov 17, 2012 at 4:44 AM, Kaspar Rohrer <kaspar.ro= hrer@gmail.com> wrote:
Hi List

I'm messing around with the new GADT feature in OCaml 4.0, trying to wr= ite a (more or less) strongly typed EDSL. And I've run into non-exhaust= ive pattern-matching warnings (see below for an example). I'm pretty su= re that it is just an inherent shortcoming of GADTs, not a bug. The workaro= und 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 aca= demic, documentation on GADT seems sparse at best. The description of the o= riginal 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
=A0 =A0 =A0 =A0 Kaspar


Code that illustrates the problem:

module T :
=A0 =A0 sig
=A0 =A0 =A0 type 'a t
=A0 =A0 =A0 val int : int t
=A0 =A0 end
=A0 =A0 =3D
=A0 struct
=A0 =A0 type 'a t =3D ()
=A0 =A0 let int =3D ()
=A0 end

type ('r,_) args =3D
=A0 | ANil : ('r,'r) args
=A0 | ACons : 'a * ('r,'b) args -> ('r,'a -> '= ;b) args

let a =3D ANil
let b =3D ACons (3, ANil)

type ('r,'a) fun' =3D
=A0 | FVoid : 'r T.t -> ('r,'r) fun'
=A0 | FLambda : 'a T.t * ('r,'b) fun' -> ('r,'a = -> 'b) fun'

let f =3D FVoid T.int
let g =3D FLambda (T.int, f)

let rec apply : type r a . (r,a) fun' * (r,a) args -> unit =3D funct= ion
=A0 | FVoid t, ANil -> ()
=A0 | 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)
=A0*)
--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://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
<= br>
--e89a8f8388cb0f2aae04ceb474ee--