Hacker News new | ask | show | jobs
by coolsunglasses 4257 days ago
Harper's an accomplished person in CS and has done great work, but he's not putting a good argument forward here.

I've talked to Harper about this post and his opposition to Haskell before. I mentioned that it was leading people to believe they could ignore typed FP, not redirecting to an ML derivative. Harper expressed dismay at this.

There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to day stuff.

First: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loos... (This isn't a throw-away reference, informal reasoning has worked extremely well in practice. Yes, I'm making that argument as a user of a pure, typed FP language.)

unsafePerformIO is primarily used to change thunk-memoization behavior [1]. Also, it says unsafe right on the tin. Nobody uses it in practice in ordinary code. It's not something you have to incorporate when reasoning about code.

Giving up reasoning about your Haskell code as if there were semantics-violating unsafePerformIOs lurking in the depths is similar to giving up reasoning about any code because a cosmic ray might flip a bit.

Lets consider the rather remarkable backflips Standard ML and OCaml had to perform in order to make FP work with strictness and impurity.

You can ignore unsafePerformIO because very very few people ever need it and you'll almost never have a reason to use it. Just don't use it.

Similarly, writing total functions is the cultural default in Haskell. The compiler warns on incomplete pattern matches which you can -Werror as well.

You can't define your own Typeable instances as of GHC 7.8 - only derive them, so that soundness issue is gone. Typeable itself is not popularly used, particularly as SYB has fallen out of favor. One critical aspect of why I like Haskell and the community around it is the willingness to fix mistakes. Meanwhile, ML implementations still use the value restriction.

>the example once again calls into question the dogma

Oh please. Haskell is an ensemble, multi-paradigm language with the right defaults (purity, types, immutability, expressions-only) and escape hatches for when you need them.

Haskellers appreciate the value of modules a la ML, but typeclasses and polymorphism by default have proven more compelling in the majority of use-cases. There are still some situations where modules (fibration) would be preferred without resorting to explicit records of functions. For those cases, Backpack [3] is in the works. It won't likely satisfy serious ML users, but should hopefully clean up gaps Haskell users have identified on their own.

Harper's case is over-stated, outdated, and not graced with an understanding of how Haskell code is written. Informal reasoning works if the foundations (purity, types, FP) are solid.

[1]: https://github.com/bitemyapp/blacktip/blob/master/src/Databa...

[2]: http://caml.inria.fr/pub/papers/garrigue-value_restriction-f...

[3]: http://plv.mpi-sws.org/backpack/

5 comments

Having read numerous rants by Harper against Haskell, it really just seems like he's upset Haskell turned out to be the "popular" language.

He is an accomplished computer scientist and a major contributor to Standard ML (i.e. understandably biased), but his Haskell rants read like (type-safe) schoolyard banter.

Perhaps there are some sour grapes, but I think more than that he's just hoping for more. Harper clearly has an executes on a grand vision for what PLs should be—he regularly states that there is only one PL and we're just working to slowly uncover it. Haskell fits it in some ways, and now those ways aren't worth talking about any further, and misses it in others. Harper, I believe, writes to galvanize people to move toward his grand vision of unified PL.

ML is better than Haskell in many ways. This should drive Haskell to improve as much as it drives people to check out ML. And it has!

That makes sense. I wish he'd stop writing obviously linkbait titles like "Haskell is Exceptionally Unsafe" when what he means is that there are some really obscure safety implications for typeable exceptions. I completely agree with bjterry that it has probably caused more people to not look at Haskell to begin with, than people to look at ML.
I think, honestly, Harper has recently discovered his platform is larger than he once expected. There was certainly a time that incendiary, link-Barry titles were useful for, say, getting Haskell's exception system to be more safe (which he absolutely played a part in).

As the audience of his posts widens though it's clear that the impact of those posts is changing.

Usually Andreas Rossberger has written a good rebuttal in the comments.
> Lets consider the rather remarkable backflips Standard ML and OCaml had to perform in order to make FP work with strictness and impurity.

What backflips are these?

Apart from the value restriction (which is a real albeit minor inconvenience; I find it about as annoying in practice as Haskell's monomorphism restriction, and each can be removed in principle, at the cost of making it harder to reason about the semantics/cost of using a variable), I'm honestly not sure what you have in mind.

On a tangent, I'm not sure when statically-enforced purity (as opposed to purity-by-default) and pervasive laziness (as opposed to laziness-as-a-tool) became culturally defining features of FP. The original FP language, Lisp (and even its "this FP stuff is great, let's have some more" cousin Scheme) is impure and strict. I'm grateful to Haskell for trying to answer the question "just how far can we push these purity and laziness ideas", but I don't think that complete purity or laziness are necessary features for FP. They're just tools in its toolbox. But then, I have always been inclined to pluralism.

"There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to day stuff."

Examples, please. (I like bright, shiny things.)

The principal thing I push learners towards after Haskell would be things like Coq and Agda. Coq has better learning materials, Agda has Haskell integration.

The usual sequence is [1] followed by [2].

Augment with [3] and [4] as needed.

One negative thing about Coq/Agda/Idris is they don't have a satisfactory encoding of typeclasses [5]. This is a problem in general with all dependently typed languages. Proof obligations get "churned" by changing code and the only tool to address that is extremely general proof terms combined with proof search. The best proof search is Coq, but the code extraction is heartburn-inducing for Haskell users.

Whereas in Haskell, we get extremely lightweight and type-safe code refactoring because of the way in which we leverage typeclasses and parametricity. This turns out to be very valuable as your projects get more serious.

That said, still entirely worthwhile to learn Coq or Agda.

By the way, this [6] is how I teach Haskell. Working on a book as well.

[1]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

[2]: http://adam.chlipala.net/cpdt/

[3]: http://cheng.staff.shef.ac.uk/proofguide/proofguide.pdf

[4]: http://www.amazon.com/How-Prove-It-Structured-Approach/dp/05...

[5]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...

[6]: https://github.com/bitemyapp/learnhaskell

Perhaps Coq, Agda, Idris, and other such dependently-typed languages are to be considered, at least in some dimensions, "more advanced" than Haskell.
I wouldn't say full-blown theorem provers (Coq, Agda) are really in the same category as Idris, which is supposed to be more practical.
Why not? I'd say that Agda/Idris/Coq are substantially the same languages with variation arising only in the kind of styles of coding they emphasize.
But isn't this a variant on the old "but it's Turing-complete, therefore you can do anything" fallacy? Sure, their type system may be similar, but the question is, which one will let you write, say, a robust, maintainable HTTP client with the least amount of pain?
I suppose that's true. I guess in my eyes DTs are such a meteoric difference that Idris is not sufficiently more interesting than the others yet. But time will tell if they manage to build a better way to manage proofs, for instance, they could really change the game.
I'm curious what your objections to the value restriction? It's a tradeoff for allowing impurity, which is of debatable use (I like it), but it's not totally off the wall.
As an intermediate Haskeller I'm curious, what's the replacement for SYB? I've worked in haskell primarily on compiler-like tree tranformation code and SYB seems to fit the bill perfectly.
The direct equivalent and replacement is GHC http://www.haskell.org/haskellwiki/Generics.

Edit: I just wanted to add that if you do compiler-like tree transformation code it behooves you to explore uniplate/multiplate/plated.

Sick, thank you for the reply and pointer to uniplate and associated tools!
IIRC, the thing about Uniplate is that the API makes it easy to build traversal functions like "get a list of all X nodes in this tree" while SYB provides some folding operators that are a bit harder to work with.
TH isn't really the same functionality as SYB.