"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."
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.
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.
That there is no game-plan for doing anything any better than Coq presently does is why I'm a bit skeptical. The trimmings are nicer - nothing else as of yet.
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