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 CD2C25D5 for ; Tue, 6 Oct 2020 16:01:19 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.77,343,1596492000"; d="scan'208";a="471274699" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 06 Oct 2020 18:01:16 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 4AA49E0B49; Tue, 6 Oct 2020 18:01:16 +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 CE04EE00E5 for ; Tue, 6 Oct 2020 18:01:11 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=oleg@okmij.org; spf=Pass smtp.mailfrom=oleg@okmij.org; spf=None smtp.helo=postmaster@mail1.g3.pair.com IronPort-PHdr: =?us-ascii?q?9a23=3AU8XvVRQieCnrbp8/JHGvoL4W8tpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6yYRyN2/xhgRfzUJnB7Loc0qyK6v+mBTBLvM3JmUtBWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6?= =?us-ascii?q?OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRe7oR/eu8QZjodvKqg8wQbVr3VVfO?= =?us-ascii?q?hb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnY?= =?us-ascii?q?UAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhS?= =?us-ascii?q?waMTMy7WPZhdFqjK9DrhyvpwJxzZPXbo6aKPVxY6HSct0BSGpdQspcTTBNDp+m?= =?us-ascii?q?YocRCecKIOZWr5P6p1sLtRawHA2sC/3gyjRVgXL22qk63PouEQzd2wwgHNcOsH?= =?us-ascii?q?XWrNnvM6cSS++1wbDOwD7eYPxYxS3z55LUchA9v/6MR7RwfNLexEQrCg7Iilud?= =?us-ascii?q?p4P4Mj+Ly+gArXSW4u58WO+zl2IqpB18riWyysojloXEiYAYxFDL+yh2wIs7K8?= =?us-ascii?q?O0RVNlbNK6FpZbqi+UN4xzQsw4QmFovj43yroFuZ6+fSgKyo4rxxnFa/yIdYWD?= =?us-ascii?q?/xHtVP6JLDp5hX9pYryyihKo/UWu0OHwS9S43VlSoiZbj9XAqmoB2wHd58WEUP?= =?us-ascii?q?dx4Fut1DWV2w3S7uxJJ10/m7DBJJ472LEwk4IesUTdES/yn0X7lKqWeV8l+uis?= =?us-ascii?q?9ujreLrmq5GGO49skA7+M74ultajDuQ/NwgCR2mb+eKi273/5UD0QbRHguc4n6?= =?us-ascii?q?TdqpzXK94XqrOkDwJayooj7gywDzai0NQWh3kHK1dFdQqAj4jtJV7OL+v1DfC8?= =?us-ascii?q?g1SpkTdrxerKPrr7ApXCNnTDiqvufa5h605Azwo+1cxQ6IhRCrEFOf7zXk7xtM?= =?us-ascii?q?fEDhIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvOfGGZJUJtzblN/gl+/nu?= =?us-ascii?q?gGc3mV8FeqmpwYcXaHGmEfR8OEiYYHvsgtIaHmcQpAUyVu3qiFuYUT5SfXm+Ra?= =?us-ascii?q?w85itoQL6hWInZT4amh72amj+8AoFXa3puC1aWEH6ueZ/Xde0LbXe1JsJu2mgD?= =?us-ascii?q?UbWuY4gi0BCs8gjgxOw0faLv5iQEuMe7h5BO7OrJmERqrG0mP4Gmy2iIClpMsC?= =?us-ascii?q?YNTj4y0rp4pBUkmFCA1Kl6xftCGo4Kvq8bYkIBLZfZitdCJZXqQAuYJ4WOS1On?= =?us-ascii?q?QJOhGz5jFotske9LWF50HpCZtj6G3yeuBOZExbmCBZhttK2HmWD4Jtw7wHHDhv?= =?us-ascii?q?Es?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CfAQAMlHxfh3IDJ0JggQmEaVYBMSyNP?= =?us-ascii?q?4g5nCYLAQMBDSMKAgQBAYRKAoIHAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQo?= =?us-ascii?q?LCQgphWMMgjcigxoBAgIBJxM/BRZad4MLAYJcHwEPqEeBATOKWYE4jTEODYFAQ?= =?us-ascii?q?IERgmIuPoJFgkWCfYItBJxNmlMvgnGBHYEshjaRVjGEN4Ejm0eeA5VRgWuBek0?= =?us-ascii?q?wCDuCaQlHGQ2OOYhrhVEyATI3AgYKAQEDCViNcAEB?= X-IPAS-Result: =?us-ascii?q?A0CfAQAMlHxfh3IDJ0JggQmEaVYBMSyNP4g5nCYLAQMBDSM?= =?us-ascii?q?KAgQBAYRKAoIHAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQoLCQgphWMMgjcig?= =?us-ascii?q?xoBAgIBJxM/BRZad4MLAYJcHwEPqEeBATOKWYE4jTEODYFAQIERgmIuPoJFgkW?= =?us-ascii?q?CfYItBJxNmlMvgnGBHYEshjaRVjGEN4Ejm0eeA5VRgWuBek0wCDuCaQlHGQ2OO?= =?us-ascii?q?YhrhVEyATI3AgYKAQEDCViNcAEB?= X-IronPort-AV: E=Sophos;i="5.77,343,1596492000"; d="scan'208";a="361033143" X-MGA-submission: =?us-ascii?q?MDEt5Gk+lxqkxKm26lxBQc2aTnhUnQzaEZGzQu?= =?us-ascii?q?u0JmkzSP5NqiGYZQ7astCfYUoJZvMZOtZEbG8MKfw2KG/Gw46FXs3hfn?= =?us-ascii?q?EAlpZvUHLhKH8B2iHVtAZ71cCjgvS9onAlE4p0OebZswQgXmUhSXccrb?= =?us-ascii?q?ImrK8yb6ekWfNMmPCwhhKuMQ=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 06 Oct 2020 18:01:10 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 707C93FB50C; Tue, 6 Oct 2020 12:01:05 -0400 (EDT) Received: from Melchior.localnet (69.208.138.210.rev.vmobile.jp [210.138.208.69]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mail1.g3.pair.com (Postfix) with ESMTPSA id 4F35A584BD6; Tue, 6 Oct 2020 12:01:04 -0400 (EDT) Date: Wed, 7 Oct 2020 01:05:19 +0900 From: Oleg To: francois.pottier@inria.fr Cc: caml-list@inria.fr Message-ID: <20201006160519.GA2217@Melchior.localnet> Mail-Followup-To: Oleg , francois.pottier@inria.fr, caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <29c64a17-6bda-89eb-49c9-e986116d8e70@inria.fr> User-Agent: Mutt/1.10.1 (2018-07-13) Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 18257 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: > 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.