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 B088F5D5 for ; Tue, 6 Oct 2020 19:05:11 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.77,343,1596492000"; d="scan'208";a="471293609" 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:05:07 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 68B9BE0B5B; Tue, 6 Oct 2020 21:05:07 +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 03B46E00E5 for ; Tue, 6 Oct 2020 21:05:02 +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@out2-smtp.messagingengine.com IronPort-PHdr: =?us-ascii?q?9a23=3AdWJcNRYRrMYWbGBY7H8QvnH/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZrsi/bnLW6fgltlLVR4KTs6sC17OJ9fy8EjVZv96oizMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVr?= =?us-ascii?q?O+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6twrcu8YZjYd/N6o8ywbCr2dVde?= =?us-ascii?q?hR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/Y?= =?us-ascii?q?TQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhS?= =?us-ascii?q?EaPDM/7WrZiNF/jLhDrR29qBNx3o7ab4ObOvRxfa3dc80US21aU8ZNTixBB5+w?= =?us-ascii?q?b4sTA+YfO+tTsonzp0EJrRu7HQSiAOTvyiRIhnTrwKA1zf4hHhzH3AwmAd0FrX?= =?us-ascii?q?PZrNfyNKcJUeC417LHwivZb/xL2Df97pbHfgonof6SQbJ9aMzcwlQgGA3ZlFuf?= =?us-ascii?q?s5DlPy+L2eQXtWiW9/dsW+yxh2I7qgx8rDuiy8kjh4TNmo4Z117J+yplzIsxKt?= =?us-ascii?q?C1VFN3bN2gHZVQuCyXKYt4T94sTmxmuys0xKMLtJ+9cSMXxponwBvfZOaGc4iO?= =?us-ascii?q?+h/jU+WRITJ5hHJnYr6/gAyy8Uemx+bhVce0yE5HoytEn9XWq3wBygHf5tKIR/?= =?us-ascii?q?dn4Eus2C6D2gPN5u1eP0w5lbDXJ4Miz7MwjJYfr0rOEjPwlU7rkqKWclgk+vO0?= =?us-ascii?q?6+v5eLXou56cNo5qhQzmLqgjnNG0D/4iPQgURWeb/Pyx1L398k39R7VHlvo2kr?= =?us-ascii?q?TFsJzEPMgbvau5AxNN0oo57hawESym0M8CknkILVJFfh2HgJbvO1HBIfD4C+mw?= =?us-ascii?q?j06wnzdswvDKJrzhApPTIXjfiLrsfLdw51RBxAYu0NxT/Z1ZBqsfLP/yQkPxsc?= =?us-ascii?q?bXDh49Mwy62ebnD9B925scWWKIGa+ZMLjfvkSW6eI1PuaMZYkVtyjnJ/gj+fHu?= =?us-ascii?q?kWc1mUUBcqmxwZsXdHe4E+x6LEqDZHrshs4NEWMLvgolUOznk0aCUD5WZ3aqRa?= =?us-ascii?q?0w/DA7CIS8DYfCXI+hmrKB3D2jFJ1Mem9GEkyMEWvvd4icVfcMcCWSItN9kjwF?= =?us-ascii?q?S7ehUZQs1BCvtA//0LVnNPDb9jcZtZLlzth15vfcmQs89TxuXIyh1DSqS2x71j?= =?us-ascii?q?cPQzI59Kd8pE1/jFCZ3v4rreZfEIlx4OhJGi03L5LdyeEyX9L1QQLpdNqTRFeg?= =?us-ascii?q?T5OgDC1nHYF5+MMHf0soQ4bqtRvExSf/W+ZJxYzOP4Q99+fn51a0P9x0ki2U3q?= =?us-ascii?q?Q7g1ggT41JOHH03vcupTiWPJbAlgCir4jvcK0d2CDX82LaljiEsVtUUQh9F6PI?= =?us-ascii?q?QSJGPxaEnZHC/krHCoSWJ/EnPw9GkpfQLbZWMJjyiEleAvLuI8/XbGO3lGq2Ch?= =?us-ascii?q?eOy/WHa4+4Img=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DcAAAkv3xfhxoEb0JgHAEBAQEBAQcBA?= =?us-ascii?q?RIBAQQEAQFAgU+DGlYBATAsjT+IOoN6mCwLAQMBDSMMBAEBhEYCAgKCBwIeBgE?= =?us-ascii?q?ENBMCEAEBBQEBAQIBAwMEARMBAQEIDQkIKYVjDII3IoMZAQEBAQIBJxMGAQE3A?= =?us-ascii?q?QQLCxguVwYTG4MLAYJcIAQLp3V0gQEzgwEBAQWCTIM8gTkJgTiNMxs+gUKBESc?= =?us-ascii?q?cgh8uPoJFgXiDSoItt1OCcoESh22RaB+BFIMmjVoVjn6eBZFKhAeBa4F6MxoIJ?= =?us-ascii?q?go7KgGCPgk1EhkNjh8ag1eCX4F6O4VDQAEBMTcCBgoBAQMJjkMFAQE?= X-IPAS-Result: =?us-ascii?q?A0DcAAAkv3xfhxoEb0JgHAEBAQEBAQcBARIBAQQEAQFAgU+?= =?us-ascii?q?DGlYBATAsjT+IOoN6mCwLAQMBDSMMBAEBhEYCAgKCBwIeBgEENBMCEAEBBQEBA?= =?us-ascii?q?QIBAwMEARMBAQEIDQkIKYVjDII3IoMZAQEBAQIBJxMGAQE3AQQLCxguVwYTG4M?= =?us-ascii?q?LAYJcIAQLp3V0gQEzgwEBAQWCTIM8gTkJgTiNMxs+gUKBESccgh8uPoJFgXiDS?= =?us-ascii?q?oItt1OCcoESh22RaB+BFIMmjVoVjn6eBZFKhAeBa4F6MxoIJgo7KgGCPgk1Ehk?= =?us-ascii?q?Njh8ag1eCX4F6O4VDQAEBMTcCBgoBAQMJjkMFAQE?= X-IronPort-AV: E=Sophos;i="5.77,343,1596492000"; d="scan'208";a="471293577" X-MGA-submission: =?us-ascii?q?MDH1PFRl2NRGS9z+ZbAN2goGm5zjAojvadOxAo?= =?us-ascii?q?Wvl/lfSab0K+gfHdKejv+O5VnQkVKpTjkSMPlCFGavLnE8pbaKlLsYvR?= =?us-ascii?q?nUtQ++5pSG2FDHiHp2ZqJ83m8Mik9VNWCSd97UH7XbwFYEYKOswXVYwr?= =?us-ascii?q?LF55/jWyaZtGXdUiq3Ecic7Q=3D=3D?= Received: from out2-smtp.messagingengine.com ([66.111.4.26]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 06 Oct 2020 21:05:00 +0200 Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.nyi.internal (Postfix) with ESMTP id 3CE9C5C0165; Tue, 6 Oct 2020 15:04:58 -0400 (EDT) Received: from mailfrontend1 ([10.202.2.162]) by compute3.internal (MEProxy); Tue, 06 Oct 2020 15:04:58 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=berdine.net; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=fm1; bh=r OCGpIEqZ0dOqKdvMlx/7aoBZfnpqcQIkYp98M6Qbgc=; b=MfHAW5ckDJrnW9BAo 0W8ObAgp86FoGvHf9pdQ01SPnBVMWHH+N0Q+WJ7xD9PdtfD3fX8a0eH5RqoOv/RO Z4nGIeKZUQ0W/AJxrDOlxOg0xSE6OZyRgOSifq0KEggBry/0baF+8+g/fq2SJCpR eoGqmdGkKX2NXLYxA5KO8ukuBx/9f49FhO7ARYslwCdyU3TDw6lTq89/uAp/5zES 5IndBwRNTvzzpOFnQC1CY0FvSAGBtg653tYBxD1m9H5iglCAnBrUnX0YhORTB7TE 1aiQO+YvkK87XDBuBDcqFt1ZQmE0n/lgYJjoag+BwKW6cS+hLqAanjIyzEsIID5a yoGjA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc:content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-proxy:x-me-proxy:x-me-sender:x-me-sender :x-sasl-enc; s=fm1; bh=rOCGpIEqZ0dOqKdvMlx/7aoBZfnpqcQIkYp98M6Qb gc=; b=ZMvGIyHV56adXKBZb4W2AnhUsT8mOFsiXsWkZ9B44FZ9NpUj1q91rWJL1 1ZyzJW1YBhXOdvzMeyadbNPaW9NpqD8jtDcykXKURBkcxYlAj0SnuesmL5+EZWYe FWapf51Ward3E1RpvUMwd+q9I9iLftP96hOs11btd+qeS0o7Sf+jyswbC23werVo ZoX2y2nTkJBvJJZ5Wt8HkmHk69pVPNN2goPTDTv5+JerOBRqqmwfqR0K4VdhOS6W pjvB2burjcTPTD/BELJNWo85WoKh9Smux0iERB2g1Y6jzR25C+rzSGae0QOjbH6f 9CU4fhAYgXno2Dxt8t2hGHyWspXDA== X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedujedrgeeggddufedtucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucenucfjughrpegtggfuhfgjfffgkfhfvffosehtqh hmtdhhtddvnecuhfhrohhmpeflohhshhcuuegvrhguihhnvgcuoehjohhshhessggvrhgu ihhnvgdrnhgvtheqnecuggftrfgrthhtvghrnhepudffvddtieefkeefgeeltddufefgtd elgeetudeklefhgeevhfeufeefkeffveeinecuffhomhgrihhnpehokhhmihhjrdhorhhg necukfhppeekvddrvdehrddukeehrddvfedtnecuvehluhhsthgvrhfuihiivgeptdenuc frrghrrghmpehmrghilhhfrhhomhepjhhoshhhsegsvghrughinhgvrdhnvght 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 41FDD3280064; Tue, 6 Oct 2020 15:04:57 -0400 (EDT) Content-Type: text/plain; charset=us-ascii Mime-Version: 1.0 (Mac OS X Mail 13.4 \(3608.120.23.2.4\)) From: Josh Berdine In-Reply-To: <20201006160519.GA2217@Melchior.localnet> Date: Tue, 6 Oct 2020 20:04:56 +0100 Cc: francois.pottier@inria.fr, caml-list@inria.fr Content-Transfer-Encoding: quoted-printable Message-Id: References: <20201006160519.GA2217@Melchior.localnet> To: Oleg X-Mailer: Apple Mail (2.3608.120.23.2.4) Subject: Re: [Caml-list] Question on the covariance of a GADT (polymorphic Reply-To: Josh Berdine X-Loop: caml-list@inria.fr X-Sequence: 18259 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 Oct 6, 2020, at 5:05 PM, Oleg wrote: >=20 >> type 'a t =3D >> | Wine: [> `Wine ] t >> | Food: [> `Food ] t >> | Box : 'a t * 'a t -> 'a t >> | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t >>=20 >> 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. >>=20 >> 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.). >=20 > 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: >=20 > http://okmij.org/ftp/tagless-final/subtyping.ml >=20 > 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. >=20 > 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. Francois, your examples is way better than mine! :-) Apologies for dropping the ball before, I got busy and there was some = chaos going on. But Oleg, thank you very much for digging into this so thoroughly and = making such concrete suggestions! There are some points I'm unsure of. My understanding of `Reducer` is = that it is a way of implementing a particular (reduction) function on = expressions from this little language, where rather than the "initial" = approach of defining an explicit datatype for the expressions and then = reducing them, you use constructor functions that eagerly perform the = reduction, and extract the result with `observe`. What I'm unsure of is how this generalizes to additional functions on = expressions. For instance, suppose I also wanted to define a function = which computed the set of int literals that appear in the (unreduced) = expression? One possibility would seem to be to revise your second = solution (say) so that `'a Reducer.t` is `'a * int list` instead of = `'a`, and revise the constructor functions to compute this list of ints = eagerly. My working assumption is that which operation on the expression will be = performed isn't known at the time when they are constructed. Otherwise a = variant of the whole `Reducer` module could be defined for each = operation, each with its own `'a t` type defined as appropriate. More pressingly, I think, is what operations such as `map_ints : (int -> = int) -> 'a exp -> 'a exp` would look like. With an initial style = representation, this could be defined by traversing the abstract syntax = and rebuilding it with the updated `int`s. One approach would be to = change `Reducer.t` to a sort of abstract syntax, but this seems to me to = lead straight back to the original `'a exp` type. This is, as far as I = understand, coming up against the usual situation where the "initial" = representation is syntactic in nature and the "final" representation is = semantic. I don't know how much is known about handling such cases in = the final style though. Does it sound like I simply have not understood your solution? :-) Cheers, Josh > On Jun 27, 2020, at 4:36 PM, Oleg wrote: >=20 > Josh Berdine has posed a problem:=20 >> 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 ...=20 >> 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 >> ``` >=20 > We demonstrate three solutions to this problem. The first has an > imperfection, but is easier to explain. The second removes the > imperfection. The third one is verbose, but requires the least of > language features and can be implemented in SML or perhaps even > Java. All three solutions give the end user the same static > guarantees, statically preventing building of senseless > expressions. All three rely on the tagless-final style, in effect > viewing the problem as a language design problem -- designing a DSL > with subtyping. It has been my experience that the tagless-final, > algebraic point of view typically requires less fancy > typing. Incidentally, the third solution, of explicit coercions, can > be combined with GADTs and is hence the general solution to the posed > problem, showing how to do phantom index subtyping with GADTs. >=20 > Presenting all three solutions is too long for a message, so one > should look at the complete code with many comments: >=20 > http://okmij.org/ftp/tagless-final/subtyping.ml >=20 > Below is the outline of the first solution, the easiest to > explain. (The others just add slight variations; the main > example looks almost the same in all three). >=20 > We will think of the problem as a DSL with subtyping. > Let's define its syntax and the type system, as an OCaml signature: >=20 > module type exp =3D sig > type +'a t > val int : int -> [> `int] t > val float : float -> [> `float] t > val add : ([< `int | `float] as 'n) t -> 'n t -> [> `int | `float] = t > val string : string -> [> `string] t > end >=20 > The language expressions are indexed with a subset of tags `int, > `float, `string. The language has the obvious subtyping: [> `int] > can be weakened to [> `int | `float]. This weakening, and general = typechecking > of our DSL is performed by OCaml's type checker for us. Let's see an > example >=20 > module Ex1(I:exp) =3D struct > open I >=20 > (* We can put expressions of different sorts into the same list *) > let l1 =3D [int 1; float 2.0; add (add (int 3) (float 1.0)) (int 4)] > (* val l1 : [> `float | `int ] I.t list *) >=20 > let l2 =3D string "str" :: l1 > (* val l2 : [> `float | `int | `string ] I.t list *) >=20 > (* An attempt to build an invalid expression fails, with a good error = message: > let x =3D add (int 1) (string "s") > ^^^^^^^^^^^^ > Error: This expression has type [> `string ] t > but an expression was expected of type [< `float | `int > `int ] = t > The second variant type does not allow tag(s) `string > *) >=20 > (* We can define a function to sum up elements of a list of = expressions, > returning a single expression with addition > *) > let rec sum l =3D List.fold_left add (int 0) l > (* val sum : [ `float | `int ] I.t list -> [ `float | `int ] I.t *) >=20 > (* We can sum up l1 *) > let l1v =3D sum l1 > (* val l1v : [ `float | `int ] I.t *) >=20 > (* but, predictably, not l2 > let l2v =3D sum l2 > *) > end >=20 > Now, what we can do with the expressions? We can print/show them >=20 > module Show : (exp with type 'a t =3D string) =3D struct > type 'a t =3D string > ... elided ... > end >=20 > let _ =3D let module M =3D Ex1(Show) in M.l1 > (* - : string list =3D ["1"; "2."; "Add(Add(3,1.),4)"] *) >=20 > We can also reduce them. The following is the reducer -- although > in reality it does the normalization-by-evaluation (NBE) >=20 > A subset of expressions: values >=20 > module type vals =3D sig > type +'a t > val int : int -> [> `int] t > val float : float -> [> `float] t > val string : string -> [> `string] t > end >=20 > module Reducer(I:vals) :=20 > (sig include exp val observe : ([> `float | `int ] as 'a) t -> 'a = I.t end)=20 > =3D struct > type 'a t =3D Unk of 'a I.t | Int of int | Float of float > let observe =3D function > | Unk x -> x > | Int x -> I.int x > | Float x -> I.float x >=20 > let int x =3D Int x > let float x =3D Float x > let string x =3D Unk (I.string x) >=20 > let add x y =3D match (x,y) with > | (Int x, Int y) -> Int (x+y) > | (Float x, Float y) -> Float (x+.y) > | (Int x, Float y) | (Float y, Int x) -> Float (float_of_int x +. y) > (* This is the imperfection. We know that the case cannot happen, > but this is not clear from the type system. > We should stress that this imperfection does not compromise the = guarantees > offered to the end user, who never sees the internals of Reducer, > and can't even access them. > *) > | _ -> assert false > end >=20 > (* We can now evaluate exp to values. We need a way to show them = though. > Luckily, exp is a superset of values, and we already wrote the show > interpreter for exp > *) > let _ =3D let module I =3D Reducer(Show) in > let module M =3D Ex1(I) in List.map I.observe M.l1 > (* - : string list =3D ["1"; "2."; "8."] *) >=20 > The second solutions removes the imperfection in Reduce, making > Reduce.add total, by making the types more phantom. The third solution > does the obvious thing: implementing subtyping using explicit > coercions. In the given example, it doesn't add too much annoyance to > the user. It does however remove the reliance on variance and so > is applicable to GADTs in general. One can imagine more solutions > along the shown lines. >=20