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 ESMTP id 931CF5D5 for ; Sun, 29 Apr 2018 10:39:08 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.49,342,1520895600"; d="scan'208";a="324954709" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 29 Apr 2018 12:39:06 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 2DA2D82451; Sun, 29 Apr 2018 12:39:06 +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 ECEA78240C for ; Sun, 29 Apr 2018 12:38:57 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mandrykin@ispras.ru; spf=Pass smtp.mailfrom=mandrykin@ispras.ru; spf=None smtp.helo=postmaster@smtp.ispras.ru IronPort-PHdr: =?us-ascii?q?9a23=3Air3L2BYJcwHOFKu8BTWoygv/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZrs66bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+?= =?us-ascii?q?RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPC?= =?us-ascii?q?TQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhz?= =?us-ascii?q?sGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7Ses4URXdaXsZJSSNOHp+8?= =?us-ascii?q?YYUID+oEJ+lYro/9rEYKoRaxAQSgAeXiwSJKiHDrx603y/kvHx/I3AIgHNwAvn?= =?us-ascii?q?rbo9r3O6gOXu6417XIwDfZYv9KxTvw5orFfxY8qv+MR7Jwds/RxFEoGQPEjVWQ?= =?us-ascii?q?qZbqPzKR1u8QtGaU9exgWv+1i28nqAFxoz6vzdorh4nMnI0VzE3L9T95wYY2JN?= =?us-ascii?q?24TlV2Yd+/EJtIrSGVLZB2Ttk4Q2F1oSs3zKANt5C8fCgP0psnxhjfZuSDc4iJ?= =?us-ascii?q?5BLjSemQIStmi3J+ZLK/hhCy8Ue6xu37TMm0305GritDktnWt3ACzQbf6sadSv?= =?us-ascii?q?dl8Ueh2CqP1wDO6u5fO0w0lK3bJ4Yuwr4xipoTsVnDETTslErqi6+Wc10o++iy?= =?us-ascii?q?5OTnZbXmoYWQOJNzigH7NKklh8+xAfwgPwUNUWWX4/mw2bLn8EHjXblHivk7nr?= =?us-ascii?q?PEvJ3eJMkWoLOyDRVP3YY58Rm/Ci+r0NQGknkDK1JIYAmHj431O1HWOvz4DOy/?= =?us-ascii?q?g0y2kDhx3PDKJKfhAojVInjClrfuY6p95lZfxQc919xT+p1ZB7UbLP7uXkL8sM?= =?us-ascii?q?bUAgI9PgG12+rnDc9y1oIaWWKBGK+ZN6bSvEeN5u01JemDeZUVuTb+K/gk4f7j?= =?us-ascii?q?ln45mUQFfamzx5QXc2q0Hu57I0mBe3rjns8BEXsWvgo5VOHllEeNUTtXZ3qrW6?= =?us-ascii?q?I85yo7CJ69AIfYRoGthaSB0z2hEp1XYGBGEFGMHm3ye4WKQfdfIB6Vd+18lHQl?= =?us-ascii?q?U7+8Rsd11wyo8gvzzrBrJ8Lb/yQZsdTo090jtMPJkhRn0D13D82c1ymoRmd4hH?= =?us-ascii?q?ILRjl+iKV2p0Bn21SC14B5mORCHMcV/e4fAVRyDoLV0+EvU4O6YQnGZNrcDQv/?= =?us-ascii?q?G4T0MXQKVts0huQ2TQN4EtSmgArE2nPzUb4Oj6aCH9ou7/CFhiSjF4NG03/DkZ?= =?us-ascii?q?IZoRw+WMIWbD+nnbZl/hOVHZObyxzExZbvTrwV2Wv2zEnGzWeKuxgGAhV1Tb2D?= =?us-ascii?q?XGsHfELN687ktBvP?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ApAwBcoOVa/8THlVNcGgEBAQEBAgEBA?= =?us-ascii?q?QEIAQEBASqDenoog2yIYI4PgQ+BQIUyjDaBZC6CHIItAoJnBwEENBQBAgEBAQE?= =?us-ascii?q?BAQEBAWscDII1JIJQAQUjBBE2CxALGAICCR0CAiEkEgYNBgIBAQ6EZQMZC6dYg?= =?us-ascii?q?WkzhFiCLAMKgSuCR4EJiSCBMoI6LoJPNwsCAoEYDoM4glQChg4IfCaEWGCKdiw?= =?us-ascii?q?IhWSFaoJ3BoFxhU4PQYRIhWqDUkZXhwgzIYFSTTJBDQ2CKQmCP4M0gT6BJoE8d?= =?us-ascii?q?IVBPDCOCYI3AQE?= X-IPAS-Result: =?us-ascii?q?A0ApAwBcoOVa/8THlVNcGgEBAQEBAgEBAQEIAQEBASqDeno?= =?us-ascii?q?og2yIYI4PgQ+BQIUyjDaBZC6CHIItAoJnBwEENBQBAgEBAQEBAQEBAWscDII1J?= =?us-ascii?q?IJQAQUjBBE2CxALGAICCR0CAiEkEgYNBgIBAQ6EZQMZC6dYgWkzhFiCLAMKgSu?= =?us-ascii?q?CR4EJiSCBMoI6LoJPNwsCAoEYDoM4glQChg4IfCaEWGCKdiwIhWSFaoJ3BoFxh?= =?us-ascii?q?U4PQYRIhWqDUkZXhwgzIYFSTTJBDQ2CKQmCP4M0gT6BJoE8dIVBPDCOCYI3AQE?= X-IronPort-AV: E=Sophos;i="5.49,342,1520895600"; d="scan'208";a="263682004" Received: from bran.ispras.ru (HELO smtp.ispras.ru) ([83.149.199.196]) by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Apr 2018 12:38:56 +0200 Received: from [10.10.2.183] (molnar.intra.ispras.ru [10.10.2.183]) by smtp.ispras.ru (Postfix) with ESMTP id B2C93203BF; Fri, 27 Apr 2018 13:40:17 +0300 (MSK) To: Jun Inoue Cc: Jacques Garrigue , Mailing List OCaml References: <30D1A366-BDE1-4D6A-9531-A21492C930CE@math.nagoya-u.ac.jp> From: Mikhail Mandrykin Message-ID: <589199fb-e544-0e54-d252-b09dea764fdb@ispras.ru> Date: Fri, 27 Apr 2018 13:40:17 +0300 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Content-Language: en-US Subject: Re: [Caml-list] Type That's Concrete From Within A Library Abstract From Without Reply-To: Mikhail Mandrykin X-Loop: caml-list@inria.fr X-Sequence: 16864 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: Hello, > $ cat > p.mli > module B : sig type t = A.t val x2 : t end It seems it's the ambiguity between the "outer" and "packed" module A. Shadowing the outer A in p.mli fixes it: $ cat > p.mli module A : sig type t end (* t is abstract *) module B : sig type t = A.t val x2 : t end $ ocamlc -c p.mli $ ocamlc -pack -o p.cmo a.cmo b.cmo On 27.04.2018 11:53, Jun Inoue wrote: > Hi Jacques, > > OCaml gives a type error if a public type in b.ml references a > non-trivial type in a.ml. Is there a way around this? > > $ cat > a.ml > type t = Foo of int > let x : t = Foo 3 > $ cat > b.ml > type t = A.t > let x2 = A.x > $ cat > p.mli > module B : sig type t = A.t val x2 : t end > $ ocamlc -for-pack P -c a.ml b.ml > $ ocamlc -c p.mli > $ ocamlc -pack -o p.cmo a.cmo b.cmo > File "_none_", line 1: > Error: The implementation (obtained by packing) > does not match the interface p.mli: > In module B: > Modules do not match: > sig type t = A.t val x2 : A.t end > is not included in > sig type t = A.t val x2 : t end > In module B: > Type declarations do not match: > type t = A.t > is not included in > type t = A.t > > > On Fri, Apr 27, 2018 at 3:05 PM, Jacques Garrigue > wrote: >> You can provide a mli for the -pack. >> Just compile it before. >> >> $ cat > a.ml >> type t = int >> let x : int = 3 >> $ cat > b.ml >> let x2 = A.x * A.x >> $ ocamlc -for-pack P a.ml b.ml >> $ cat > p.mli >> module A : sig type t val x : t end >> module B : sig val x2 : int end >> $ ocamlc -c p.mli >> $ ocamlc -pack -o p.cmo a.cmo b.cmo >> >> Now, if you use your library with only p.cmo and p.cmi available, you will >> only be able to access it through the interface you provided. >> >> Also, the method using module aliases can work too: you just have >> to use longer file names for the internal modules, to reduce the risk of >> conflicts. But this is more involved than using -pack with a mli. >> >> Jacques Garrigue >> >> On 2018/04/27 14:48, Jun Inoue wrote: >>> Hi Ivan, >>> >>> That's basically our current approach, but it doesn't solve the >>> namespace pollution problem. In your example, when someone installs a >>> file named b.cmi (whose interface is unrelated to your b.ml), the name >>> conflict prevents loading the std.cma file at all: >>> >>> $ ocaml >>> OCaml version 4.04.0 >>> >>> # #show B;; >>> module B : sig val foo : int end >>> # #load "std.cma";; >>> The files std.cma and b.cmi disagree over interface B >>> >>> So the technique makes B inaccessible but doesn't remove it from the >>> namespace. This is why we want to -pack things, because our analogue >>> of b.ml is named matrix.ml, and there's no other sensible name for it. >>> >>> This technique doesn't work with -pack because that option demands all >>> .cmi's, including b.cmi. I guess we could rename matrix.ml to >>> matrix_internal_dont_touch.ml, but we wanted to know if there's a >>> cleaner approach. I wish we could supply a .mli file to the product >>> of -pack, but that also doesn't work... >>> >>> On Fri, Apr 27, 2018 at 12:06 AM, Ivan Gotovchits wrote: >>>> Hi Jun, >>>> >>>> You can achieve this by implying an extra layer of indirection, i.e., by >>>> having two levels of interfaces. For example, >>>> >>>> * A.ml - implementation of module A >>>> * A.mli - private interface of module A >>>> * B.ml - implementation of module B that may rely on anything in A.mli >>>> * Std.ml - a set of modules that you would like to import, e.g., `module >>>> A = A`, `module B = B` >>>> * Std.mli - public interface specification >>>> >>>> >>>> Next, you deploy `std.cmxa` and `std.cmi` but keep `a.cmi` and `b.cmi` to >>>> yourself. This will prevent users from accessing your private modules A and >>>> B directly. (In oasis you can use PrivateModules stanza for this) >>>> >>>> Now you will have `Std.A` and `Std.B` that exposes as much as you want. Not >>>> sure whether it will work with the `-pack`, but you can use this approach >>>> instead of it. This is how we address the same issue in [BAP][1] >>>> >>>> Cheers, >>>> Ivan >>>> >>>> [1]: https://github.com/BinaryAnalysisPlatform/bap >>>> >>>> >>>> On Thu, Apr 26, 2018 at 10:18 AM, Jun Inoue wrote: >>>>> Dear list, >>>>> >>>>> Is there a way to make a type concrete inside a library, yet opaque to >>>>> library users, preferably in a way that works with -pack? This is a >>>>> nagging issue in our sundials package >>>>> (http://inria-parkas.github.io/sundialsml/). >>>>> >>>>> Basically, we have a type declared in one module of the library that >>>>> is pattern-matched upon in other modules, like: >>>>> >>>>> (* private.ml *) >>>>> type opaque_type = Foo | Bar >>>>> >>>>> (* public.ml *) >>>>> let f : opaque_type -> int = function >>>>> | Foo -> 0 >>>>> | Bar -> 1 >>>>> >>>>> There are a few constraints: >>>>> - We don't want users to be able to pattern-match on opaque_type. >>>>> - We need multiple modules in the library to pattern-match on >>>>> opaque-type (so moving opaque_typ e to public.ml is not an option). >>>>> - To avoid namespace pollution, we want to pack the whole library >>>>> (with ocamlc -pack) as a single Sundials module, so the user sees a >>>>> Sundials.Public module instead of just Public. >>>>> >>>>> Is this possible? Right now, we just collect public.cmo and >>>>> private.cmo into sundials.cma and throw away private.cmi. But this >>>>> doesn't work with packing: >>>>> >>>>> $ ocamlc -pack -o sundials.cmo private.cmo public.cmo >>>>> >>>>> demands that there be a private.cmi. >>>>> >>>>> -- >>>>> Jun Inoue >>>>> >>>>> -- >>>>> Caml-list mailing list. Subscription management and archives: >>>>> https://sympa.inria.fr/sympa/arc/caml-list >>>>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >>>>> Bug reports: http://caml.inria.fr/bin/caml-bugs >> >> > > -- Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru -- Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs