Thanks for pointing this out. I was about to believe the post was correct, but it seems it isn't. However, just to be sure I understand you correctly:
Is the module functor compiled only once, or once for every parameter type? I'm asking because if it's compiled only once, the generated code might be significantly less optimized. This might not play a role for complex parameter types, but could miss lots of good optimization opportunities for simple types such as int or char. How is this solved in those languages?
Also, is it just OCaml and Coq, or is this possible with other strongly typed languages (such as Haskell) as well?
> Is the module functor compiled only once, or once for every parameter type?
Only once. It does in fact miss optimization opportunities in OCaml (where ints and float arrays are given special treatment). In theory this can be overcome with whole-program optimization. The MLton compiler for SML (which also has functors) is such a compiler, though I do not know how it handles this particular case (I would presume it does).
I know of no other languages that allow type modularity beyond the ML family (including various derived formal logic systems). Racket (PLT Scheme) provides "units" which are a similar idea to functors but use contracts instead of types (since Racket is currently untyped). The analogue of a type in Racket is a type membership function from any value to boolean; this function can be used elsewhere in the unit. See for example: http://docs.racket-lang.org/guide/Signatures_and_Units.html
Haskell's module system isn't very advanced. In fact, it about as simple as it could get. This is pretty well known known and there are proposals floating around to add more advanced features. But there generally isn't much need and, as you mention, adding things like module type parameters prevents many cross-module optimizations (which GHC does quite aggressively).
In practice, it doesn't seem to cause much of an issue, but this may just be down to how Haskell tends to be used.
Indeed, typeclasses in languages such as Haskell and Mercury can be (ab)used for many of the same uses as functors. I've used both and there are merits to each, but I still can't put my finger on when one is better than the other.
Is the module functor compiled only once, or once for every parameter type? I'm asking because if it's compiled only once, the generated code might be significantly less optimized. This might not play a role for complex parameter types, but could miss lots of good optimization opportunities for simple types such as int or char. How is this solved in those languages?
Also, is it just OCaml and Coq, or is this possible with other strongly typed languages (such as Haskell) as well?