Why the requirement for signatures in mutually recursive modules in OCaml?

Question

When using mutually recursive module definitions in OCaml, it's necessary to give signatures, even in the .ml file. This is an annoyance where I also want to expose a given interface from the .mli, as I end up repeating the signature twice. :(!

module rec Client : sig
  type ('serv,'cli) t

  (* functions ... *)
end = struct
  type ('serv,'cli) t =
    { server: ('serv,'cli) Server.t
    ; (* other members ... *)
    }
end
and Server : sig
  type ('serv,'cli) t

  (* functions ... *)
end = struct
  type ('serv,'cli) t =
    { mutable clients: ('serv,'cli) Client.t list
    ; mutable state: 'serv
    }

  (* functions again ... *)
end

This is a rough approximation of what I'm doing (Client type objects know the Server that instantiated them. Servers know their Clients).

Of course, the signatures are repeated in the .mli. Why is this necessary?

(Note: I'm not complaining, but actually want to know if there's a type-theory or "hard compiler problem"-related reason for this.)

Tsarevitch

Answer 1

My guess : in order to compile recursive modules compiler needs type annotations for implementation. In mli file (if you are using any) types of those modules can be further restricted or hidden altogether, so in general case it is not sensible for compiler to expect to find useful types in mli wrt resolving type-recursion.

Verticillate

That makes sense. Indeed, I make use of this "feature" by exposing a different type signature for outside consumers in the .mli; I should've realised. – Tsarevitch

Good guess. Type annotations are required because inference in the case of mutually recursive modules and functors is undecidable in general. The literature is full of attempts to refine type systems to optimize for minimal annotation requirements and retain soundness. Whether OCaml's type system could be improved to lower the annotation requirement burden is debatable. – Narda

Answer 2

As far as I know, there is no way around it this. At a very high level, as far as the compiler is concerned, the type signature of Client is incomplete until it knows the type signature of Server, and vice versa. In principle, there is a way around this: the compiler could cross reference your .mli files at compile time. But that approach has disadvantages: it mixes some of the responsibilities of the compiler and the linker, and makes modular compilation (no pun intended) more difficult.

If you're interested, I recommend Xavier Leroy's original proposal for recursive modules.

Pinchcock

Thanks for the link! The type theory is a little above me, but still a good read. But I suppose as ygrek mentioned, it's not for the .mli to declare the type used in compiling the actual module itself. It would make it more ugly, as you mention, if it tried to do so. – Tsarevitch