From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id AE9085D5 for ; Sun, 21 Jun 2020 16:10:39 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.75,263,1589234400"; d="scan'208";a="455844856" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 21 Jun 2020 18:10:38 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 70DC0E034C; Sun, 21 Jun 2020 18:10:38 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id A6A94E00CE for ; Sun, 21 Jun 2020 18:10:31 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=josh@berdine.net; spf=Pass smtp.mailfrom=josh@berdine.net; spf=Pass smtp.helo=postmaster@out4-smtp.messagingengine.com IronPort-PHdr: =?us-ascii?q?9a23=3AKiSglBVUjdffP9jGi1Bktd+S9Z/V8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbBGHt8tkgFKBZ4jH8fUM07OQ7/m9HzVQud3Q7jgrS99lb1c9k8?= =?us-ascii?q?IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBo?= =?us-ascii?q?KevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrQjdrNQajIh+Jqo+zhbEo2ZDdv?= =?us-ascii?q?hLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfM?= =?us-ascii?q?TQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklD?= =?us-ascii?q?sLOjgk+2zRl8d+jr9UoAi5qhJ/34Hab46aOud9cK3TY90UQnFMXtpIVyxEHo+8?= =?us-ascii?q?b5cDAugHMO1Fr4f9vVwOrR6mCAeoA+Pv0T9IjWLr0KIkyeQuDADG3Ao+ENkTt3?= =?us-ascii?q?nUrtL1NLwSUe2u16bH0y/DYO5X2Tf79ofEaBYhru+QXb9pd8fa1EYgGR/fgFqK?= =?us-ascii?q?tYzlIy2a1v4Ls2WD7+RtVv+jhm4npgxzoDWixMgih4fNi48UxF3I6Tt0zYU3KN?= =?us-ascii?q?C4R0B2Zd6qHZlfui2GOYV7Qc0vTnxotisnyrAKpZi2dzUJxpQ/3xPSav2Kf5KV?= =?us-ascii?q?7h7+SeqdOzh1iGh7dL+8nxq/8lasxvfiWsS0ylpGsylIn9nWunwT2RHf9s6KQe?= =?us-ascii?q?Zj80elxDaPzBzT5f9eIU4plKraKoAuz6YsmpcVrE/NBDX5mF/sg6+Tbkgk+van?= =?us-ascii?q?6+DgYrj+oZ+cKpN0hw7nPqQ1n8y/Hfw4PhILX2eF4uS8z6fs/UL4QLVMgf05jK?= =?us-ascii?q?/ZsJ/bJcQduKG1GRNa0oEm6xqnDjem1soXnWUfIV9EeR+LlZXlN0zTLPziAvqz?= =?us-ascii?q?mUqgnTRzy/DDJLLhA5HNLnbZkLfmeLZw80xcyA0ozdBf/J9bEa8OIOjuVU/wst?= =?us-ascii?q?zXEAU1MwqqzOb7ENl9zJ8RWXqTAq+FN6PfqUOH6fgqI+mIfYMVvDf9K+M55/P1?= =?us-ascii?q?ln84mVodfbGz0pcNaXC4GO5mI0SDbnb2jNcBCzRCgg1rR+XvjBiGUCVPLyK5Vq?= =?us-ascii?q?c4ozU6E56ODIHZR4nrjqbXjwmhGZgDRGddChimHG3kdoOJE6MObzmSCsVsiDAF?= =?us-ascii?q?U7XnTYI9g0L9/DTmwqZqe7KHshYTsojugYAsu7/j0Coq/DkxNPyzlnmXRjgvzG?= =?us-ascii?q?kFXTM32q05p0FhmA/ajPpIxsdAHNkW3MtnFwc3MZmHlr59FsyuHxnEYs/PTVu9?= =?us-ascii?q?WdypADc+Q9Q+wtkDJU16Hof710GR72+RG7YQ0oezKtkx+6PY0WL2Ip8mmXzLzq?= =?us-ascii?q?UgiVRgRMZTZzSr?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DEAgDJhe9ehxwEb0JmgQmEZlIBATAsh?= =?us-ascii?q?CSJAYt8mAsLAQMBDC8EAQGGcQIdBgEENBMCEAEBBQEBAQIBAwMEARMBAQEIDQk?= =?us-ascii?q?IKYViDII7IoM/BBkBATAINAImAl+DOYJ9BLZtfzODAQEBBYJJg2uBNwmBDiqMY?= =?us-ascii?q?xo+gUKBEScchxKDSjOCLbRXgmQEgQaYIh2BCY9sFY1xrCSDd4FqgXgzGggmCmU?= =?us-ascii?q?Bgj4+EhkNjjiDV4RZhX5AAQExNwIGAQcBAQMJkQEBAQ?= X-IPAS-Result: =?us-ascii?q?A0DEAgDJhe9ehxwEb0JmgQmEZlIBATAshCSJAYt8mAsLAQM?= =?us-ascii?q?BDC8EAQGGcQIdBgEENBMCEAEBBQEBAQIBAwMEARMBAQEIDQkIKYViDII7IoM/B?= =?us-ascii?q?BkBATAINAImAl+DOYJ9BLZtfzODAQEBBYJJg2uBNwmBDiqMYxo+gUKBEScchxK?= =?us-ascii?q?DSjOCLbRXgmQEgQaYIh2BCY9sFY1xrCSDd4FqgXgzGggmCmUBgj4+EhkNjjiDV?= =?us-ascii?q?4RZhX5AAQExNwIGAQcBAQMJkQEBAQ?= X-IronPort-AV: E=Sophos;i="5.75,263,1589234400"; d="scan'208";a="455844828" X-MGA-submission: =?us-ascii?q?MDGA3blF6U0+WSh7V0uVV2dHhCAnaV8TPeMVJA?= =?us-ascii?q?lDThY1+BH3l8h0Ci9R2Bd+OX93jYhZyX58TeeoBw+orVFR4pShc4ZLDX?= =?us-ascii?q?Ql86aRGfO3/yR/3thNfGYWGdHiM/XlIsYrdDDEuaKqtAN92nufOPZQKd?= =?us-ascii?q?2adXFJ6Kx/CRWBotxcSbw3Hw=3D=3D?= Received: from out4-smtp.messagingengine.com ([66.111.4.28]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 21 Jun 2020 18:10:30 +0200 Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id D42825C0EB5 for ; Sun, 21 Jun 2020 12:10:28 -0400 (EDT) Received: from mailfrontend1 ([10.202.2.162]) by compute2.internal (MEProxy); Sun, 21 Jun 2020 12:10:28 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=berdine.net; h= from:content-type:content-transfer-encoding:mime-version:subject :message-id:date:to; s=fm3; bh=DYm1GdiGPMn+XJi+IuEKFkw0g/c5z1+E2 bjDzfJ/21k=; b=Szo9Wc+sP9yfifYYKOWi6ooob7N1L9gX/ozrLvg5c/WsUmCO5 pNKZQsZmmcGOzBJxeIvBM9bs2fOy9s2eRgt04waVUAs0GMW0DteEcCwUkgUbUdCP HbMAThhwn5WvbC5YXYz4xtaPVLH+qfXgwzcNhYOqp/OuX/C8NtmJmRdzpbkCgt8v JKuirlW+v0MyzTKtJvl+UTSBapUADbgR8nMY1oswEUqB4ZwPenwjIpyoFz/aK93K Avjx6Y4ePJOMLbQRPpaqe3NA/llbH2aqQrjr2sgyWqJVFqKsIgFCrokzgl4GSnpH PxU4y+PcjH8v16Lg3mxUQVBnayQxURtyHC8QA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:message-id:mime-version:subject:to:x-me-proxy :x-me-proxy:x-me-sender:x-me-sender:x-sasl-enc; s=fm3; bh=DYm1Gd iGPMn+XJi+IuEKFkw0g/c5z1+E2bjDzfJ/21k=; b=T/sbWvO3OGblolsv7SPHej BJVpR9CVHQQiqNtajuhzBb/Fr3Pk2qkjwy3x7YNAULNK2omTNc45YU0iRsrmgrKH Ygf+lHH+yLt59BSjryDvE35/WcyC0m+dv9/XbHfzKwX8/gGj1x7HFwY41SoYfw6K twZyiWGwUmJ/Utf/S31DIPn/LSNOFaCm6urAmf8OGfrYLaJWBmKk8y9QjNe5h5WH C6Pr2LnVJ0QTmt9QTYHyx4f8KCEggjUd1daNOIHHV8bU/y2rBJY1Dt7U95fopzWI no3ff2fOd9VB4Ogw8zqYyYz4jZPZMlptdMlCdD+pkhjIGkCXRs3K0uEOZeHS2gBw == X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduhedrudektddgleelucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucenucfjughrpefhtgfgggfukfffvffosehtqhhmtd hhtdejnecuhfhrohhmpeflohhshhcuuegvrhguihhnvgcuoehjohhshhessggvrhguihhn vgdrnhgvtheqnecuggftrfgrthhtvghrnhephfekudehheejjeejgfefleeifedtveekje ehgfelhfejgedtffekfeeuhfeuhedtnecukfhppeekvddrvdehrddukeehrddvfedtnecu vehluhhsthgvrhfuihiivgeptdenucfrrghrrghmpehmrghilhhfrhhomhepjhhoshhhse gsvghrughinhgvrdhnvght 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 5DEA13280067 for ; Sun, 21 Jun 2020 12:10:28 -0400 (EDT) From: Josh Berdine Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.14\)) Message-Id: <452E9622-D117-43E6-A0B1-9B8272F3C5FE@berdine.net> Date: Sun, 21 Jun 2020 17:10:26 +0100 To: caml-list X-Mailer: Apple Mail (2.3445.104.14) Subject: [Caml-list] Subtyping of phantom GADT indices? Reply-To: Josh Berdine X-Loop: caml-list@inria.fr X-Sequence: 18178 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: I wonder if anyone has any suggestions on approaches to use GADTs with a = type parameter that is phantom and allows subtyping. (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.?) 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 ``` 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 ``` 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? 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. 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? Cheers, Josh