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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 1D0797EE51 for ; Mon, 29 Apr 2013 12:52:14 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: An8EAMZPflGFBoIFdGdsb2JhbABTwgWBGA4BDBUIPIIfAQEEAUMBNwMLCxgcElcGExuHdQWqO4REAoUKh2oHjmc6gm5hiROODpRK X-IPAS-Result: An8EAMZPflGFBoIFdGdsb2JhbABTwgWBGA4BDBUIPIIfAQEEAUMBNwMLCxgcElcGExuHdQWqO4REAoUKh2oHjmc6gm5hiROODpRK X-IronPort-AV: E=Sophos;i="4.87,572,1363129200"; d="scan'208";a="12579142" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Apr 2013 12:52:11 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id BF1CF6297 for ; Mon, 29 Apr 2013 19:52:07 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id CF82C2529 for ; Mon, 29 Apr 2013 19:52:06 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id C6D822504 for ; Mon, 29 Apr 2013 19:52:04 +0900 (JST) Content-Type: text/plain; charset=windows-1252 Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) From: Jacques Garrigue In-Reply-To: <517E2818.5040506@frisch.fr> Date: Mon, 29 Apr 2013 19:52:03 +0900 Content-Transfer-Encoding: quoted-printable Message-Id: <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <517E2818.5040506@frisch.fr> To: OCaML List Mailing X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs Dear Camlers, First, let me reiterate my request for feedback: What I want to know is whether anybody is using GADTs in a way that would be broken if we disallow type variables under abstract types (other than the predefined ones) in the return type of GADTs. I.e., for instance defining a type witness type involving such abstract typ= es. This is really the question I want you all to answer. If this is not the case, we can safely prohibit that at this point, and take our time to think about the solution. But if there are some users, we had better provide at least some mechanism, and injectivity annotations seem to be the less intrusive (they don't break any code, at least any existing code). We may need to make clear that they are experimental and might disappear, but at least we are not in a complete void. Now just my 2 centimes on alternative approaches On 2013/04/29, at 16:58, Alain Frisch wrote: > On 04/29/2013 07:17 AM, Jacques Le Normand wrote: >> Fully injective types are the norm. It would have been nice to have a >> "non injectivity" or "phantom type" annotation. Since phantom types are >> seldom used, beginners won't get confused. It might even help beginners >> understand the concept of a phantom type. >=20 > I'd also prefer an annotation on "non injective" type parameters, rather = than on "injective" one. The problem with this approach is that it require= s existing well-typed code to be rewritten, to add these annotations (while= annotating injectivity will only impact code using GADTs). I still believ= e this is less intrusive than requiring most parametrized abstract type to = be annotated, or else making GADTs less useful. This may be a good idea for 5.00, but honestly this is a big change. Moreover it is not so clear that this is the right choice for functors: when a functor takes an abstract type as argument, it usually doesn't care whether it is injective or not. And in practice there is a technique of add= ing a type parameter to abstract types just in case we want to pass a parameter= ized type, but usually using this functor for non-parameterized types. Another point is that I'm not sure how much "less useful" GADTs become when= one forgets an injectivity annotation somewhere. > For the transition, we could have two compilation modes (decided on the c= ommand-line) for this feature. In "non-injective" (legacy) mode, every par= ametrized abstract type would be assumed to be non-injective. This would a= llow to compile existing code bases (at least those not relying on GADTs). = In "injective-by-default" mode, non-injective parameters would need to be = marked as such. Enabling this mode will require a few annotations to be ad= ded to existing code, but this will be very easy, so I guess we don't need = to support "injectivity" annotations the "non-injective" mode. Again, the defect of such a mode is that it is going to apply to everything= , including functors. A functor compiled in this mode might be not be applicable to some modules,= whereas there was no reason from the beginning to require injectivity there. And just using variance to change the behavior is not going to work well: a standard practice is to explicitly define module types for the input and = output of the functor. We want the output types to be injective, but we don't really = need such requirement for the input types. But they are just module type definitions= =85 (See hashtbl.mli for instance for this pattern.) Jacques=