Um... NO. This argument applies equally to functions and constants and is equally wrong.
Types are not anti-modular: the culprit is module systems that don't allow type parameterization. Systems such as Java solve this problem for functions and constants by allowing code to be parameterized over interfaces. Bam, you can compile code using said functions and constants separately from their implementation.
The solution for types is exactly the same: move types into interfaces. Guess what, Objective Caml and Coq do this via module functors and it's glorious. If my airline scheduler module needs to compile separately from my graph module, well I can write:
module Scheduler(Graph: sig
type graph
val traverse: graph -> (string -> unit) -> unit
end) = struct
...blabla...
end
and I can compile that code without ever writing a snippet of the graph module -- not even defining the ADT!
TLDR: this problem has been solved 30 years ago by people who actually use typed languages.
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.
Oddly enough, I think this functorized style is what Bracha advocates. If I understood him correctly in an interview he gave on FLOSS Weekly, his Newspeak language forces you to program in (the dynamically typed equivalent of) the style you describe: each module takes as parameters all modules which it depends on. (He would point out, I think, that ML doesn't force you to adopt this style of writing modules...)
Maybe he discovered module functors on his own and is unaware of their use in statically typed languages such as ML? I don't know, but it certainly seems that this solution is just as good in a statically typed setting as in the dynamically typed setting.
TLDR: this problem has been solved 30 years ago by people
who actually use typed languages.
You have no idea who Gilad Bracha is, do you? In the face of people like him, a bit more modesty is appropriate. You may want to consider that maybe he isn't so obviously wrong, because he knows his subject matter very well.
Types are not anti-modular: the culprit is module systems that don't allow type parameterization. Systems such as Java solve this problem for functions and constants by allowing code to be parameterized over interfaces. Bam, you can compile code using said functions and constants separately from their implementation.
The solution for types is exactly the same: move types into interfaces. Guess what, Objective Caml and Coq do this via module functors and it's glorious. If my airline scheduler module needs to compile separately from my graph module, well I can write:
module Scheduler(Graph: sig type graph val traverse: graph -> (string -> unit) -> unit end) = struct ...blabla... end
and I can compile that code without ever writing a snippet of the graph module -- not even defining the ADT!
TLDR: this problem has been solved 30 years ago by people who actually use typed languages.