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.
> 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.