Re:Ask HN: How to be fluent in functional language speak?
by jolux on Wednesday May 06, 2020 @11:24PM
(#23099364)
>Eilenberg and Lane introduced functors (in the sense more or less used by Haskell) in the 40s.
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.
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).