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 1E9727EE51 for ; Sun, 28 Apr 2013 12:28:26 +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: AgwEAB/5fFGFBoIFnGdsb2JhbABTwXsEBAGBFA4BAQEBAQgUCTyCHwEBBAFDATUCAwsLGBwSITYGExuHaQMJBatjhEQChBgNTIdqB4xEgROBEDMHgm5hiROMKoFkjAuIPw X-IPAS-Result: AgwEAB/5fFGFBoIFnGdsb2JhbABTwXsEBAGBFA4BAQEBAQgUCTyCHwEBBAFDATUCAwsLGBwSITYGExuHaQMJBatjhEQChBgNTIdqB4xEgROBEDMHgm5hiROMKoFkjAuIPw X-IronPort-AV: E=Sophos;i="4.87,566,1363129200"; d="scan'208";a="12488201" 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; 28 Apr 2013 12:28:23 +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 91AC262E4; Sun, 28 Apr 2013 19:28:19 +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 DAD01395D; Sun, 28 Apr 2013 19:28:16 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 477E93A19; Sun, 28 Apr 2013 19:28:16 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) Content-Type: text/plain; charset=iso-8859-1 From: Jacques Garrigue In-Reply-To: Date: Sun, 28 Apr 2013 19:28:24 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <0F60A861-8DC4-41C8-98FA-B86FF53A4D39@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> To: Markus Mottl X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 2013/04/28, at 11:45, Markus Mottl wrote: > On Sat, Apr 27, 2013 at 8:02 PM, Jacques Garrigue > wrote: >> The fix is simple enough: we should track injectivity, and assume that a= bstract >> types are not injective by default. >> However, this also means that the first type I defined above (using Hash= tbl.t) >> will be refused. >=20 > If I understand your proposal correctly, the first type would only be > refused unless the standard Hashtbl module were updated with > appropriate injectivity annotations. The type variables in the GADT > would not need any annotations, because it is assumed that they have > to be injective there anyway for soundness. Yes, only abstract types need to be annotated. Injectivity only makes sense for type aliases and abstract types (and priva= te row types, which hide an abstract type), since concrete types are always injective. Fo= r instance, type 'a t =3D T of int is injective (you cannot unify int t with bool t). >> How many of you are using GADTs in this way, and how dependent are you on >> abstract types ? >=20 > This seems like a "one percenter" problem. OTOH, I guess most people > also rarely run into problems where variance annotations matter, but > if they do, they have no option. The question should therefore rather > be: what's the alternative? Are there workarounds? If not, > annotations may just be a necessity to support advanced use cases. At this point I think very few people are concerned. So it might be the case that we could delay injectivity annotations until 4= .02. However, there is no easy workaround for abstract types. The simplest one I can think of is duplicating types: type ('a,'b) t_impl type ('a, 'b) =3D Hashtbl of ('a,'b) t_impl >> If we need to be able to define GADTs relying on the injectivity of some= abstract >> types, a straightforward solution is to add injectivity annotations on t= ype parameters, >> the same way it was done for variance: >>=20 >> type #'a t >>=20 >> would mean that t is injective. >=20 > Seems concise, but I'm just a little worried that we may be raising > the bar for beginners again. The standard library would have to be > updated with another annotation that may seem as obscure to beginners > as variance annotations. I hope we'll never have to explain to a > beginner the meaning of $%^&#-'a. Maybe a more verbose type > constraint language would have been the better design choice here, but > I guess we've already left this path with variance annotations. As Jacques Le Normand pointed, injectivity is a property of parameters, not of the whole type. (But in most cases a type is injective in all its pa= rameters). The addition of hard to read information is indeed the main drawback. The fortunate part here is that, as long as you don't use GADTs, you need n= ot understand the meaning. >> If you are curious about other difficulties of GADTs, the is also branch= es/abstract-new >> which introduces a notion of new types, either concrete or abstract, whi= ch are guaranteed >> to be distinct from each other, and any other concrete type. This is use= ful when >> checking the exhaustiveness of pattern-matching, as we can then discard = impossible >> branches. That branch is completely experimental. >=20 > I haven't looked at this feature yet, but would this require even more > annotations in the standard library? If so, maybe it would indeed be > time to think about a more accessible syntax for type constraints. This is not really a replacement, since the requirements to be "new" are ra= ther restrictive. However, as a new type is automatically injective in all its p= arameters, you would never need to make its injectivity explicit. But we need indeed to think about the syntax. All the more as other features, like the addition of runtime type informati= on, may also require annotations on types. Jacques