3 ms·

> It's weird to call it anomalous ML came first in the programming sphere. Eilenberg and Lane introduced functors (in the sense more or less used by Haskell) i

> It's weird to call it anomalous ML came first in the programming sphere. 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).

jolux 6y ago
>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.