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.
> 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.
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.
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.
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.
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.
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
Just so you don't think that the entire Haskell community disapproves of your ideas, let me say that I very much appreciate this kind of programme (as long as you preserve purity!).
> All clients have to do is use the functions `pure`, `delay`, `force` and `fix`.
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?
> > All clients have to do is use the functions `pure`, `delay`, `force` and `fix`.
> 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.
> Oh great, this would only add hundreds of lexemes to your average Haskell file!
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”.
"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,"
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.
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.
Practical programming is all about the effects. Without effects, maybe you can do very good mathematics, but write software you cannot.
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.
> that is as ridiculous as saying "the reduction of `(λx.x)4` is an effect".
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”.
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.
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.
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.
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.
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.
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.
> 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.
It 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.
The 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.
I'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.
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!”
That's a really disingenuous interpretation of "straightforward". If you don't want to have a real conversation then just don't bother replying next time.
I really don't know what's got into you. You've clearly got some great ideas about what's valuable in programming languages. If you took the time you spent making vague complaints about Haskell and instead spent it pointing out concrete flaws, their consequences, and how to fix them, then we'd all be much better off. I would encourage you to do that.
For most type classes and instances, the proofs that the corresponding laws hold break horribly if you substitute their free variables with nonterminating computations. For instance, `0 * x = 0` doesn't hold if `x` is `undefined`.
How would a strict language help? `0 * x = 0` doesn't hold if `x` is substituted by a non-terminating computation `f ()`. What exactly would be the benefit?
There's no such distinction. But, in the operational semantics of a call-by-value language, variables are only substituted with values.
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.
God, 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.
Bottom 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. But, if that's overkill, it's easier to get the benefits of laziness in a primarily strict language, than the other way around.
Do 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.
Is 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
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.
I'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).
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!
It'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. The danger is that they might want to switch to a strict language.
Oh, 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?
> 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.
I 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.
That 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.)
76 comments
[ 5.7 ms ] story [ 143 ms ] threadOn 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.
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.
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:
You can also provide a means to tie lazy (co)fixpoints: 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.
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:
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.
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 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.
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.
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”.
A foot closer to where the error occurred.
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.
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.
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.
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.
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.
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.
Category Theory isn't very useful for learning the theoretical underpinnings of the language itself.
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
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!
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.
* 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?
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.
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.)