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 BAB305D5 for ; Sat, 27 Feb 2021 11:37:57 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.81,211,1610406000"; d="scan'208";a="495208562" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 27 Feb 2021 12:37:56 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 2D4B0E1D3D; Sat, 27 Feb 2021 12:37:56 +0100 (CET) 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 0A044E1D37 for ; Sat, 27 Feb 2021 12:37:52 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=leo@lpw25.net; spf=None smtp.mailfrom=leo@lpw25.net; spf=Pass smtp.helo=postmaster@out5-smtp.messagingengine.com IronPort-PHdr: =?us-ascii?q?9a23=3AU8WiGRP6ka4t2YOTTWMl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0LfX4rarrMEGX3/hxlliBBdydt6sVzbuM+Pi9EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQpFiCe5bL9oKBi6swrdutUWjIB/Nqs/1xzFr2dSde?= =?us-ascii?q?9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLY?= =?us-ascii?q?TQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgz?= =?us-ascii?q?oFOTEk6mHakst+g6xUrxyipRN/zYDaboGLOvRjYqzQZs8aSXZbU8pNTSFMGJ+w?= =?us-ascii?q?Yo0SBOQBJ+ZYqIz9qkMAoRW4GwasA/7kxT9Ihn/3wa01zeotGhzB0QwkAd0Ot2?= =?us-ascii?q?/ZrNHtNKYcT+y4zLPEzTPdYPNKwDrw7pXDfR89r/+WR71wbdbRxlc1FwPDllid?= =?us-ascii?q?poPoMT2L2+gTt2WW7+5tWOyrhmAptg18oTehytkyh4fGho8Yy03I+CdlzIs2Jd?= =?us-ascii?q?C1Skp2bNGmHZVQqiyXNo97T8U/SG9roCY30rwLtJ+hcCQX1Zgr2gTTZvOdf4SW?= =?us-ascii?q?5h/uUvuaLCl8hHJ4Y7K/mwi98VK9xO39V8i7zk5HojZDn9LRrH4CzQbT5dKCSv?= =?us-ascii?q?Zl/keuxzKP1wfL5+FDPEA0iarWJ4c6wr41ipoTqV7PHirol0Xtl6+ZbEok+umu?= =?us-ascii?q?6+TofLrmoJCcN45yig7gKKghhsu/AeEgPggPWWiU5/i82aXi8ED4WrlGk+A6nr?= =?us-ascii?q?TDvJ3VP8gXuKq0DxdQ0ok56ha/Czmm0M4fnXkCNF9FfAyIj4/yNlHKOPD5A+mz?= =?us-ascii?q?jlS2nDdt2f/GIqXtAo/RIXjbjLfhYbF95lZAxwUpyNBf44tYCrUAIPLoRk/8r8?= =?us-ascii?q?fYDx88Mwys2enrEtR91oUEWWKOGKCVKq3SsUXbrt4oduKFYYtQvDfmN9Ak4eTv?= =?us-ascii?q?hDk3gwwzZ66siNEzZXfwIfRnP0jTKS7oj9ApFX8V5Fd4SuH23g7RGQVPbmq/Cv?= =?us-ascii?q?pvrgowD5irWN+aG9KdxYeZ1SL+JaV4I2BLDlfXSCXvapnZHuwJdDrUJ8J6iTUL?= =?us-ascii?q?VL6uRoku1Bej8gT9zug+d7aGymgjrZvmkeNNyajLjxhrrG5wF9vHjieLQn0mxj?= =?us-ascii?q?pZFQ9z57h2pAlG8nnG1KF5h/JCEtkKvqFNShhgaNjawvAoU90=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DQBQAILjpghx0Eb0JihXlWAQE4MY1Fi?= =?us-ascii?q?CgwnEsLAQMBDSAUBAEBhE0CgXoCHgUCBDQTAhABAQUBAQECAQMDBAETAQEBAQs?= =?us-ascii?q?NCQgphWgNgjgig2oBAQEDAScZAQE4BAsLGC4sK4MJAYJmIbADgXUzgwQBAQaCQ?= =?us-ascii?q?IQ0XwmBOIhcgwOBZCYcggeBEScPgjYuPoo0ggZEfIMGuFeBFAgCgnyBHwKIHpJ?= =?us-ascii?q?VBQofo1a3G4FrgXp7CjsugjsJRxcCDY44gg2BSYJfgXqGAEEBAi84AgYKAQEDC?= =?us-ascii?q?YwTAQE?= X-IPAS-Result: =?us-ascii?q?A0DQBQAILjpghx0Eb0JihXlWAQE4MY1FiCgwnEsLAQMBDSA?= =?us-ascii?q?UBAEBhE0CgXoCHgUCBDQTAhABAQUBAQECAQMDBAETAQEBAQsNCQgphWgNgjgig?= =?us-ascii?q?2oBAQEDAScZAQE4BAsLGC4sK4MJAYJmIbADgXUzgwQBAQaCQIQ0XwmBOIhcgwO?= =?us-ascii?q?BZCYcggeBEScPgjYuPoo0ggZEfIMGuFeBFAgCgnyBHwKIHpJVBQofo1a3G4Frg?= =?us-ascii?q?Xp7CjsugjsJRxcCDY44gg2BSYJfgXqGAEEBAi84AgYKAQEDCYwTAQE?= X-IronPort-AV: E=Sophos;i="5.81,211,1610406000"; d="scan'208";a="495208543" X-MGA-submission: =?us-ascii?q?MDHzcG/qY0Ec//Mu3ToT1dYZgz+XVRVGKwdPpW?= =?us-ascii?q?Q7jIqAgBE+k1pMPPWhb5zKQ+qNjXVBkRdwwSidsq+Jb63BMFwiSl32nn?= =?us-ascii?q?l+ypKmM7qUXhfbOzeCpqeGUrdSzqMYL2z+hQYvkeT1Hqs0D3Lb05Kv9v?= =?us-ascii?q?Kjioqx/Ww8deCkmGM0V0D48A=3D=3D?= Received: from out5-smtp.messagingengine.com ([66.111.4.29]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 27 Feb 2021 12:37:51 +0100 Received: from compute4.internal (compute4.nyi.internal [10.202.2.44]) by mailout.nyi.internal (Postfix) with ESMTP id 6D6345C0090 for ; Sat, 27 Feb 2021 06:37:49 -0500 (EST) Received: from imap1 ([10.202.2.51]) by compute4.internal (MEProxy); Sat, 27 Feb 2021 06:37:49 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=lpw25.net; h= mime-version:message-id:in-reply-to:references:date:from:to :subject:content-type; s=mesmtp; bh=OxOSXrnfup+k9IMuBdfLCdKhqz+a NZ1PF118PJ+eiHk=; b=RjoLXSFtVFbnnDVVvW6F+rlBMUWdMd405Pvgti/SGeBS Imar+4IMseahncZjBaMzC+jT7LVCVh9f+EwJqd01ll6v47p4FzxkxUe701mNllNZ EigHmBM/SVLNwXTXnLs5ffBXoyOM1dQOsdUbHEFfQlWcpAm1soH82u9UmBs/OHc= DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=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=fm2; bh=OxOSXr nfup+k9IMuBdfLCdKhqz+aNZ1PF118PJ+eiHk=; b=fxOKXc1FfsClpBJX5LWUhw TWLANaN46SnIshFcVzIsPyCOoTX1+xH9jgoc1Anul6zRfgKDrgppE2fkhUtmGO+d MYrNyG0zYt8m3vgLLjYquEXlZ3+YLf1sU1p2qPD3sITPtOtVqNTMMX2YruyCCXSE DjszbKHxHn5e9k7pTQ+5GCpKtEBTU8CPsqVL8Xw5JjbKvWv1vH0vQj+qoqryxKVO gD7FkBfLY4uJqOR3s0fsrzdb6f0x8Sn+O7nPL2G1xYG6v2ra6uFzqHssJ+ss+xI+ nTkm4DiNwUEKEmFRROIKvYmU4T6cfkxd2Ckm+Q5dSXyIhAAC17RBVV8XmWNrqJAw == X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduledrleefgdeftdcutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecunecujfgurhepofgfggfkjghffffhvffutgesthdtre dtreertdenucfhrhhomhepfdfnvghoucghhhhithgvfdcuoehlvghosehlphifvdehrdhn vghtqeenucggtffrrghtthgvrhhnpeeggeffvedvleehleefleffudekgfdvvefgheeiud ejtdekheejleegjefhueeileenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhep mhgrihhlfhhrohhmpehlvghosehlphifvdehrdhnvght X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 14E66130005D; Sat, 27 Feb 2021 06:37:49 -0500 (EST) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.5.0-alpha0-141-gf094924a34-fm-20210210.001-gf094924a Mime-Version: 1.0 Message-Id: In-Reply-To: <20210227105013.GA2146@Melchior.localnet> References: <20210227105013.GA2146@Melchior.localnet> Date: Sat, 27 Feb 2021 11:37:27 +0000 From: "Leo White" To: caml-list@inria.fr Content-Type: text/plain Subject: Re: [Caml-list] Breaking type abstraction of modules Reply-To: "Leo White" X-Loop: caml-list@inria.fr X-Sequence: 18412 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: Hi Oleg, I don't really understand your unease here. Firstly, this isn't some unexpected aspect of extensible variants, it is the main reason that I proposed adding them to the language. Secondly, you can easily create similar behaviour without extensible variants. For example, here we do the same thing without extensibility (code not actually tested or even type-checked): type (_, _) eq = Refl : ('a, 'b) eq module Rep : sig type 'a t val int : int t val string : string t val destruct : 'a t -> 'b t -> ('a, 'b) eq option end = struct type 'a rep = | Int : int rep | String : int rep let int = Int let string = String let destruct (type a b) (a : a t) (b : b t) = match a, b with | Int, Int -> Some Refl | String, String -> Some Refl | _, _ -> None end let counter = ref 0 module AF() : sig type t (* Here, t is abstract *) val rep : t Rep.t val x : t end = struct type t = int (* Here, t is concrete int *) let rep = Rep.int let x = incr counter; !counter end module A1 = AF () module A2 = AF () let ar = ref [A1.x] let _ = match Rep.destruct A1.rep A2.rep with | Some Refl -> ar := A2.x :: !ar | _ -> assert false Extensible variants make these kinds of type representations much more useful, but they don't change the nature of what you can do. Regards, Leo On Sat, 27 Feb 2021, at 10:50 AM, Oleg wrote: > > Gabriel Scherer wrote: > > > Is this very different from exposing the GADT equality directly in the > > module interface? > > > > module A : sig > > type t (* abstract *) > > val reveals_abstraction : (int, t) eq (* or maybe not *) > > val x : t > > end > > I think it is different: if you are declaring reveals_abstraction > (that is, the witness of the type equality) in your _interface_, you are > effectively declaring to the users that "type t = int", no? > > Thinking about this more, I come across the following example that > better illustrates my unease. The example concerns type generativity, > and explicit promise by generative functors to create fresh, > incompatible types. It seems this promise has to come with some > conditions attached. > > Assuming the same preamble with teq as before, consider the following > code > > let counter = ref 0 > > module AF() : sig > type t (* Here, t is abstract *) > type _ trep += AT : t trep > val x : t > end = struct > type t = int (* Here, t is concrete int *) > type _ trep += AT : t trep > let x = incr counter; !counter > > let () = > let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y -> > match (x,y) with > | (AT,AT) -> Some Refl > | (AT,Int) -> Some Refl (* Since t = int, it type checks *) > | (Int,AT) -> Some Refl > | _ -> None > in teq_extend {teq=teq} > end > > Here, AF is a generative functor. The type t is defined > abstract. Hence each instantiation of AF should come with its own, > fresh and incompatible with anything else type t. (For the same of > example below, the value x is also made fresh). > > Here are the two instances of the functor. > > module A1 = AF () > module A2 = AF () > > Indeed, the types A1.t and A2.t are different: putting A1.x and A2.x > into the same list predictably fails. > > let _ = [A1.x; A2.x] > > Line 1, characters 15-19: > 1 | let _ = [A1.x; A2.x];; > ^^^^ > Error: This expression has type A2.t but an expression was expected of type > A1.t > > > But now it succeeds: > > let ar = ref [A1.x] > > let _ = match (teq A1.AT Int, teq A2.AT Int) with > | (Some Refl,Some Refl) -> ar := A2.x :: !ar > | _ -> assert false > > let _ = !ar > - : A1.t list = [; ] > > The list in ar really has A2.x and A1.x as elements, which we can confirm > as > > let _ = match teq A1.AT Int with > | Some Refl -> (!ar : int list) > | _ -> assert false > > - : int list = [2; 1] >