Module but no module type recursion?


#1

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.


#2

here it is with something more concrete:

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.

request for comment if you please…


#3

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 ...


#4

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.


#5

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.


#6

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)

#7

thanks guys for that - it indeed is enough for coping with translating some C++.I have here.
is this "r :=… " syntax in the manual? :wink:


#8

Yes, here.


#9

is there a better way of expressing this?:

sig
type x
end

module type v=
sig
type y
end

module F(U:u) (V:v) :
  sig type t  end 
       with type t := U.x 
=struct
type t =V.y
end

…which is to use an otherwise redundant statement to link the types of parameter modules.

in fact I have just used this in my code and the body of the functor does NOT
accept that V.y and U.x are synonymous…


#10

@progman: Just a general note: when posting on discuss, you probably want to surround code with triple-backquotes, i.e. ```, like this:

let x = 5

so that it is properly formatted and indented. You should edit your post to fix that.


#11

Did you mean

module F(X:x)(Y:y with type t = X.t) = struct ... end

?


#12

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)

#13

Destructive substitution removes a type definition and replaces it with the type provided on right-hand side of the substitution. Thus,

module type s = sig type t val x :t end with type t := int
(* is equivalent to *)
module type s = sig val x: int end

If you wish to keep the type definition, you can use regular substitution which adds a type equation to the signature:

module type s = sig type t val x: t with type t = int` 
(* is equivalent to *) 
module type s = sig type t = int val x: t end

#14

what’s the difference?


#15

I mean, I would be quite happy to substitute the type for the real
type or give an equivalence.


#16

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.