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 F0CBC5D5 for ; Sat, 27 Feb 2021 10:45:08 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.81,210,1610406000"; d="scan'208";a="495205756" 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 11:45:07 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id C29D6E1D3B; Sat, 27 Feb 2021 11:45:07 +0100 (CET) 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 39052E1D37 for ; Sat, 27 Feb 2021 11:45:04 +0100 (CET) Authentication-Results: mail3-smtp-sop.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 IronPort-PHdr: =?us-ascii?q?9a23=3Ap/AdfRcUTTjyJcM9vpTtr2LJlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcu/bB7h7PlgxGXEQZ/co6odzbaP4uaxAydYvN6oizMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVr?= =?us-ascii?q?O+/7BpDdj9it1+C15pbffxhEiCCybL9vKBi6twHcutcZjYd+Kqs61wfErGZPd+?= =?us-ascii?q?lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLe?= =?us-ascii?q?TQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgz?= =?us-ascii?q?oBOjUk8m/Yl9ZwgbpVrhyhuRJx3o3ab46JO/VjfKzSc8gXRXZdUstLSyBNHpmx?= =?us-ascii?q?Y5UJAuEcPehYtY79p14WoBWnAQmjGuzvwSJPi3/x2a01zeshHBrB3AwjGtIOsX?= =?us-ascii?q?bUoM/yNKcIXuC41a/FxijMYP1Kwzny8pTIcgw/rvGWW7J9acXfxE0xGg7bgFud?= =?us-ascii?q?p4LoMi+b2OoCvGaW8/dsWOKghWAotg18rCSjy9kjh4TXiYwZ1F7J+DhkzYg6JN?= =?us-ascii?q?C2R0B2bN6iHZBNtC+aL5N7T8IjTm1ytis3zqcKtJChcCQX1ZgqyAbTZ+GGfoWG?= =?us-ascii?q?+B7uW+KcLS1miH55eb+znQi+/Va8xuD6S8K6ykxFrjBfndnJrn0N1wLc6syASv?= =?us-ascii?q?Zl+0euwzeP1wTO5u1eLkA5m7DXK4Y7zb4xjJofq1jMHijzmEnuja+WcFsr+vSw?= =?us-ascii?q?5unmY7jqvJGROotuhgzwKKgih9GzDOsgPggLRWeb+OC81LP5/U3+RbVHlvo2kq?= =?us-ascii?q?3Hv5DVPskboa25AwpU0oYh8Rq/CC2m0NsAkXkdMF1FYA6Hj5TuO1zWPP/3F/K/?= =?us-ascii?q?g1C1nDdvxvDGJaHhD47WLnnDlbfhZaxy51RdyAo119Bf5ohbBqsPIPLpCQfNs4?= =?us-ascii?q?nXBxUjMgGwhf3sCNhn25k2VmeGA6vfO6TX4nGS4ed6BO2Ba8dBvzLwJNAi5Pvv?= =?us-ascii?q?jzk+g1BLLvrh5ocedH3tRqcuGE6ee3e52o5QQ1dPhRI3SanRsHPHVDdSY3ioWK?= =?us-ascii?q?dlv2M8C4enD8HEXI//2eXdjhf+JYVfYyV9Mn7JCW3hLtzWXPQJaSDUJdVuwGRd?= =?us-ascii?q?COqRDrQ53BTrjzfUjrpqKu2Nq38dvJPnjZ56vKvLnBAoszdzCpbF3g=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AoAAAuIjpgmHIDJ0JiHQEBAQEJARIBB?= =?us-ascii?q?QUBQIE+BQELAYMgVwE4MY1FiFicSwsBAwENIBICBAEBhE0CgXoCHQcBBDMGDgI?= =?us-ascii?q?QAQEFAQEBAgEDAwQBEwEBAQEBAQEBCQsLBimFaA2COCKDawEEAScTPwUWWoNMA?= =?us-ascii?q?YJmIAGwZoEBM4pbgTgBjUImDw2BREOBEYJsLj6FDIJ9gisEggKBQIMGnW6bSzK?= =?us-ascii?q?DBoEqgTSGYZJSMYYanTy3G4FqgXtNMAg7gmkJRxkNjjiCDYwxMgExOAIGCgEBA?= =?us-ascii?q?wlYizsBAQ?= X-IPAS-Result: =?us-ascii?q?A0AoAAAuIjpgmHIDJ0JiHQEBAQEJARIBBQUBQIE+BQELAYM?= =?us-ascii?q?gVwE4MY1FiFicSwsBAwENIBICBAEBhE0CgXoCHQcBBDMGDgIQAQEFAQEBAgEDA?= =?us-ascii?q?wQBEwEBAQEBAQEBCQsLBimFaA2COCKDawEEAScTPwUWWoNMAYJmIAGwZoEBM4p?= =?us-ascii?q?bgTgBjUImDw2BREOBEYJsLj6FDIJ9gisEggKBQIMGnW6bSzKDBoEqgTSGYZJSM?= =?us-ascii?q?YYanTy3G4FqgXtNMAg7gmkJRxkNjjiCDYwxMgExOAIGCgEBAwlYizsBAQ?= X-IronPort-AV: E=Sophos;i="5.81,210,1610406000"; d="scan'208";a="374266237" X-MGA-submission: =?us-ascii?q?MDEbhWFjWoY0wSSiOfNktPyPUshlToNO7uvPPy?= =?us-ascii?q?ExRwyjAYt/LqnALhOGoRsjzzWgB2SV7+6iPNeeXuKtNTHzvtbGOjNzx7?= =?us-ascii?q?Fh7Env928htfpXCMcqFDy6oWgBD56q+XvIrrD9QJgvIs05uF1WDxeqYR?= =?us-ascii?q?Zo0IucW5dI902z2CQA+IDHUA=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 27 Feb 2021 11:45:02 +0100 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id BA4813FB8F2; Sat, 27 Feb 2021 05:44:59 -0500 (EST) Received: from Melchior.localnet (220.206.49.163.rev.vmobile.jp [163.49.206.220]) (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 BB763582CB0; Sat, 27 Feb 2021 05:44:58 -0500 (EST) Date: Sat, 27 Feb 2021 19:50:13 +0900 From: Oleg To: gabriel.scherer@gmail.com Cc: caml-list@inria.fr Message-ID: <20210227105013.GA2146@Melchior.localnet> Mail-Followup-To: Oleg , gabriel.scherer@gmail.com, 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] Breaking type abstraction of modules Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 18411 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: 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]