5 ms·

> Category theory in the context of haskell is a source of ideas, not a tool for formal proofs. My thought as well. It seems Haskell gets criticism from both

> Category theory in the context of haskell is a source of ideas, not a tool for formal proofs. My thought as well. It seems Haskell gets criticism from both ends of the spectrum: it's either too academic to be practical or too practical to be academic.

catnaroek 10y ago
> It seems Haskell gets criticism from both ends of the spectrum: it's either too academic to be practical or too practical to be academic. How about “its abstractions leak in ways the community doesn't want to address”? And “too practical to be academic” is bullshit. There's nothing more practical than an elegant language whose actual semantics matches the way you think.
- codygman 10y ago
  Can you give some examples of abstractions that leak which the community doesn't want (or hasn't wanted) to address?
  - catnaroek 10y ago
    Let's take a basic one: Haskellers would tell you with a straight face that `Either a b` is really the coproduct of `a` and `b`. It's not. If you bring up bottom, they'll tell you “oh, let's just ignore it”. Well, the only way you can ignore it and not be wrong, is to arrange things so that a variable never stands for bottom - that is, to use a strict language. Don't get me wrong, Haskell's abstractions are nice - or they would be, if the premises they are built upon were true.
    - paulddraper 10y ago
      That was a lot of words to say the problem is the bottom type. In other words, "too practical to be academic".
      - catnaroek 10y ago
        The problem isn't the bottom type. The problem is that, in a lazy language, bottom is a value. And this is by no means practical. It's a pain.
        wyager 10y ago
        So you either have bottom as a value or you spin forever because your function that strictly produces a non-bottom value never terminates. Why is the latter preferable? Seems worse to me, since functions that are non-strict on the bottom value will still terminate.
        catnaroek 10y ago
        In a strict language, bottom isn't a part of the domain of any function to begin with, because bottom isn't a value. Functions map values to computations (in call-by-push-value), and then we classify computations by the type of their possible return value (in call-by-value). In any case, if you want to recover the benefits of laziness in a strict language, it's easy: just explicitly thunk computations. Here's how to do it in Standard ML: datatype 'a cell = Pure of 'a | Except of exn | Delay of unit -> 'a type 'a lazy = 'a cell ref fun pure x = ref (Pure x) fun delay f x = ref (Delay (fn _ => f x)) fun compute f = Pure (f ()) handle e => Except e fun force r = case !r of Pure x => x | Except e => raise e | Delay f => (r := compute f; force r) You can also provide a means to tie lazy (co)fixpoints: exception Diverge fun fix f = let val r = ref (Except Diverge) in r := compute (fn _ => f r); force r end The type checker will tell you in very clear terms the difference between `foo` (a value) and `foo lazy` (a thunked computation), in case you forget. On the other hand, recovering the benefits of strictness in a lazy language is much harder, less intuitive, and you don't get help from the type checker.
        wyager 10y ago
        Your "easy" thunked laziness is horrendous. Not only is it unusably verbose, but it relies on mutable reference updates. Doing this properly is a non-trivial problem that really requires language support. GHC has a whole infrastructure around thunks, sparks, blackholing, etc. It's also much easier to make a strict Haskell data type than it is to do this ML hack you've proposed. You either annotate the module as STRICT or you add a few exclamation marks in the data definition. And again, strict languages don't actually solve the totality problem: def foo(x): y = collatz(x) return y y is not bottom. Great, but you've gained nothing. This computation might still diverge. All you've done is kicked the can a foot to the left. To actually get any interesting benefits of bottom not being a value, you need a totality checker, and at that point you might as well use a lazy language with a totality checker. An actually interesting solution would be to distinguish between data and codata at the type level, which would provide the same compile-time guarantees as explicitly deferring computation without the awful syntactic overhead. It still wouldn't solve atotality, but it would address all your concerns.
    - danharaj 10y ago
      Strict languages have the dual problem where products aren't really products.
      - catnaroek 10y ago
        Of course. But I'm not terribly interested in categorical products. They are types inhabited by objects (in the OOP sense: records of methods). I'm more interested in tensor products (types inhabited by plain tuples of data!), which strict languages do have, and which actually distribute over sums.
        danharaj 10y ago
        Porque no los dos? Polarized languages have all the correct semantics and a value/computation distinction and their categorical models aren't that much more complicated than a plain old category.
        catnaroek 10y ago
        I said just that, twice: https://news.ycombinator.com/item?id=12240669 https://news.ycombinator.com/item?id=12240669, https://news.ycombinator.com/item?id=12240622 https://news.ycombinator.com/item?id=12240622 The reason why I care more about values is that, in a general-purpose language, computations will always be somewhat ill-behaved. As far as I can tell, the most we can aspire to is to “cordon off” the misbehavior so that it doesn't infect values - which is exactly what strict languages do, and lazy languages don't do.
        danharaj 10y ago
        Ah so you did. I think your opinion is fair. I care more about computations because they're easier to compose than values. i suppose those are the two major camps on the issue.
        catnaroek 10y ago
    - vilhelm_s 10y ago
      There is one more way to make sure that variables do not stand of bottom -- make sure that you only write terminating functions. Then the equational theory for strict and lazy evaluation becomes the same. I think this is the main reason that people don't worry too much about bottom: in practice all functions should terminate anyway. If your program gets stuck in an infinite loop, you probably have bug.
      - catnaroek 10y ago
        > in practice all functions should terminate anyway Sometimes they terminate with an exception.
tome 10y ago
I wish I could upvote fmap and greydius a hundred times. Yes, Hask isn't quite a category. Can we make a lot of milage by attempting to transport some category theoretical constructions to Haskell nonetheless? Yes. Does Andrej's article serve anything other than to give himself a sense of superiority? No. EDIT: Actually I want to restate my criticism. The blog post does outline a useful programme of research but it is unfortunately overshadowed by Andrej's grandstanding, which is a great shame.

catnaroek 10y ago

> It seems Haskell gets criticism from both ends of the spectrum: it's either too academic to be practical or too practical to be academic. How about “its abstractions leak in ways the community doesn't want to address”? And “too practical to be academic” is bullshit. There's nothing more practical than an elegant language whose actual semantics matches the way you think.

codygman 10y ago
Can you give some examples of abstractions that leak which the community doesn't want (or hasn't wanted) to address?
- catnaroek 10y ago
  Let's take a basic one: Haskellers would tell you with a straight face that `Either a b` is really the coproduct of `a` and `b`. It's not. If you bring up bottom, they'll tell you “oh, let's just ignore it”. Well, the only way you can ignore it and not be wrong, is to arrange things so that a variable never stands for bottom - that is, to use a strict language. Don't get me wrong, Haskell's abstractions are nice - or they would be, if the premises they are built upon were true.
  - paulddraper 10y ago
    That was a lot of words to say the problem is the bottom type. In other words, "too practical to be academic".
    - catnaroek 10y ago
      The problem isn't the bottom type. The problem is that, in a lazy language, bottom is a value. And this is by no means practical. It's a pain.
      - wyager 10y ago
        So you either have bottom as a value or you spin forever because your function that strictly produces a non-bottom value never terminates. Why is the latter preferable? Seems worse to me, since functions that are non-strict on the bottom value will still terminate.
        catnaroek 10y ago
        In a strict language, bottom isn't a part of the domain of any function to begin with, because bottom isn't a value. Functions map values to computations (in call-by-push-value), and then we classify computations by the type of their possible return value (in call-by-value). In any case, if you want to recover the benefits of laziness in a strict language, it's easy: just explicitly thunk computations. Here's how to do it in Standard ML: datatype 'a cell = Pure of 'a | Except of exn | Delay of unit -> 'a type 'a lazy = 'a cell ref fun pure x = ref (Pure x) fun delay f x = ref (Delay (fn _ => f x)) fun compute f = Pure (f ()) handle e => Except e fun force r = case !r of Pure x => x | Except e => raise e | Delay f => (r := compute f; force r) You can also provide a means to tie lazy (co)fixpoints: exception Diverge fun fix f = let val r = ref (Except Diverge) in r := compute (fn _ => f r); force r end The type checker will tell you in very clear terms the difference between `foo` (a value) and `foo lazy` (a thunked computation), in case you forget. On the other hand, recovering the benefits of strictness in a lazy language is much harder, less intuitive, and you don't get help from the type checker.
        wyager 10y ago
        Your "easy" thunked laziness is horrendous. Not only is it unusably verbose, but it relies on mutable reference updates. Doing this properly is a non-trivial problem that really requires language support. GHC has a whole infrastructure around thunks, sparks, blackholing, etc. It's also much easier to make a strict Haskell data type than it is to do this ML hack you've proposed. You either annotate the module as STRICT or you add a few exclamation marks in the data definition. And again, strict languages don't actually solve the totality problem: def foo(x): y = collatz(x) return y y is not bottom. Great, but you've gained nothing. This computation might still diverge. All you've done is kicked the can a foot to the left. To actually get any interesting benefits of bottom not being a value, you need a totality checker, and at that point you might as well use a lazy language with a totality checker. An actually interesting solution would be to distinguish between data and codata at the type level, which would provide the same compile-time guarantees as explicitly deferring computation without the awful syntactic overhead. It still wouldn't solve atotality, but it would address all your concerns.
  - danharaj 10y ago
    Strict languages have the dual problem where products aren't really products.
    - catnaroek 10y ago
      Of course. But I'm not terribly interested in categorical products. They are types inhabited by objects (in the OOP sense: records of methods). I'm more interested in tensor products (types inhabited by plain tuples of data!), which strict languages do have, and which actually distribute over sums.
      - danharaj 10y ago
        Porque no los dos? Polarized languages have all the correct semantics and a value/computation distinction and their categorical models aren't that much more complicated than a plain old category.
        catnaroek 10y ago
        I said just that, twice: https://news.ycombinator.com/item?id=12240669 https://news.ycombinator.com/item?id=12240669, https://news.ycombinator.com/item?id=12240622 https://news.ycombinator.com/item?id=12240622 The reason why I care more about values is that, in a general-purpose language, computations will always be somewhat ill-behaved. As far as I can tell, the most we can aspire to is to “cordon off” the misbehavior so that it doesn't infect values - which is exactly what strict languages do, and lazy languages don't do.
        danharaj 10y ago
        Ah so you did. I think your opinion is fair. I care more about computations because they're easier to compose than values. i suppose those are the two major camps on the issue.
        catnaroek 10y ago
  - vilhelm_s 10y ago
    There is one more way to make sure that variables do not stand of bottom -- make sure that you only write terminating functions. Then the equational theory for strict and lazy evaluation becomes the same. I think this is the main reason that people don't worry too much about bottom: in practice all functions should terminate anyway. If your program gets stuck in an infinite loop, you probably have bug.
    - catnaroek 10y ago
      > in practice all functions should terminate anyway Sometimes they terminate with an exception.

tome 10y ago

I wish I could upvote fmap and greydius a hundred times. Yes, Hask isn't quite a category. Can we make a lot of milage by attempting to transport some category theoretical constructions to Haskell nonetheless? Yes. Does Andrej's article serve anything other than to give himself a sense of superiority? No. EDIT: Actually I want to restate my criticism. The blog post does outline a useful programme of research but it is unfortunately overshadowed by Andrej's grandstanding, which is a great shame.