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 42F7B5D5 for ; Wed, 7 Oct 2020 08:11:00 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.77,345,1596492000"; d="scan'208";a="471353747" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 07 Oct 2020 10:10:55 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 735D9E0B59; Wed, 7 Oct 2020 10:10:55 +0200 (CEST) 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 33777E00E5 for ; Wed, 7 Oct 2020 10:10:52 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dra-news@metastack.com; spf=Pass smtp.mailfrom=dra-news@metastack.com; spf=None smtp.helo=postmaster@outmail148100.authsmtp.co.uk IronPort-PHdr: =?us-ascii?q?9a23=3A6Zh7RBIssbk+JYO2M9mcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgXKv38rarrMEGX3/hxlliBBdydt6sbzbaL+Pm6AyQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTagY75+Nhq7oAXeusULn4duNLs6xwfUrHdPZ+?= =?us-ascii?q?lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRne?= =?us-ascii?q?VgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gy?= =?us-ascii?q?oBKjU38nzYitZogaxbvhyhqR5wzZPaboGSN/Rxcb/Sc9wdS2pdRctRSy5MAoyg?= =?us-ascii?q?Y4cRE+YNI+BVpJT9qVsUqhu+ABGhCO3hxDBSmH/23LA12Pk9HAHC2AwgBNUOsG?= =?us-ascii?q?zMrNn7KawfVv26zLPSwjnaafNZxzn86JPTfxAkv/6MQah/cdHNyUY1CwzFjU+c?= =?us-ascii?q?ppDiPzOQz+kAtXWQ4OV8W+y1kWEntx1xrSa1xscqkoTEmJ4Yx1TL+yhlzog7Jc?= =?us-ascii?q?C1RVBlbdK4DJddtz2WO5VoT80tXm1lpig3x7wGt5O1cyYG1pcqyhzCZ/GGcoWF?= =?us-ascii?q?4wzuWeCMKjl2g3Jlfaiwhxe08UW4ze38Vcy00FdIriZfldnMrH8N2wTU6sebUP?= =?us-ascii?q?R9+0Oh1SyI1wDJ5eFJJ10/m6nDK5M5w7M8iIAfvVnNEyPshUn7g6ybel859uS0?= =?us-ascii?q?9+jrerHrq5GGO4J3jgzyKLkil8KwDOgiLwQDUGiW9OKh37P550L5Wq9Fjvgun6?= =?us-ascii?q?nZrp/aIcMbq7a+Aw9IzoYj7gywDzai0NgFknQKL09JdA6bg4TzIV7OPez4Dfek?= =?us-ascii?q?g1SpjDdr3+rKMaHmApnXM3jDk6/tfbd760FC1Ao+1dFS64xOBr0cLv//QFL9ud?= =?us-ascii?q?PbAxMjLgC43/rrBM141owEWGKPBqGZMLnVsV+N/u8gPvOMa5UMtDb7Nfck6eXu?= =?us-ascii?q?gGQ8mVADYammx4AXaGyiEft6IEWVe2bjgtAEEWsSpAoxUPTqiEGeUT5Uf3u9Q7?= =?us-ascii?q?gz5jQ/CI6/CYfDR5utgKCa0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDwO?= =?us-ascii?q?TaKhRJM51RGyqA/6zKJqLuTM+i0fqZLjyNl16PPJlRwp9D10DsGd3HqXT25uhG?= =?us-ascii?q?8IRjk23Lp+oUNn0FuD37J40LRkEokZqNRNXwh1f9aIyOh3BPj1WQfAfJGOUlnw?= =?us-ascii?q?Bp3yDys4SNk2wsRIe0FhB9SvlDjC2TCrCvkbjerYKoYz9/eW83HvJso14nLCz6?= =?us-ascii?q?45lxNuFsdVPCigi7Fk3w3eG4fSj0ySlOChcqFKj32Fz3uK0Wfb5BIQawV3S6iQ?= =?us-ascii?q?BSlCNHuTlszw4wb5d5HrCbkjNVAZm8mfNq5Da9mw0QUfHK+lMcnCY3m0h3/2Dh?= =?us-ascii?q?HO27DeNNO2KVVY5z3UDQ0/qy5W5WyPbFVsAyq9qnnCBTdtU1noZhG0qLgsmDaA?= =?us-ascii?q?VkYxijqyQQhk3rux9AQSgKXBGfYewrsfpC4qqHN/G1Pvht8=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AFAQAKd31fl2SUDT5gHQEBAQEJARIBB?= =?us-ascii?q?QUBQIFPAoMYWDAsjT+IOYNDhl2FPYxJCwEDAQsBASUIAgQBAYRKAoIHAh0HAQQ?= =?us-ascii?q?0EwIQAQEFAQEBAgEDAwQBEwEBAQEBCBYGhgwMQxYBgV0igxkBAQEBAwgCHQESP?= =?us-ascii?q?w0DAgkNCy4ZIxsCBAESCwULgwsBglcpAQqnfnSBAQIxhDsBhhaBOAGNMoEUgQe?= =?us-ascii?q?BEYJiLj6CRYFOhiEEm32bUwqCaAOBEYdrkgmEOpxvkxiKcJUpAgQLAhWBa4F6c?= =?us-ascii?q?FCCaQkKLBEZDY45iGuFQ0IxAgEBATICBgoBAQMJW4hTgmWCNQEB?= X-IPAS-Result: =?us-ascii?q?A0AFAQAKd31fl2SUDT5gHQEBAQEJARIBBQUBQIFPAoMYWDA?= =?us-ascii?q?sjT+IOYNDhl2FPYxJCwEDAQsBASUIAgQBAYRKAoIHAh0HAQQ0EwIQAQEFAQEBA?= =?us-ascii?q?gEDAwQBEwEBAQEBCBYGhgwMQxYBgV0igxkBAQEBAwgCHQESPw0DAgkNCy4ZIxs?= =?us-ascii?q?CBAESCwULgwsBglcpAQqnfnSBAQIxhDsBhhaBOAGNMoEUgQeBEYJiLj6CRYFOh?= =?us-ascii?q?iEEm32bUwqCaAOBEYdrkgmEOpxvkxiKcJUpAgQLAhWBa4F6cFCCaQkKLBEZDY4?= =?us-ascii?q?5iGuFQ0IxAgEBATICBgoBAQMJW4hTgmWCNQEB?= X-IronPort-AV: E=Sophos;i="5.77,346,1596492000"; d="scan'208";a="361080767" X-MGA-submission: =?us-ascii?q?MDEAgn5aPE+2B2lBEXMQ0zo5riDYFv4+BwQWQm?= =?us-ascii?q?vRryRDtcn0/r1oSnlAE1PMXU1JlZTE6Uhg4hT6lVQ/nJZtkZo3Z/MsgL?= =?us-ascii?q?dxH0A4idkeR8adDLgzNiDq21YoloBg2TNQES72Z6wUJbk/ITP4ej5ur8?= =?us-ascii?q?S2ilccn4VEjXyomJAvPbsASQ=3D=3D?= Received: from outmail148100.authsmtp.co.uk ([62.13.148.100]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 07 Oct 2020 10:10:51 +0200 Received: from punt19.authsmtp.com (punt19.authsmtp.com [62.13.128.203]) by punt17.authsmtp.com. (8.15.2/8.15.2) with ESMTP id 0978Ao9V088380; Wed, 7 Oct 2020 09:10:50 +0100 (BST) (envelope-from dra-news@metastack.com) Received: from mail-c233.authsmtp.com (mail-c233.authsmtp.com [62.13.128.233]) by punt19.authsmtp.com. (8.15.2/8.15.2) with ESMTP id 0978AobQ035418; Wed, 7 Oct 2020 09:10:50 +0100 (BST) (envelope-from dra-news@metastack.com) Received: from romulus.metastack.com (cust145-dsl93-89-134.idnet.net [93.89.134.145]) (authenticated bits=0) by mail.authsmtp.com (8.15.2/8.15.2) with ESMTPSA id 0978Ama7012821 (version=TLSv1 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Wed, 7 Oct 2020 09:10:49 +0100 (BST) (envelope-from dra-news@metastack.com) Received: from Libera ([172.16.0.125]) (authenticated bits=0) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id 0978AmIi025066; Wed, 7 Oct 2020 09:10:48 +0100 From: "David Allsopp" To: "'Oleg'" , Cc: References: <29c64a17-6bda-89eb-49c9-e986116d8e70@inria.fr> <20201006160519.GA2217@Melchior.localnet> In-Reply-To: <20201006160519.GA2217@Melchior.localnet> Date: Wed, 7 Oct 2020 09:10:53 +0100 Organization: MetaStack Solutions Ltd. Message-ID: <000001d69c81$60341ab0$209c5010$@metastack.com> MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Mailer: Microsoft Outlook 16.0 Thread-Index: AQHWm/n1b4kMJrEQGUq+rgH2vtgaqqmLyq6w Content-Language: en-gb X-Scanned-By: MIMEDefang 2.65 on 62.31.77.26 X-Server-Quench: 9c45f4ed-0874-11eb-80b4-84349711df28 X-AuthReport-Spam: If SPAM / abuse - report it at: http://www.authsmtp.com/abuse X-AuthRoute: OCd1ZAARAlZZVg1f DC4bFwdFRBksPQFF ChxFJgxfNl8UURhQ KkJXbgESJgVDAnZS R3kJW1ZUQF14U2J1 YQ5YIwxefEJHQQRp VFZIRldNFgB3AFIB DxkWI0QjcAVHenZy ZAhqW3BTEk0pcUMr RhsACG0OYmN9aWFK Al1Qd1FQbQtOfRtM bVF+ACUPaStlE3Bw LCQ6OjR0OTRENBEd exwANk4TRkBDGTh0 WxAPVT4oA0QfRiw1 JBFuLVBUFQ4+G2kO eRs5XlYJNhgIEg1f FCkA X-Authentic-SMTP: 61633634383431.1021:7600 X-AuthFastPath: 0 (Was 255) X-AuthVirus-Status: No virus detected - but ensure you scan with your own anti-virus system. Subject: RE: [Caml-list] Question on the covariance of a GADT (polymorphic Reply-To: "David Allsopp" X-Loop: caml-list@inria.fr X-Sequence: 18263 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: Oleg wrote: > > type 'a t = > > | Wine: [> `Wine ] t > > | Food: [> `Food ] t > > | Box : 'a t * 'a t -> 'a t > > | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t > > > > In this definition, the type parameter 'a is a phantom parameter. It > > is not used to describe the type of a value; it is used only to > > restrict the set of values of type "t" that can be constructed. > > > > The goal here is to allow storing wine and food (and boxes > > containing boxes containing wine and food) in a fridge, but forbid > > storing a fridge in a fridge (or a fridge in a box in a fridge, etc.). > > This is indeed a very `popular' problem. On June 21 this year Josh > Berdine posed almost the same question (without wine and food, alas). > On 28 June 2020 I sent the reply with three solutions. Perhaps it > would be easier to point to the code, which also has many comments and > explanations: > > http://okmij.org/ftp/tagless-final/subtyping.ml > > The gist of the first two solutions is to exploit the fact that > tagless- final is sort of isomorphic to GADTs. That is, lots of things > that can be done with GADTs can be done without (or with GADTs hidden > away). That hiding has benefit of no longer bringing the problems with > variance. No GADTs (at least, not in the part facing the user), no > variance problems, at least, not for the end user. The library author > may use regular ADT, which are also non-problematic. A regular ADT > doesn't have the same typing guarantees -- but the typing is enforced > by the signature (at the module level), so there is no loss. > > I was going to write an article for my web site explaining this and a > few earlier answers to the similar problems. Maybe I will eventually > get to it. It is indeed popular - as are your historic answers, too :) https://inbox.ocaml.org/caml-list/20130705102138.98516.qmail@www1.g3.pair.co m/ --dra