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) ->
and F : fsig =
functor (M: s) -> struct
let f _= M.v
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…