Re: [Caml-list] Type That's Concrete From Within A Library Abstract From Without

[Mikhail Mandrykin <mandrykin@ispras.ru>]

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
> <garrigue@math.nagoya-u.ac.jp> 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 <ivg@ieee.org> 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 <jun.lambda@gmail.com> 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