> I believe this is to do with the language rather than to do with modules?
Both, sort of. The problem is that mutually recursive modules are tricky. So, it's a limitation of the language, but one that is there for a reason.
> I think this is fixed by OCaml GADTs
No, GADTs solve a different problem. Essentially, normal ADTs lose type information (due to runtime polymorphism). GADTs give you compile time polymorphism, so the compiler can track which variant a given expression uses. Consider this:
# type t = Int of int | String of string;;
type t = Int of int | String of string
# [ Int 1; String "x" ];;
- : t list = [Int 1; String "x"]
# type _ t = Int: int -> int t | String: string -> string t;;
type _ t = Int : int -> int t | String : string -> string t
# [ Int 1; String "x" ];;
Error: This expression has type string t
but an expression was expected of type int t
Type string is not compatible with type int
The problem with functors (and also type parameters) is the following. Assume that you have a functor such as:
module F(S: sig type t val f: t -> t end) = struct ... end
To avoid code duplication, F has to pass arguments to S.f using the same stack layout, regardless of whether it's (say) a float, an int, or a list. This means that floats need to get boxed (so that they use the same memory layout) and integers have to be tagged (because the GC can't tell from the stack frame what the type of the value is).
Both, sort of. The problem is that mutually recursive modules are tricky. So, it's a limitation of the language, but one that is there for a reason.
> I think this is fixed by OCaml GADTs
No, GADTs solve a different problem. Essentially, normal ADTs lose type information (due to runtime polymorphism). GADTs give you compile time polymorphism, so the compiler can track which variant a given expression uses. Consider this:
The problem with functors (and also type parameters) is the following. Assume that you have a functor such as: To avoid code duplication, F has to pass arguments to S.f using the same stack layout, regardless of whether it's (say) a float, an int, or a list. This means that floats need to get boxed (so that they use the same memory layout) and integers have to be tagged (because the GC can't tell from the stack frame what the type of the value is).