10 ms·
Hask is not a category
- fmap 10y agoThe 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 agoCan you give some examples of abstractions that leak which the community doesn't want (or hasn't wanted) to address?
- catnaroek 10y agoLet'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 agoThat was a lot of words to say the problem is the bottom type. In other words, "too practical to be academic".
- catnaroek 10y agoThe 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 agoSo 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 agoIn 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 agoI 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.
- dietrichepp 10y agoI would like to see an analysis of Hask when restricted in one of the following ways: 1. Only strict functions (f ⊥ = ⊥) 2. Only total functions (x ≠ ⊥ -> f x ≠ ⊥) But otherwise, the notion that Hask is not a category is nothing new.
- TAForObvReasons 10y ago> But otherwise, the notion that Hask is not a category is nothing new. I'm not entirely sure. Read the official Haskell page on the subject: https://wiki.haskell.org/Hask https://wiki.haskell.org/Hask > In order to make Hask a category, we define two functions f and g as the same morphism if f x = g x for all x. Thus undef1 and undef2 are different values, but the same morphism in Hask. If I understand the passage correctly, they are defining the morphism in a way that makes Hask a category. I think the author of the original post interpreted it the same way.
- dietrichepp 10y agoIt seems like the author isn't interpreting it the same way at all, because "(undefined . id)" would be the same morphism as "undefined" by the criteria on the wiki page, and then the author says that they must be different because you get different behavior when you pass them to "seq", which is a radically different set of criteria. Which is exactly what is addressed by the wiki page... you get different behavior when you use "seq" on two different things which are the same morphism. The wiki page even uses almost the same example.
- catnaroek 10y agoThe problem is that the entire library ecosystem is built under false premises. It's annoying, because you occasionally stumble upon an abstraction leak, and then you need to take a really deep breath, climb down the abstraction ladder (which is pretty tall in Haskell's case!), and look for the exact place where something went wrong.
- dietrichepp 10y agoI'm not convinced. All abstractions are leaky, you just have to decide whether a particular abstraction is useful or not in spite of its leaks. I think the problem you are talking about is the fact that Haskell code tends to have lots of abstractions built on top of other abstractions. While this is definitely a problem in some Haskell code bases, you will also see your fair share of Haskell code which is closer to purely functional code or closer to straightforward imperative code.
- wyager 10y agoGod, I'm so tired of this boring platitude. Every criticism of Haskell not satisfying category laws (of which there are many) are of the form "undefined breaks things". Obviously! How would a runtime-error-inducing concession to practicality not break things? Haskell also fails to satisfy the category laws if I make unsafe FFI calls or use unsafePerformIO to crash the program randomly. Thus is the nature of programming languages.
- ezyang 10y agoReplace every occurrence of "undefined" with "non-terminating program" and the point still stands.
- seagreen 10y agoBut as Haskellers we _are_ concerned about unsafePerformIO et al. -- this is why we have the SAFE pragma.
- tome 10y agoAgreed. But it doesn't need Andrej Bauer to point it out to us.
- l_zzie 10y ago"undefined" isn't the problem here, seq is.
- catnaroek 10y agoBottom values aren't a “concession to practicality”: they're a defect in lazy languages. In ML, when types are viewed as collections of values, the empty type is really empty, sum types are really sums, tuple types are really tensor products and distribute over sums. But, of course, strict languages have dual defects, function spaces aren't as nice unless the language is total (which a general-purpose language can't be), and `let x = e in t` isn't equivalent to the result of substituting `x` with `e` in `t`. To get both the good parts of strictness and the good parts of laziness, you need call-by-push-value: http://www.cs.bham.ac.uk/~pbl/cbpv.html http://www.cs.bham.ac.uk/~pbl/cbpv.html. But, if that's overkill, it's easier to get the benefits of laziness in a primarily strict language, than the other way around.
- danharaj 10y agoIt's well known that `seq` wreaks havoc on lazy semantics. Without `seq` it's much easier to make it a category.
- revelation 10y agoThis is an awesome article about a novel, practical problem solved by Haskell. Or rather I wish it was so my time wasn't utterly wasted.
- danharaj 10y agowhat did you expect from the title?
- Chinjut 10y agoDo we not get a category if we take morphisms from A to B to be expressions of type B with a free variable of type A (thus, morphisms are non-closed terms), and composition of f with g to be substitution of g into the free variable in f? This is automatically associative with proper identities, anyway, even with a purely syntactic notion of morphism equivalence. Of course, one will probably want to impose a coarser notion of equivalence to reason categorically about Haskell in near-usual ways, and perhaps subtleties plague all attempts to do so usefully.
- KZeillmann 10y agoIs there a good introduction to category theory online that references applications in functional programming? I never took a category class in college and am looking to read up on it
- buddhu 10y ago"Category Theory for Programmers" is generally excellent and quite easy to read: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
- qwertyuiop924 10y agoIs this true? Probably, I don't know the math. Do we, as Haskell programmers, need to care? No. If you want to learn Haskell, forget Category theory, until you want to learn the theoretical underpinnings of it. Focus on learning how Haskell ACTUALLY works, not how mathematicians want it to work. In short, learning category theory will likely help you learn Haskell about as much as learning lambda calculus will help you learn Lisp. Maybe a bit less.
- dllthomas 10y ago> If you want to learn Haskell, forget Category theory, until you want to learn the theoretical underpinnings of it. Category Theory isn't very useful for learning the theoretical underpinnings of the language itself.
- qwertyuiop924 10y agoOh. Wow. It's worse than I thought.
- deleted 10y ago[deleted]
- dllthomas 10y agoI'm not sure what you mean by that. Haskell, the language, is theoretically built more on the lambda calculus and logic. Category Theory has served a fruitful source of inspiration in the design of some languages (and in some places provides a common vocabulary).
- tome 10y ago> If you want to learn Haskell, forget Category theory Yes please. Please Don't Learn Category Theory to Learn Haskell: http://jozefg.bitbucket.org/posts/2013-10-14-please-dont-learn-cat-theory.html http://jozefg.bitbucket.org/posts/2013-10-14-please-dont-lea... > learning category theory will likely help you learn Haskell about as much as learning lambda calculus will help you learn Lisp. Maybe a bit less Much, much less, I would have said
- vilhelm_s 10y agoDan Piponi wrote an article about this: "What Category do Haskell Types and Functions Live In?" (http://blog.sigfpe.com/2009/10/what-category-do-haskell-types-and.html http://blog.sigfpe.com/2009/10/what-category-do-haskell-type...) He says that the more fruitful connection between Haskell and category theory goes in the reverse direction. Rather than trying to define a category Hask, which would contain all Haskell programs including exceptions, "undefined", out of memory, and so on, and then see if there are any general theorems in category theory which would help us understand Haskell, we should do it the other way around. Look at a particular small Haskell program, consider all the different categories it could be interpreted in, and see if this gives us a better understanding of category theory!
- catnaroek 10y agoIt's been known for quite a while that Haskellers live in a make-believe world where totality is taken for granted, and Hask is morally the category of sets. One possible fix is to read the call-by-push-value papers: http://www.cs.bham.ac.uk/~pbl/cbpv.html http://www.cs.bham.ac.uk/~pbl/cbpv.html. The danger is that they might want to switch to a strict language.
- danharaj 10y agoHaskell* is essentially an extension of System F. System F has no set models. * Need to enable a few extensions.
- catnaroek 10y agoOh, that's another thing that makes me really angry too: GHC's lack of distinction between first-class polymorphism (functions from types to values, à la System F(ω)) and second-class polymorphism (values, not necessarily functions, that admit more than one type, à la Damas-Milner). But that's a topic for another day. EDIT: Also, I forgot, I haven't actually seen Haskellers use ImpredicativeTypes much. Are you really sure that the predicative subset of System F (just RankN types) has no set models?
- dllthomas 10y ago> It's been known for quite a while that Haskellers live in a make-believe world Or some of us live in the real world where we get work done with useful but imperfect tools, and are pretty aware of where our abstractions run risk of breaking down in practice.
- tome 10y agoI am one of the foremost proponents of Haskell on HN, and you know what? I actually agree with you that a strict language with explict thunk data type would likely be a better way to program. But your attitude really discourages your potential allies from constructively engaging with you.
- nshepperd 10y agoI wonder what the author thinks of "Fast and loose reasoning is morally correct" (Danielsson, Hughes, Jansson, Gibbons. 2006. https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loo...).
- jonsterling 10y agoThat paper is just a bit of bureaucracy which demonstrates that total programs behave the same in a total language as when they are embedded into a partial language (which is an intuitive result, and it's nice that they worked out the details!). It's also a nice demonstration of the logical relations proof technique. But sadly this paper is pulled out all the time by people who I suspect don't understand what is going on, to justify sleight of hand & dodgy reasoning which has little to do with the result in the paper. (Not claiming that's what's happening in the above comment! But I bristle a bit when I see this paper come up in amateur/Haskell circles.)
- deleted 10y ago[deleted]