How can an OCaml module export a field defined in a dependent module?

Question

I have a decomposition where module A defines the type of structure and exports a field of this type, which is defined as a value in module B :

a.ml :

 type t = { x : int } let b = Ba 

b.ml :

 open A (* to avoid fully qualifying fields of a *) let a : t = { x = 1; } 

A circular dependency is excluded because B depends only on type declarations (not values) in A

a.mli :

 type t = { x : int } val b : t 

As far as I know, this should be kosher. But the compiler with these errors:

 File "a.ml", line 1, characters 0-1: Error: The implementation a.ml does not match the interface a.cmi: Values do not match: val b : At is not included in val b : t 

This is especially stupid, of course, because it is not clear which val b interpreted as having type t and having type At (and to which A is an interface definition or module definition - this applies).

I suppose that there is some secret rule (the lines “structural fields should indicate the full name of the module when the module does not open”, the semantics that every neocomit OCaml bites at some point), but I still do not understand .

Answer 1

Microscope modules are thinner than they appear

(If your eyes blur at some point, skip to the second section.)

Let's see what happens if you put everything in the same file. This should be possible, since individual computing units do not increase the power of the type system. (Note: use separate directories for this and for any test with a.* And b.* Files, otherwise the compiler will see compilation units A and B , which can be confusing.)

 module A = (struct type t = { x : int } let b = Ba end : sig type t = { x : int } val b : t end) module B = (struct let a : At = { Ax = 1 } end : sig val a : At end) 

Oh well, that won't work. Obviously, B is not defined here. We need to clarify the chain of dependencies: first define interface A , then interface B , then implementations of B and A

 module type Asig = sig type t = { x : int } type u = int val b : t end module B = (struct let a : Asig.t = { Asig.x = 1 } end : sig val a : Asig.t end) module A = (struct type t = { x : int } let b = Ba end : Asig) 

Oh no.

 File "d.ml", line 7, characters 12-18: Error: Unbound type constructor Asig.t 

You see, Asig is a signature. A signature is a specification of a module, and no more; in Okamla there is no calculation of signatures. You cannot reference signature fields. You can only refer to module fields. When you write At , this refers to a type named t module A

In Ocaml, this subtlety is quite rare. But you tried to stick out the corner of the tongue, and that is what is hiding there.

So what happens when there are two compilation units? A closer model is to see A as a functor that takes module B as an argument. The required signature for B is the one described in the b.mli interface b.mli . Similarly, B is a function that takes the module A whose signature is given in a.mli as an argument. Oh wait, this is a little more important: A appears in signature B , so interface B really defines a functor that takes A and creates B , so to speak.

 module type Asig = sig type t = { x : int } type u = int val b : t end module type Bsig = functor(A : Asig) -> sig val a : At end module B = (functor(A : Asig) -> (struct let a : At = { Ax = 1 } end) : Bsig) module A = functor(B : Bsig) -> (struct type t = { x : int } let b = Ba end : Asig) 

And here, when defining A , we are faced with a problem: we do not yet have A to pass the value of B as an argument. (Of course, the prohibition of recursive modules, but here we are trying to understand why we can not do without them.)

Determining the generative type is a side effect

The main gluing point is that type t = {x : int} is a generative type of definition. If this fragment appears twice in the program, two different types are defined. (Ocaml takes steps and forbids you to define two types with the same name in the same module, with the exception of the top level.)

In fact, as we saw above, type t = {x : int} in the module implementation is a generator type definition. This means "define a new type, called d , which is a record type with fields ...". The same syntax may appear in the interface of the module, but there it has a different meaning: there, this means that "the module defines the type t , which is the type of record ...".

Since the definition of a generic type creates two different types twice, the specific generic type that is defined by A cannot be fully described by the specification of module A (its signature). Therefore, any part of the program that uses this generative type really uses the implementation of A , and not just its specification .

When you move on to it by defining the generative type, this is a form of side effect. This side effect occurs during compilation or during the initialization of the program (the difference between the two appears only when you start working with functors, which I will not do here). Therefore, it is important to monitor when this side effect occurs: occurs when module A detected (compiled or loaded).

So, to put it more specifically: the definition of type type t = {x : int} in module A compiled into "let t type # 1729, a new type that is a record type with a field ...". (A new type means one that is different from any type that has ever been previously defined). Definition B defines A to be of type # 1729.

Since module B depends on module A , A must be loaded to B But implementation A explicitly uses implementation B These two are mutually recursive. The Ocaml error message is a bit confusing, but you really exceed the boundaries of the language.

Answer 2

(and for which A - interface definition or module definition - this applies).

A refers to the whole module A. With the usual assembly procedure, it refers to the implementation in a.ml, which is infringed by the signature in a.mli. But if you play tricks, moving cmi around and such - you are on your own :)

As far as I know, this should be kosher.

I personally qualify this problem as a circular dependency and remain valid against structuring the code in this way. IMHO causes more problems and dizziness than solving real problems. For instance. moving common types of definitions into type.ml and executing with them is what comes to mind first. What is your initial problem that leads to this structuring?