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 pBEFC9qM004869 for ; Wed, 14 Dec 2011 16:12:09 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkQBAL276E7RVdc2kGdsb2JhbABDDqsRCCIBAQEBCQkNBxQEIYFyAQEBBBICLAEUBx0BAwwGBQsNLiEBAREBBQEcBhMioXgKi2SCa4UZQIhxAgULi34EiDKMQopsgwk9g0FV X-IronPort-AV: E=Sophos;i="4.71,352,1320620400"; d="scan'208";a="135399153" Received: from mail-lpp01m010-f54.google.com ([209.85.215.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 14 Dec 2011 16:12:04 +0100 Received: by lahl5 with SMTP id l5so724492lah.27 for ; Wed, 14 Dec 2011 07:12:04 -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=UfSwbHKtS7Yl8OZLOClZk3GVRiU6/yzBi2Nu9p+Dw8Y=; b=kTYfQNJSyxepHdqfuId9722uq4NN2Wrj2P3VVX3W9wesm2WMRbsDudN8ax5ZWCvV2p QCSxr7ajs1pY433nfr1zOb5CJvgOdUIaqNjfzJcaKmQC0JcqKF83CCRR4qHQ0j9h21aG AzCAaGLb81XJcpRlxCdPcEgAQuQeRoF/b72GI= MIME-Version: 1.0 Received: by 10.152.104.6 with SMTP id ga6mr2936164lab.45.1323875523922; Wed, 14 Dec 2011 07:12:03 -0800 (PST) Received: by 10.152.30.38 with HTTP; Wed, 14 Dec 2011 07:12:03 -0800 (PST) In-Reply-To: References: <1323786905.94413.YahooMailNeo@web111503.mail.gq1.yahoo.com> Date: Wed, 14 Dec 2011 10:12:03 -0500 Message-ID: From: Markus Mottl To: Jacques Garrigue Cc: Dario Teixeira , 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 pBEFC9qM004869 Subject: Re: [Caml-list] PV-GADTs On Tue, Dec 13, 2011 at 21:56, Jacques Garrigue wrote: > 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. I really like using PVs for defining extensible, recursive DSLs. If it were possible to use GADTs in a similar way, that would be an awesome feature. But I wonder how this could be done cleanly. I agree that type inference would be impractical when combining PVs and GADTs, since PV constructors are not tied to a specific type. It seems you have something in particular in mind when you speak of extensible GADTs. Wouldn't such a feature require that GADTs have the same runtime representation as PVs, i.e. using the hash value of the variant name? Not sure what the GADT representation is right now anyway, but maybe this should be determined carefully before the next release if we want to add extensibility later. Regards, Markus -- Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com