4 ms·

I use OCaml at work ~every day, and HKTs (to the extent they can be expressed at all, using HOMs) are so unwieldy that I have never run across them in productio

I use OCaml at work ~every day, and HKTs (to the extent they can be expressed at all, using HOMs) are so unwieldy that I have never run across them in production code. In Haskell, they are both easy and routine. So I’m approximating this with “no HKTs in OCaml”.

jolux 6y ago
HKTs indeed aren't a common pattern in OCaml, but first-class modules and similar patterns are common enough in Core. Your statement was that the type system was not powerful enough to express them at all. Whether or not it's practical is a bit different :) 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.
- deleted 6y ago
  [deleted]
- centimeter 6y ago
  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

HKTs indeed aren't a common pattern in OCaml, but first-class modules and similar patterns are common enough in Core. Your statement was that the type system was not powerful enough to express them at all. Whether or not it's practical is a bit different :) 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.

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