4 ms·

I definitely sufficiently hedged my original claim: > OCaml's type system is not powerful/expressive enough that (to use the given example) abstracting over ty

I definitely sufficiently hedged my original claim: > 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.

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

jolux 6y ago

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

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