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