6 ms·

The article is spot on. Even the proposed construction of a category by taking the quotient of closed terms under observational equivalence probably wouldn't re

by fmap 10y ago

The article is spot on. Even the proposed construction of a category by taking the quotient of closed terms under observational equivalence probably wouldn't really work. You may be able to get a category this way, but it just wouldn't have nice properties. Reasoning in the presence of selective strictness is hard... On the other hand I don't think it's actually very relevant. Category theory in the context of haskell is a source of ideas, not a tool for formal proofs. Stream fusion and related constructions such as free monads are wrong if you take seq and undefined into account (and don't even start with actual impure features such as unsafePerformIO). So the "real" category Hask would tell you that these constructions don't exist. The category that people seem to think of as Hask seems to consist of the total functions modulo the obvious observational equivalence. This is very well behaved and I'd argue that it's a great source of ideas for practical programming patterns.

greydius 10y ago
> 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.
- 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.

by fmap 10y ago

greydius 10y ago

> 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.
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.