From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBDF0qbF019272 for ; Tue, 13 Dec 2011 16:00:52 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am0BAFFo507RVdQ2kGdsb2JhbABDmmCQOQgiAQEBAQkJDQcUBCGBcgEBAQQSAiwBGxILAQMMBgULDQ0hIgERAQUBChIGEwgKEIdimQQKi2SCa4RpP4hxAgULg2iHdQSIMIxBimyDCD2EFg X-IronPort-AV: E=Sophos;i="4.71,345,1320620400"; d="scan'208";a="123206635" Received: from mail-vw0-f54.google.com ([209.85.212.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Dec 2011 16:00:47 +0100 Received: by vbbfr13 with SMTP id fr13so8318591vbb.27 for ; Tue, 13 Dec 2011 07:00:46 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=lyx9J4aI/4OlecPU5OGiTXmmqqk3DjSTG3r0F6/XJiY=; b=NESC3EE/BXGyvnOtVHgaz+Or3fd4dRjSehy49vjdVzoqL3DrLE5x/2zQ/ExFY9cvDf 5GiDRDfSVptF2FlavGeR9qVkyYCIbcc3ZkcclklZf1PZXykGIwnSOfsh5wbIixnwOaAh URJKCjA2cUNjqJcCd2qUMHXVpAY5wKMNH/8ag= MIME-Version: 1.0 Received: by 10.52.97.34 with SMTP id dx2mr1484426vdb.3.1323788446206; Tue, 13 Dec 2011 07:00:46 -0800 (PST) Received: by 10.52.92.102 with HTTP; Tue, 13 Dec 2011 07:00:46 -0800 (PST) In-Reply-To: <1323786905.94413.YahooMailNeo@web111503.mail.gq1.yahoo.com> References: <1323786905.94413.YahooMailNeo@web111503.mail.gq1.yahoo.com> Date: Tue, 13 Dec 2011 10:00:46 -0500 Message-ID: From: Jacques Le Normand To: Dario Teixeira Cc: caml Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id pBDF0qbF019272 Subject: Re: [Caml-list] PV-GADTs The way GADTs are handled is that local constraints are generated when patterns are typed and then those constraints are used in the body of the associated clause. To generate the constraints, we need to propagate typing information. From my understanding, we can't do this with polymorphic variants because it would change the typing algorithm. In other words, with polymorphic variants the type of the pattern is infered independently of the context. >From my understanding, Jacques Garrigue has good reasons to reject propagation in such a case. Personally, I'd like to see a flag, say -unsafepropagation, to let people use polymorphic variants and GADTs at their own risk, knowing that the behaviour of the typing algorithm may not satisfy some expected theoretical properties. On Tue, Dec 13, 2011 at 9:35 AM, Dario Teixeira wrote: > Hi, > I wonder, is there any theoretical reason why GADTs cannot be associated with > polymorphic variants?  As an example, consider the two type declarations below. > The first is your run-of-the-mill GADT, supported by the current SVN trunk.  The > second is a PV-GADT, which is not accepted.  But is this just a present limitation > or a fundamental one? > > type _ t1 = Foo: int t1 | Bar: float t1 > > type _ t2 = [ `Foo: int t2 | `Bar: float t2 ] > > > Thanks in advance for your input! > Cheers, > Dario Teixeira > > > -- > Caml-list mailing list.  Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >