I’m probably misunderstanding here but trying out recursive modules
for the first time to overcome forward-declaration amongst a set of module files,
I think there’s a limitation.
in order to specify a functor one has to supply a signature thusly:
in file n.ml ->
module F ( M : sig … end ) =
struct
…
end
and in file M ->
module F ( N : sig … end ) =
…
struct
end
what if the signature’s themselves make reference to the other’s module content, such as the return types of functions?
a solution to this (for the example of function return types) would be to separate
out and pre-declare any such types themselves (make into a file ‘included’ by the client modules) but this is getting ugly.
module type msig= functor (N: sig end) -> sig type t val v : t end
module type s= sig type t val v : t end
module type fsig = functor (M: s) -> sig val f: int->M.t end
module rec M : fs =
functor (N: sig end) ->
struct
type t=int
let v=1
end
and F : fsig =
functor (M: s) -> struct
let f _= M.v
end
and M' : s = M (F')
and F' : sig val f:int->M'.t end = F (M')
this compiles. it shows that one can take a module as a parameter, and define a function
that returns a type defined by that module parameter. great.
now consider that the signature of M’ is declared previously.
but that the signature of F’ is inline.
that’s because there is no way to define the latter otherwise.
so if one’s interfaces don’t make use of any types coming in through module parameters
all well and good: the final tying together of functors into modules can be done with
separately written interface specifications.
but if one has a interface/signature dependent upon the functor parameters then
one is forced to recreate the signature, in it’s entirety, inline as above.
what I think is desirable is the following modification (2nd line pseudocode) to the above code:
and F' : fsig' = F (M')
and type fsig' = fsig (M')
… specializing a parameterized (functor) signature into a concrete one.
this would render it unnecessary to reproduce a signature, one necessarily already existing when the relevant functor is put in a separate file.
this doesn’t look to me to be a case of violating typing considerations but I’m no expert.
I haven’t worked through your example, but one thing to note is that for
modules which consist of only types, you can recursively define them to
be themselves:
module rec ...
and S : sig
type t = ...
end = S
This trick might provide a way to accomplish what you mean with and type ...
could you elaborate on the ‘t = …’ ?
I’m not catching your drift.
if it clarifies matters, I’m trying to relate the types exported by a
module , from a functor
argument module, to those in a signature, but since the signature
itself is of a functor, to make
it concrete it ought to be applied to a module signature just like a
functor applied to a module.
The usual way to parameterise a signature is to add an abstract type and use with type to constrain it. A simple example:
module type FOO = sig
type t
val zero : t
end
module A : FOO with type t = int = struct
type t = int
let zero = 0
end
module B : FOO with type t = float = struct
type t = float
let zero = 0.0
end
This is probably how you would avoid the signature duplication that you mention, if there were no other difficulties. However, there are restrictions on module rec which will prevent simply using this to tie the knot between mutually referring modules. An example:
module type ATy = sig
type b_t
type t
val zero : t
val consume_b : b_t -> unit
end
module type BTy = sig
type a_t
type t
val zero : t
val consume_a : a_t -> unit
end
module A (B : BTy) = struct
type b_t = B.t
type t = int
let zero = 0
let consume_b _ = ()
end
module B (A : ATy) = struct
type a_t = A.t
type t = float
let zero = 0.0
let consume_a _ = ()
end
module rec X : ATy with type b_t = Y.t = A (Y)
and Y : BTy with type a_t = X.t = B (X)
let _ = X.consume_b Y.zero
let _ = Y.consume_a X.zero
This looks reasonable enough, but the compiler will reject it with
Error: Cannot safely evaluate the definition
of the recursively-defined module X
This is due to module rec raising issues of order of evaluation. In order to avoid the difficulties restrictions have been placed on what kind of terms can go on the right hand side of module rec bindings, much like they have with let rec.
The standard advice in this situation is to adjust your design to not need module rec. That can be quite annoying indeed.
First, it would be far easier to keep recursive modules in the same file, at least until you are more familiar with the module system. It is often better to only use module rec with tightly coupled small modules.
Second, generally the result module type ( combined with some judicious substitutions and supplementary types) is more useful that the whole functor type when dealing with functor. For instance, what you wanted to achieve was probably:
module type empty = sig end
module type s= sig type t val v : t end
module type f = sig type r val f: int-> r end
module Make_M: empty -> s with type t = int =
functor(_:empty) -> struct
type t=int
let v=1
end
module Make_F: functor(M:s) -> f with type r := M.t =
functor(M:s) ->
struct
let f _ = M.v
end
module rec M : s with type t = int = Make_M(F)
and F : f with type r := M.t = Make_F(M)
yes that did it.
I think an uneducated but natural expectation is that the scope of (Y:y with…) should have no access to (X:x). Does the scope extend to functor arguments that might come
after (Y:y with …) as well as before? (I re-ordered my functor parameters before imagining this question)
I started out using the := sig substitution and spent hours trying to make sense of the
error messages coming from a 5-way recursive functor application and finally tried
changing := to = in the 5-way and within the modules themselves and it went through.
great relief.
so I suppose I just don’t understand the sig substitution experimental feature!
the example below produces the ‘is required but not provided’ error but unfortunately a bit
more which my code didn’t. so perhaps it is not representative of the problem, but anyway:
module type f=sig type z end
module type g=sig type t end
module F (G: g) : f with type z:=G.t =
struct
type z=G.t
end
module G (F: f) =
struct
type t=F.z
end
module rec Fmod : f with type z:=Gmod.t = F(Gmod)
and Gmod : g = G (Fmod)
I am not sure to follow you. As an illustration sig type t end with type t := int is the empty signature whereas sig type t end with type t = int is equivalent to sig type t = int end . May I also reiterate my first warning? Recursive modules are complicated enough. It is better to avoid them. And you may want to avoid complicated encoding of recursive modules while you are not familiar with the module system.