From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBE2uRl9005375 for ; Wed, 14 Dec 2011 03:56:27 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap0BAIAP6E7RVdQ2kGdsb2JhbABDmmiQMQgiAQEBAQkJDQcUBCGBcgEBAQQSAiwBOAEDDAEFBQsNLiISAQUBChIGEyKhMQqOT4R6iTACBQuLaASIL4xDimyDCD2BTYI6 X-IronPort-AV: E=Sophos;i="4.71,349,1320620400"; d="scan'208";a="135305537" Received: from mail-vw0-f54.google.com ([209.85.212.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 14 Dec 2011 03:56:21 +0100 Received: by vbbfr13 with SMTP id fr13so469782vbb.27 for ; Tue, 13 Dec 2011 18:56:20 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; bh=3LECdqLarzH96LPjFSxUz0UYzXjgdoftL52KHKmho5I=; b=e2JMppZkHxp4ZeyyNe7ix1bnpusELB1zZCn/fQolhkvdtlAPOjDO6tG1+ojte9WbWY fRprlk9jiYC6zeiKWDNYdHJtOLKHClBcbd9IC73xRdjzx68h3tDEif7O9xQG+wnrs1fs W/Ka1Svxb000Q9Izz0gdxJ7dVjRTMDODlX9Eo= MIME-Version: 1.0 Received: by 10.52.65.129 with SMTP id x1mr3133898vds.11.1323831380640; Tue, 13 Dec 2011 18:56:20 -0800 (PST) Sender: jacques.garrigue@gmail.com Received: by 10.220.210.137 with HTTP; Tue, 13 Dec 2011 18:56:20 -0800 (PST) In-Reply-To: <1323786905.94413.YahooMailNeo@web111503.mail.gq1.yahoo.com> References: <1323786905.94413.YahooMailNeo@web111503.mail.gq1.yahoo.com> Date: Wed, 14 Dec 2011 11:56:20 +0900 X-Google-Sender-Auth: Fw6_L9Cc2oJHeKpqR6mN8XGyMYM Message-ID: From: Jacques Garrigue 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 pBE2uRl9005375 Subject: Re: [Caml-list] PV-GADTs On Tue, Dec 13, 2011 at 11:35 PM, 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 ] Actually, Jacques Le Normand didn't directly answer your question. He just explained why we cannot currently combine polymorphic variants and GADTs in the same pattern-matching. This could be improved if the need is clear. However what you are asking for is different: you want indexed polymorphic variants. But there the problem is more fundamental. The strength of polymorphic variants is that you don't have to define them. But if you don't relate the constructors to a specific type, there is no way you can constrain the index. In your example, how do you know in a pattern-matching that `Foo comes from t2? Type inference could be used, but I'm afraid it would be very fragile, and not easy to use. So at this point there is no plan to add GADT PVs. An alternative design would be to have extensible GADTs, where you would be able to add new cases, like for exn. I think this would be useful, and cover some uses that are not possible even with PVs. Jacques Garrigue