Hask is not a category
math.andrej.com
math.andrej.com
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.
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.
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.
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.
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.
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.
Sometimes they terminate with an exception.
In other words, "too practical to be academic".
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)
exception Diverge
fun fix f =
let val r = ref (Except Diverge)
in r := compute (fn _ => f r); force r end
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.
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
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.
I'm as far from specialist and educated on the topic of FP as I could be but still collect info on it for later on (or interested people). This statement jumped out at me as I was trying to find non-Turing complete languages for LANGSEC with one sounding very similar. I'm just curious if your statement applies to it or if my guess was way off for whatever reason.
http://pll.cpsc.ucalgary.ca/charity1/www/home.html
https://en.wikipedia.org/wiki/Charity_(programming_language)
Regardless, this one seemed special versus most projects I've seen. Not like the others. Also uses category theory as OP topic is about. So, I'm keeping it & running it by people just in case there's lasting value worth further investment/exploration.
Unfortunately, effects are quite unwieldy. The difficulty of reasoning about effectful programs grows faster than linearly on the number of effects that can happen in them, because effects interact with each other in all sorts of tricky ways. In the limit, reasoning rigorously about a program in which “anything can happen” is practically impossible.
The great insight of functional programming researchers and Haskell programmers is that you can use types to classify programs according to their possible effects, from which it follows that you don't need to worry about any other effects other than those sanctioned by the type. This is the essence of the whole monad business.
At this point, I need to introduce a little bit of terminology:
(0) A value is something you can bind to a variable. At this point, it doesn't matter whether “bind” means “let binding as in functional languages” or “imperative assignment”. Either works equally well.
(1) A computation is what happens when you evaluate an expression or execute a statement. Again, the difference between the functional and imperative versions doesn't really matter.
The difference between strict and lazy languages lies in what is considered a value:
(0) In strict languages (ML, Lisp, Java, Python, etc.), a value is the result of a finished computation. For instance, in Java, `x = 2 + 2;` means “bind the result of evaluating `2 + 2` to the variable `x`”. (In case pron ever reads this, I'm openly admitting he was right and I was wrong about this, when, in a previous flame war between us, he pointed out that `2 + 2` isn't `4`, but rather the former evaluates to the latter.) As a result, values form a pure sublanguage of any strict language: Since no computation can happen and everything is already its own final result, the statement “all computations are free of side effects, and successfully terminate with a result” is vacuously true.
(1) In lazy languages, however, unfinished computations are values in their own right. Compound with the inability of Haskell's type system to distinguish between terminating and non-terminating computations, this means any variable could be bound to a non-terminating computation. Non-termination is an effect (unlike most other effects, often an unwanted one), and this causes technical difficulties, on which I shall not elaborate further, other than to note that these difficulties can be sorted out with a “denotational semantics”, which relies on powerful mathematical tool called “domain theory”. However, instead of learning and using these tools, most Haskellers just pretend the technical difficulties didn't exist in the first place.
While this is more of a philosophical than factual contention, that is as ridiculous as saying "the reduction of `(λx.x)4` is an effect". Non-termination is a property of a computation, not something that a program does to the outside world. The fact that, in Haskell, certain forms of non-termination "do something" to the computer is a consequence of the fact that real-world computers aren't actually turing machines or ideal lambda reduction machines, and sometimes the abstraction falls apart. There's nothing wrong with letting a computer churn away forever trying to reduce a divergent expression (with no effects!), but we just choose not to for practical reasons.
What I'd do is consider the use of recursion to put your computation in a partiality monad. The identity function isn't recursive, so `(λx.x)4` is a pure computation. I'd also require a positivity check on recursive datatypes, to prevent users from sneaking nontermination into pure functions via datatype constructors.
> Non-termination is a property of a computation, not something that a program does to the outside world.
Non-termination gets in the way of producing a result, so it's an effect.
> There's nothing wrong with letting a computer churn away forever trying to reduce a divergent expression (with no effects!)
I wouldn't call it “wrong” either, because effects aren't intrinsically “wrong”.
You seem to be suggesting that IO is the only effect. State, Writer and Either are effects but they don't do anything to the outside world.
A foot closer to where the error occurred.
It's an (admittedly not thread-safe) implementation in under 30 lines! (I would have bothered providing a thread-safe version if Standard ML had a thread-safe reference cell type. Alas...)
In any case, clients don't have to see any of this. All clients have to do is use the functions `pure`, `delay`, `force` and `fix`.
> but it relies on mutable reference updates.
Well, laziness is mutation. My implementation just exposes that fact. A better criticism is “your implementation doesn't give you polymorphic lazy values, because of ML's value restriction”.
> Doing this properly is a non-trivial problem that really requires language support.
I don't disagree. I want both strictness and laziness, naturally. But if I'm forced to have only one, it's easier to get the benefits of laziness in a strict language than the other way around.
> It's also much easier to make a strict Haskell data type than it is to do this ML hack you've proposed.
Even if you use the STRICT pragma, the type checker still won't distinguish lazy from strict data. What happened to “the type checker is your ally”?
> And again, strict languages don't actually solve the totality problem:
I never said they do. What strictness does is “cordon off” the misbehavior of computations (diverging, raising exceptions, you name it) so that it doesn't infect values.
> To actually get any interesting benefits of bottom not being a value, you need a totality checker
No, that's unnecessary. One benefit of bottom not being a value is that, for instance, you can prove type class laws by induction on the datatype for which you're providing an instance. (You can do that in Haskell too, if you don't mind being wrong.)
Of course, bottom is always a computation, but that's a fact of life in languages with general recursion.
> An actually interesting solution would be to distinguish between data and codata at the type level
I've said that, twice: https://news.ycombinator.com/item?id=12240669, https://news.ycombinator.com/item?id=12240622
> It still wouldn't solve atotality,
I don't see how the lack of totality is something that needs to be “solved”. General recursion is a good thing a general-purpose language.
Oh great, this would only add hundreds of lexemes to your average Haskell file!
> Well, laziness is mutation.
Reference mutation is a single implementation of lazy semantics. The trick is doing it correctly and efficiently (syntactically and computationally).
> My implementation just exposes that fact
You say that as if it's a good thing. If I wanted to deal with every detail of the evaluation model, I'd program in assembly.
> the type checker still won't distinguish lazy from strict data.
Nor does it in your example. In your example, there's only strict data, and you can simulate lazy data with a hack. I agree that the type checker should distinguish between data and codata, but let's not pretend that your example demonstrates that. I could do what you're doing in Haskell by compiling every module with STRICT and having manual thunks. (Note that I don't want to do that.)
> What strictness does is “cordon off” the misbehavior of computations
That is a fair point. However, this is not really relevant except in debugging, at which point the runtime will tell us which lazy value is diverging anyway. In production, your program is going to spin (or crash) with strict or lazy semantics.
> You can do that in Haskell too, if you don't mind being wrong.
Or if you don't mind excluding bottom from consideration, which is quite reasonable. That's morally more defensible than pretending you don't have unsafe stateful mutation in languages like ML.
> I've said that, twice:
You didn't actually say that in either of those comments.
> I don't see how the lack of totality is something that needs to be “solved”.
You're the one advocating for the compiler telling you when your program is divergent. What better way to do it than proving totality?
> Oh great, this would only add hundreds of lexemes to your average Haskell file!
What makes you think that? Thunking would be monadic (and comonadic) and so there's great hope that it could be syntactically very convenient. We don't complain that typed IO adds hundreds of lexemes to our average Haskell file.
> > the type checker still won't distinguish lazy from strict data.
> [...] I could do what you're doing in Haskell by compiling every module with STRICT and having manual thunks.
You'd still have to read other people's Haskell code where the types don't distinguish between strict and lazy.
> > What strictness does is “cordon off” the misbehavior of computations
> That is a fair point. However, this is not really relevant except in debugging, at which point the runtime will tell us which lazy value is diverging anyway.
I've never heard of that. How do you get this functionality?
> > I've said that, twice:
> You didn't actually say that in either of those comments.
Yes, that's what CBPV provides.
I'd rather only use laziness when it's absolutely necessary.
> Reference mutation is a single implementation of lazy semantics.
The only way you can avoid mutation in an implementation of laziness is to use a key-value container that maps thunk IDs to their respective contents. This imposes an extra cost, logarithmic in the number of thunks in your computation. I don't think you'd like this implementation.
I'm aware that my implementation has deficiencies, e.g., it isn't thread-safe, and it doesn't support polymorphic lazy values. And, of course, because the compiler isn't aware of what I'm doing, I don't get benefits that Haskellers take for granted, like stream fusion and whatnot. But my implementation does capture the essence of laziness: computing an expression when you first need its result, and memoizing this result to avoid recomputing it again.
> You say that as if it's a good thing. If I wanted to deal with every detail of the evaluation model, I'd program in assembly.
I don't think you can meaningfully abstract the evaluation strategy in a general-purpose programming language. Note that having the Church-Rosser property isn't enough: It says absolutely nothing about the impact of picking this or that reduction strategy on the cost of a computation. Programmers care about that too.
> Nor does it in your example. (...) let's not pretend that your example demonstrates that.
It does. The types `foo` and `foo lazy` are very different, and ML's type checker will let you know if you wrongly conflate them.
> pretending you don't have unsafe stateful mutation in languages like ML.
Using reference cells in ML is perfectly safe as long as your program is single-threaded. It's unsafe in a multi-threaded context, but the same is true of Haskell's `IORef`.
And I don't pretend that there's no mutation in ML. I'm perfectly aware that ML isn't a pure language, and every expression is potentially effectful unless proven otherwise. Just like every Haskell expression is potentially nonproductive unless proven otherwise.
> You didn't actually say that in either of those comments.
I did. Call-by-push-value distinguishes between value types (sums, tensor products) and computation types (categorical products, functions), which live in two different categories, related by a pair of adjoint functors. The composition of these adjoint functors is precisely the usual monad for whatever kind of effects your computations might have. (Corollary: if your computations are pure, the adjunction is actually an equivalence of categories. It becomes patently clear that nontermination is an effect!) All of this is explained in the papers ( http://www.cs.bham.ac.uk/~pbl/papers/ ), so I didn't feel a need to repeat it here.
> You're the one advocating for the compiler telling you when your program is divergent.
When did I say that? What I actually said is “using a strict language prevents computational effects from infecting values”.
Laziness pushes nontermination far away from its source, just like dynamic typing pushes type errors far away from their source. Of course, both laziness and dynamic typing have their place - it just isn't “everywhere in the program”.
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.
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.
That's also fair, of course.
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. But, if that's overkill, it's easier to get the benefits of laziness in a primarily strict language, than the other way around.
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!
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.
I'm not entirely sure. Read the official Haskell page on the subject: 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.
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.
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.
I can tolerate abstraction leaks when the cost of using the non-leaky version is prohibitive. For example, I wouldn't want a language that constantly reminds me that memory allocation can fail. “Memory is infinite” is just too nice an abstraction, and I'm not going to let the fact it isn't true get in the way.
But I can't live with a mismatch between the language's intended and actual semantics. If the Haskell language, libraries and community promise me that Hask is morally the category of sets, then it better be morally the category of sets! Of course, this promise is impossible to fulfill in a language without a typefully delimited terminating subset, so Haskellers better scale down their ambitions to something actually realizable.
> 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.
No, I don't mind high abstraction towers - I actually like them, in fact! What I hate is climbing them down because some abstraction leaked somewhere.
> you will also see your fair share of Haskell code which is closer to purely functional code or closer to straightforward imperative code.
Since when is imperative code straightforward? Reasoning about purely functional programs: high school algebra, plus induction over datatypes. Reasoning about imperative programs: Hoare logic. The facts speak for themselves.
In any case, this has nothing to do with functional vs. imperative. It's just “please don't impose cognitive dissonance on me!”
I wanted to have a real conversation, but, given the hostility in your response, I'll stop.
Can you give an example?
Or, to be consistent with the terminology I've used in other comments, in any language, a value is something a variable can be substituted with. It's just that, in a call-by-value language, variables can never be substituted with unfinished computations.
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.
Yes please. Please Don't Learn Category Theory to Learn Haskell: 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
Category Theory isn't very useful for learning the theoretical underpinnings of the language itself.
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.)
One possible fix is to read the call-by-push-value papers: http://www.cs.bham.ac.uk/~pbl/cbpv.html. The danger is that they might want to switch to a strict language.
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.
* Need to enable a few extensions.
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?