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