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 sympa.inria.fr (Postfix) with ESMTPS id 17891E0B5D for ; Wed, 7 Oct 2020 15:13:23 +0200 (CEST) Authentication-Results: mail2-smtp-roc.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 Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of oleg@okmij.org) identity=pra; client-ip=66.39.3.114; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of oleg@okmij.org designates 66.39.3.114 as permitted sender) identity=mailfrom; client-ip=66.39.3.114; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail1.g3.pair.com) identity=helo; client-ip=66.39.3.114; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="postmaster@mail1.g3.pair.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AkDznFhCFAadezthuWybCUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPT+r8bcNUDSrc9gkEXOFd2Cra4d1KyK7eu+AyQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTagY75+Nhq7oATeusQXn4dpN7o8xAbOrnZUYe?= =?us-ascii?q?pd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbY?= =?us-ascii?q?VguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhS?= =?us-ascii?q?waNTA27XvXh9R+gqxbvhyvuh9xzIHIb46INvVxcLjQfc8GSWdbQspdSzZMDp26?= =?us-ascii?q?YoASD+QBJ+FYr4zlqlUXqRuxGwasD/7oxz9Pgn/5w6I63v8mEQHF2QwgHtAOvG?= =?us-ascii?q?7TrNXvO6cfSOa4x7THwjvfdf1Zwyv96JTWfRA7p/GBRb19fM7MxEQrGQ7LgUid?= =?us-ascii?q?pZL4Mz6LyukAt3SW4vZ8We+gl2Mrthx9rzezysojiITHho0bx1/E+Ct33oo4OM?= =?us-ascii?q?O1RFB9bNW5HpVQsCSaOJF3QsMkW2xovyU6yrgHuZ65ZiQKz44nxxHZZveacIaI?= =?us-ascii?q?+gruWeeQLDtiin9ofKizihio/US91+HxWdG43EhXoiZZiNXAq34A2h/J5sSaSP?= =?us-ascii?q?Zw/V2t1DiN2g3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLunUX5lq6WdkE59uSy?= =?us-ascii?q?5OTqbK/qpoeGOI91kAHyKLghmsu6AeggMwgOWXaU+fik2bDi/ED1WrtHg/ksnq?= =?us-ascii?q?TXqpzWONkXq6GhDw9QyIkj6hK/Dzm80NQfmHkKNFVFeBaZgIjmIFzOJ/P4DfK+?= =?us-ascii?q?g1SuijtrwOrGPrL5DpXXMnfDiKvhfap660NE1AU819Vf55ZNBrEFIfLzQVPxuc?= =?us-ascii?q?fDDh45Ngy02/zoBM981oMYQ2KPA7WWPLncsV+S/ugvOfWDZJcJuDbhLPgo//Du?= =?us-ascii?q?jWc+mV8BYamp3IUYaGqjE/VnIkWZZGHjgs0bHmsQvwo+SvbqiFyYXjJJaXayRf?= =?us-ascii?q?F02jZuBpivC4zER5vrmLudwCa2BLVXYHpHAxaCCyTGbYKBDtAIZS3adshlnzMs?= =?us-ascii?q?UrukSo1n0guh4lypg4F7J/bZr3VL/ano08J4srWKxEMCsAdsBsHY6FmjCmR9n2?= =?us-ascii?q?cGXTgzhfktpk94y1XF1rJ30aUBSI5joshRWwJ/Dqbyiux3D9erC1DEd9aNERCp?= =?us-ascii?q?GZO+CDArCNk2xo1WOhovK5CZlhnGmhGSLfoNjbXSXc4z8afd3T72Pckvk3s=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AUAQBtvn1fh3IDJ0JggQmEaVYBMSyNP?= =?us-ascii?q?4g7nCYLAQMBDSMKAgQBAYRKAoIHAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQo?= =?us-ascii?q?LCQgphWMMgjcigxoBAgIBOi4RBRZad4MLAYJcHwEPqUiBNIpigTiNMw4NgUBAg?= =?us-ascii?q?RGCYi4+gkUXA4Irgn2CLQScVJpVL4JygR2BLIY3kVgxhDyBJJtNngqVU4FrgXp?= =?us-ascii?q?NMAg7gmkJRxkNjjmIa4VRMgEyNwIGCgEBAwlYjXABAQ?= X-IPAS-Result: =?us-ascii?q?A0AUAQBtvn1fh3IDJ0JggQmEaVYBMSyNP4g7nCYLAQMBDSM?= =?us-ascii?q?KAgQBAYRKAoIHAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQoLCQgphWMMgjcig?= =?us-ascii?q?xoBAgIBOi4RBRZad4MLAYJcHwEPqUiBNIpigTiNMw4NgUBAgRGCYi4+gkUXA4I?= =?us-ascii?q?rgn2CLQScVJpVL4JygR2BLIY3kVgxhDyBJJtNngqVU4FrgXpNMAg7gmkJRxkNj?= =?us-ascii?q?jmIa4VRMgEyNwIGCgEBAwlYjXABAQ?= X-IronPort-AV: E=Sophos;i="5.77,346,1596492000"; d="scan'208";a="471423564" X-MGA-submission: =?us-ascii?q?MDHnSFF49TmSYAwAj7vO1pambd7k86ECDSzzKw?= =?us-ascii?q?RHa+ERyy2+T7rhGJ7x8No9SAwacfHS/AhX7mc4LoAZh9UliGPjj0jtne?= =?us-ascii?q?9YiB/Dw60efpUEK4vpqQfXvsLrj/SlWlRgUresaCl+j38A4YqMqEZVhx?= =?us-ascii?q?puW3/vuZLkRVVrxIJaAmHGiQ=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 07 Oct 2020 15:13:20 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id E2BAF3FBAA6; Wed, 7 Oct 2020 09:13:17 -0400 (EDT) Received: from Melchior.localnet (37.178.138.210.rev.vmobile.jp [210.138.178.37]) (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 C9CFC5835FB; Wed, 7 Oct 2020 09:13:16 -0400 (EDT) Date: Wed, 7 Oct 2020 22:17:32 +0900 From: Oleg To: francois.pottier@inria.fr Cc: caml-list@inria.fr Message-ID: <20201007131732.GA4915@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: User-Agent: Mutt/1.10.1 (2018-07-13) Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic > As far as I understand Oleg's solutions, they all boil down to the > same idea, which I have considered, but is only half satisfactory: > that is, to publish a covariant abstract type +'a t which internally > is implemented as an abbreviation for an unparameterized type u. (See > the food/wine/fridge example, rewritten in this style, below.) Good summary! > The reason why this solution is only half satisfactory is that inside the > abstraction barrier, we have an unparameterized type u that does not express > the desired data invariant, so we cannot exploit the invariant to prove that > certain branches in the code are dead. Indeed. That was the `imperfection' that I have referred to in my message. I have two comments: first, there is the second solution, which does exploit the invariant. Second, there may be more than one abstraction barrier... That is, many implementations of the wine_food signature may be in terms of some `more basic' signature -- or just the same signature, if we are talking about term transformations (as I have just replied to Josh Berdine). Eventually we have to implement the `most basic signature', and indeed we have to drop the indices and fall into the `untyped' universe, so to speak. One hopes though that this `security kernel' is really `most basic' and its operations are few and primitive, so the correctness could be relatively easily ascertained. > Also, the user cannot perform case analysis, since the type 'a t is > abstract. This is not a problem for me, but could be a problem in > other situations. When I first mentioned tagless-final, in passing at a some conference in Oxford a decade ago, an old Oxford professor (one of fathers of SML) exclaimed: ``Isn't it bloody obvious that you cannot do pattern-matching in this style!?''. I liked his phrase. Now I like to say that pattern-matching in tagless-final style is not bloody, is not obvious and is not impossible. That it is always possible was proven by Boehm and Berarducci (their proof was one inspiration for the development of Coq, as I heard). http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html Although their general method works always, often one may design simpler methods for particular pattern-matching tasks.