You also said that their use of "functor" was probably the result of being French vs English, when I pointed out that in fact it came from Standard ML, which is a British design. Moreover, the creators of Haskell originally built typeclasses as an extension to Standard ML (1980s), and Functor was added in the same version of Haskell that Monad was (1.3, roughly 1998).
The connection between ML functors (specifically the interface/signature) and typeclasses in Haskell is relatively clear, if you understand how they both work. I don't disagree that typeclasses are more general, but modules have their appeal as well. I'm pretty excited to see where Backpack ends up in Haskell, personally.
> OCaml's type system is not powerful/expressive enough that (to use the given example) abstracting over type constructors is likely to ever come up.
And I stand by that. It’s not likely to ever come up, even if it’s possible to kludge it.
You’re right about the name though - it seems like the anomalous use of “functor” predates francophone intervention.
What you said is that it's not powerful or expressive enough, but my impression was that they were both expressible in terms of System Fω, an understanding I would like to correct if it's wrong.
Eilenberg and Lane introduced functors (in the sense more or less used by Haskell) in the 40s.
> my impression was that they were both expressible in terms of System Fω
This is not correct anymore - Fω is insufficient to describe GADTs. You need coercions and equality constraints as well.
It's also approximately as useful a claim as "the languages are equally powerful because they're both Turing complete".
I'm referring to practicability, not theoretical possibility (and I've clarified as much several times now).
Yes.
>This is not correct anymore - Fω is insufficient to describe GADTs. You need coercions and equality constraints as well.
Of course, OCaml has GADTs these days. I suppose neither of them are really Fω anymore, then.
>It's also approximately as useful a claim as "the languages are equally powerful because they're both Turing complete".
Agree to disagree. I think when discussing how powerful a language is, a rigorous notion like Turing completeness or position on the lambda cube is still significant, even if it's not the most immediately visible.
>I'm referring to practicability, not theoretical possibility (and I've clarified as much several times now).
Fair enough, I'll chalk this up to a misunderstanding.