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:
Archived-At:
List-Archive:
> 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