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 CDD1B5D5 for ; Tue, 6 Oct 2020 19:19:03 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.77,343,1596492000"; d="scan'208";a="471294572" 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 21:18:51 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id DAD26E0B5D; Tue, 6 Oct 2020 21:18:51 +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 D2621E00E5 for ; Tue, 6 Oct 2020 21:18:45 +0200 (CEST) X-IronPort-AV: E=Sophos;i="5.77,343,1596492000"; d="scan'208";a="361044518" Received: from 91-175-127-215.subs.proxad.net (HELO MacBook-Pro-5.local) ([91.175.127.215]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 06 Oct 2020 21:18:45 +0200 To: Josh Berdine , Oleg Cc: caml-list@inria.fr References: <20201006160519.GA2217@Melchior.localnet> From: =?UTF-8?Q?Fran=c3=a7ois_Pottier?= Message-ID: Date: Tue, 6 Oct 2020 21:18:44 +0200 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:68.0) Gecko/20100101 Thunderbird/68.11.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: fr Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic variants involved) Reply-To: =?UTF-8?Q?Fran=c3=a7ois_Pottier?= X-Loop: caml-list@inria.fr X-Sequence: 18260 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: On 06/10/2020 at 21:04, Josh Berdine wrote: > Francois, your examples is way better than mine!:-) Thanks :-) 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.) As far as the user is concerned, this works: the relaxed value restriction works, so in my example, "meat" receives a polymorphic type, and I am happy. 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. 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. Certainly, this is better than nothing, so I may end up adopting this approach (thanks again Oleg!). I am still curious, though, to know why my original type +'a t is not recognized as covariant by the OCaml type-checker... -- François Pottier francois.pottier@inria.fr http://cambium.inria.fr/~fpottier/ module T : sig type +'a t val wine: [> `Wine ] t val food: [> `Food ] t val box: 'a t * 'a t -> 'a t val fridge: [< `Wine | `Food ] t -> [> `Fridge ] t end = struct type u = | Wine: u | Food: u | Box : u * u -> u | Fridge: u -> u type 'a t = u let wine = Wine let food = Food let box (t1, t2) = Box (t1, t2) let fridge t = Fridge t end open T let food() = food let meat = food() (* the relaxed value restriction works *) let _ = box(meat, fridge wine) (* place the meat beside a fridge *) let _ = fridge meat (* meat can still be put into fridge *)