From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 1F4FDE00E5 for ; Tue, 6 Oct 2020 22:10:55 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=josh@berdine.net; spf=Pass smtp.mailfrom=josh@berdine.net; spf=Pass smtp.helo=postmaster@out3-smtp.messagingengine.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of josh@berdine.net) identity=pra; client-ip=66.111.4.27; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="josh@berdine.net"; x-sender="josh@berdine.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of josh@berdine.net designates 66.111.4.27 as permitted sender) identity=mailfrom; client-ip=66.111.4.27; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="josh@berdine.net"; x-sender="josh@berdine.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@out3-smtp.messagingengine.com designates 66.111.4.27 as permitted sender) identity=helo; client-ip=66.111.4.27; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="josh@berdine.net"; x-sender="postmaster@out3-smtp.messagingengine.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" IronPort-PHdr: =?us-ascii?q?9a23=3AXR+PAhJGFGV2gYEN19mcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgXKv77rarrMEGX3/hxlliBBdydt6sbzbaK+Pm5ByQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTagY75+Nhq7oAreusULnIdvK7s6xwfUrHdPZ+?= =?us-ascii?q?lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRne?= =?us-ascii?q?VgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gy?= =?us-ascii?q?ocKTU37H/YhdBxjKJDoRKuuRp/w5LPYIqIMPZyZ77Rcc8GSWZEWMtaSi5PDZ6m?= =?us-ascii?q?b4YXE+UOMvtWoYn/qFUAohWwBgesCv3oxDJTmn/2xKg63/ghEQ3a3gEtGc8Fvn?= =?us-ascii?q?TOrNXyMacfSeS7zK7TzTXDcvhbxCny6JLVfRAgp/GDQ697fM3TyUkoDAPFjk6d?= =?us-ascii?q?ppf7MDOPy+sNsm6b4PR6WeKplWEntxh8rz6yzcgjlofHnJgaykzY9Spn2oY1I8?= =?us-ascii?q?W1RUF7bNCqEpZcqTyWOpZyT80tQmxkpCI3x78btZKneCUG1JYqygPDZvCac4aF?= =?us-ascii?q?/BLuWeKeLzp7i3xrd72xihas/EWm1+byVdG03U5LoydEiNXAq20B2wHJ5sWIUP?= =?us-ascii?q?dx4EWs1S6M2gzN8O1IP0A5mbDGJ5MiwrM8jIQfvErfEiLwhU77kquWdlg/+ui0?= =?us-ascii?q?9evneKjopp6dNoBqkgzyLqIjkdGlD+siKAgBRW2b9Py81LL9+U35R61Hjvorkq?= =?us-ascii?q?nFvp3WPN8bpqulAw9NyIoj7giwDyy90NsCknkHLVRFeB2ZgIjvNFHOIfb4Auml?= =?us-ascii?q?j1uwlzdrwujKPrznAprTMnjOiLbscLdn50JB1QY/0MpT6p1OBr0fIv//Qkrxu8?= =?us-ascii?q?bZDh89PQy02eHnCNBl24McXmKPGa+ZPbjJvlCW/OIgPuiMZIkLtzrnLfgq+eLu?= =?us-ascii?q?gWcjmVABZampwYcXaHegE/t6OUqZZH7sjs4FEWcLpQo+UPfniEaCUD5Wf3a9Rb?= =?us-ascii?q?gw5jA9CIK8DIfMXJqhgLKb3C2jBJ1ZenhGCkyQEXfvb4iEVe8MaCWOIs99kzwL?= =?us-ascii?q?S6KhRpQg1BGvsQ/10KBnIfDO9i0Zs5Ljztl16PfJmRE87zwnR/iahk+XRmf7mW?= =?us-ascii?q?ITcAcxwLx+rFY1nlmZ2K5zhP1DU8RU++9IXx0SNJjGzuU8BcqkHkrjd9yQVVu9?= =?us-ascii?q?CvqvGyswQc88i4sMak1kBti5yB/KxTCrDKIYv7OODZ0wtKnb2i6iCdx6ziPk07?= =?us-ascii?q?Ihx3MrWMdOM2Du0qx47Aj7DYPTn0SfmuCseLhKj32Fz3uK0Wfb5BIQawV3S6iQ?= =?us-ascii?q?GClHPhKL/+S83VvLSvqVMZpiMgZFzpXbeKxXdoasllBaXLHmNc/Fam2wnWi9Ax?= =?us-ascii?q?mJwL7KZ43vKTxEjXftTXMcmgVWxk6ocA03ByOvuWXbVWc8H1/1b0Lq/K94pW/p?= =?us-ascii?q?FxZonTHPVFVo0v+OwjBQneaVEqhB1L8etCYnpnNyEUrvh98=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CuAAD9znxfhxsEb0JgHAEBAQEBAQcBA?= =?us-ascii?q?RIBAQQEAQFAgU+DcAEBMCyEPYkCiDqBAoJ4hheSFQsBAwENLwQBAYRKAoIHAh4?= =?us-ascii?q?GAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQoLCQgphWMMgjcpAYMRAQEBAQIBIwQZA?= =?us-ascii?q?QEwBwEECwsYAgImAgIhNgYBEoMmgkwDDiAEp392fzODAQEBBYJMgk4NYoE5CYE?= =?us-ascii?q?OKo0zGz6BQoERJxyCGAcuPoIagW02gxczgi2QEY1VmRtSgnKBEpRHhQ4fgRSRA?= =?us-ascii?q?BWOfpMWjVmOYIQHgWuBejMaCCYKOyoBgj4+EhkNhDyJYwwOCRSDOoRZhX5AAQE?= =?us-ascii?q?xNwIGAQkBAQMJjkgBAQ?= X-IPAS-Result: =?us-ascii?q?A0CuAAD9znxfhxsEb0JgHAEBAQEBAQcBARIBAQQEAQFAgU+?= =?us-ascii?q?DcAEBMCyEPYkCiDqBAoJ4hheSFQsBAwENLwQBAYRKAoIHAh4GAQQ0EwIQAQEFA?= =?us-ascii?q?QEBAgEDAwQBEwEBAQoLCQgphWMMgjcpAYMRAQEBAQIBIwQZAQEwBwEECwsYAgI?= =?us-ascii?q?mAgIhNgYBEoMmgkwDDiAEp392fzODAQEBBYJMgk4NYoE5CYEOKo0zGz6BQoERJ?= =?us-ascii?q?xyCGAcuPoIagW02gxczgi2QEY1VmRtSgnKBEpRHhQ4fgRSRABWOfpMWjVmOYIQ?= =?us-ascii?q?HgWuBejMaCCYKOyoBgj4+EhkNhDyJYwwOCRSDOoRZhX5AAQExNwIGAQkBAQMJj?= =?us-ascii?q?kgBAQ?= X-IronPort-AV: E=Sophos;i="5.77,343,1596492000"; d="scan'208";a="361046795" X-MGA-submission: =?us-ascii?q?MDFvG6o4K76zatBmgxtM8G6z+YlJjS4H4Pfk0O?= =?us-ascii?q?Lkt3oIfSzo1lkxGQRT4zHGDFu6krJu43QeDgNrsMfPuRyHB/Ue2cKI/Y?= =?us-ascii?q?D9RZgXaC8aLG4QQ2hK9T42WafvDToQGmos5iIjn7V5Pw0PymHryR0QVC?= =?us-ascii?q?cueUh4V/nazBGmeVyo5d/89w=3D=3D?= Received: from out3-smtp.messagingengine.com ([66.111.4.27]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 06 Oct 2020 22:10:19 +0200 Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.nyi.internal (Postfix) with ESMTP id 7691C5C0164; Tue, 6 Oct 2020 16:10:17 -0400 (EDT) Received: from mailfrontend1 ([10.202.2.162]) by compute3.internal (MEProxy); Tue, 06 Oct 2020 16:10:17 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=berdine.net; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=fm1; bh=o c0Jf40rRI6NeM2hUWqPHUijBqzhwXpJAzKT74rFd7U=; b=td07twfDH62s8fQ+x Yq3u1t50ukNR1bTv90A9a/1cDwsF866hR9nb8taCIy26pvhL/7ROuBQDDQGN43F8 0/fNAasm9aOky+0817WSkLco3WgjtmUImJ2ywZ3nm57QFM4m/zzps6WpH0vXDV67 Ac/8FjL6nNclD1vGYy7clhCjQ7ob5+8hJgDdWnO3fMEaUBdcrqnwFCbXJvGW455b +OnDQ7Vw4VfcrGF/zaR8eGNENQMOsUP+RXBGCWyag0HUAmi1pSNGSMUo9m+MGS39 75nab5e0Mvm8U3j6t7MkD8DWRNID4FbFVBN+0gjmQDIR+TOC2IR5VXj0kuF07QKZ vWYlw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc:content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-proxy:x-me-proxy:x-me-sender:x-me-sender :x-sasl-enc; s=fm1; bh=oc0Jf40rRI6NeM2hUWqPHUijBqzhwXpJAzKT74rFd 7U=; b=n53CeddHmqyX7aux9T9hK+2FhGthYufSLFOQh6wdmZA/M7Wi9PzON+MA1 k5XYcDRURq6zmnILuCfJC+v1vmVxdXgCZVNXBMp7jh8NTT3crnfqK4ET0/t3bxMC ZPAZDx5GlJ9aaiP3ONiUbBZ/Udb5R6r3elJw4zl18/mS1ydIEGK/f5VNByDKz44Y 4g4YyWBhYFS3W3YSvOiTNWeDPozN8eJVTUHfhygIcXs2/TrsNiJfJshP+G12GHiu BAjRTqRXGfOo40ROrKatTIgkwxa6XMVaBLe00HD1wb9Xlls/AqA6yphp1hfj7BfP ken8oxrN+1xoVH8/KZ2bRajAo+SHw== X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedujedrgeeggddugeefucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne cujfgurheptggguffhjgffgffkfhfvofesthhqmhdthhdtjeenucfhrhhomheplfhoshhh uceuvghrughinhgvuceojhhoshhhsegsvghrughinhgvrdhnvghtqeenucggtffrrghtth gvrhhnpeegheffjedvudeulefgiedtleejuddtledtjeeuteduhfevheelgfekgffggfeh veenucfkphepkedvrddvhedrudekhedrvdeftdenucevlhhushhtvghrufhiiigvpedtne curfgrrhgrmhepmhgrihhlfhhrohhmpehjohhshhessggvrhguihhnvgdrnhgvth X-ME-Proxy: Received: from [192.168.0.36] (cpc87533-seve28-2-0-cust229.13-3.cable.virginm.net [82.25.185.230]) by mail.messagingengine.com (Postfix) with ESMTPA id AD2CD328005A; Tue, 6 Oct 2020 16:10:16 -0400 (EDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 13.4 \(3608.120.23.2.4\)) From: Josh Berdine In-Reply-To: Date: Tue, 6 Oct 2020 21:10:15 +0100 Cc: caml-list Content-Transfer-Encoding: quoted-printable Message-Id: <94E068C0-D2CC-42F4-A52D-A4981DF471B4@berdine.net> References: <20201006160519.GA2217@Melchior.localnet> To: =?utf-8?Q?Fran=C3=A7ois_Pottier?= , Jacques Garrigue X-Mailer: Apple Mail (2.3608.120.23.2.4) Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) > On Oct 6, 2020, at 8:18 PM, Fran=C3=A7ois Pottier = wrote: >=20 > I am still curious, though, to know why my original type +'a t is not > recognized as covariant by the OCaml type-checker... Jacques helpfully gave a precise answer earlier: > On Jun 22, 2020, at 8:39 AM, Jacques Garrigue = wrote: >=20 > The best I can say is that this combination of GADTs and polymorphic = variants is not supported. > There are actually two distinct problems: > * GADT indices must be invariant > * refinement of row types (both polymorphic variants and object types) = is only partially supported > (you can instantiate an existential row only once) >=20 > So I wouldn=E2=80=99t suggest investing time in trying to outsmart the = type system in this direction. > The best you could achieve would be discovering a soundness bug (which = should of course be promptly reported). >=20 > If your goal is just to move the polymorphism from the type itself to = its parameter, using normal phantom types (maybe combined with phantom = types to allow pattern matching) could help you, even if it may leave a = few runtime checks. >=20 > Otherwise, you may try to encode your domain in a proper GADT, not = using polymorphic variants. > There are ways to keep some degree of subsumption. >=20 > By the way, I=E2=80=99m not sure what you mean by =E2=80=9Cweaker = exhaustiveness=E2=80=9D of polymorphic variants. > I agree that polymorphic variants give weaker typing, it that they = infer the declarations, but at least closed pattern-mathcing on them do = guarantee exhaustiveness. Jacques, I am sorry that I failed to address this before. I did not mean = to imply that there was a problem, by "weaker exhaustiveness" I only = mean that for a pattern match that is missing an intended case, the type = error involving the inferred type can end up "far away" from the point = of the mistake in the code. One way around this is to add type more = annotations so that an incompatibility cannot propagate as far. But this = relies on programmer-discipline rather than being irrefutably enforced = by the type system. Cheers, Josh > Jacques >=20 > P.S. Here is an example of specific domain encoding: >=20 > type =E2=80=98a number =3D Number of =E2=80=98a >=20 > type _ exp =3D > | Integer : int -> int number exp > | Float : float -> float number exp > | Add : =E2=80=98a number exp * =E2=80=98a number exp -> =E2=80=98a = number exp > | String : string -> string exp >=20 > or >=20 > type number =3D Number >=20 > type _ exp =3D > | Integer : int -> number exp > | Float : float -> number exp > | Add : number exp * number exp -> number exp > | String : string -> string exp >=20 > Basically, you must choose between what is static and what is dynamic. >=20 > On 21 Jun 2020, at 18:10, Josh Berdine wrote: >>=20 >> I wonder if anyone has any suggestions on approaches to use GADTs = with a type parameter that is phantom and allows subtyping. >>=20 >> (My understanding is that the approach described in=20 >> "Gabriel Scherer, Didier R=C3=A9my. GADTs meet subtyping. ESOP 2013" >> hasn't entirely been settled on as something that ought to be = implemented in the compiler. Right? Is there anything more recent = describing alternatives, concerns or limitations, etc.?) >>=20 >> As a concrete example, consider something like: >> ``` >> type _ exp =3D >> | Integer : int -> [> `Integer] exp >> | Float : float -> [> `Float] exp >> | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp >> | String : string -> [> `String] exp >> ``` >> The intent here is to use polymorphic variants to represent a small = (upper semi-) lattice, where basically each point corresponds to a = subset of the constructors. The type definition above is admitted, but = while the index types allow subtyping: >> ``` >> let widen_index x =3D (x : [`Integer] :> [> `Integer | `Float]) >> ``` >> this does not extend to the base type: >> ``` >> # let widen_exp x =3D (x : [`Integer] exp :> [> `Integer | `Float] = exp);; >> Line 1, characters 18-67: >> 1 | let widen_exp x =3D (x : [`Integer] exp :> [> `Integer | `Float] = exp);; >> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ >> Error: Type [ `Integer ] exp is not a subtype of >> ([> `Float | `Integer ] as 'a) exp=20 >> The first variant type does not allow tag(s) `Float >>=20 >> ``` >> This makes sense since `type _ exp` is not covariant. But trying to = declare it to be covariant doesn't fly, yielding: >> ``` >> Error: In this GADT definition, the variance of some parameter >> cannot be checked >> ``` >>=20 >> I'm not wedded to using polymorphic variants here, but I have = essentially the same trouble using a hierarchy of class types (with = different sets of `unit` methods to induce the intended subtype = relation) to express the index lattice. Are there other options? >>=20 >> I also tried using trunk's injectivity annotations (`type +!_ exp =3D = ...`) on a lark since I'm not confident that I fully understand what = happens to the anonymous type variables for the rows in the polymorphic = variants. But that doesn't seem to change things. >>=20 >> Is this sort of use case something for which there are known = encodings? In a way I'm trying to benefit from some of the advantages of = polymorphic variants (subtyping) without the drawbacks such as weaker = exhaustiveness and less compact memory representation by keeping the = polymorphic variants in a phantom index. Is this approach doomed? >>=20 >> Cheers, Josh >>=20 >=20