Grief, this is impressive. For the record, I really can’t recommend learning (typed, pure) functional programming on Idris. It’s a whole extra step beyond learning to do Haskell well.
On the contrary, I’d recommend to start with Idris instead.
The design of the language is globally better and way more coherent. It fixes a lot of Haskell “mistakes”.
Check out “Type-Driven Development with Idris” by Edwin Brady himself. The book is truly amazing.
Idris is great, its design is super impressive, and it expanded my mind tremendously in terms of what is possible in programming. We can and should ask much more of our type systems!
It is also way less mature than Haskell, and someone trying to learn it will run into many issues as a result. I mean, read the linked blog post! Needing to regularly restart one's editor, long compile times for even short programs, and difficulties with installation are all issues I also ran into.
(Also, strong agree about the book. It's really well written, and all around excellent)
I would second this. If you've never done pure functional programming before I would hesitate to recommend Idris as your first foray simply because of ergonomic issues with the tooling. Regardless of whether you think Idris the language is suitable for a beginner, it's not a fun experience to deal with the landscape of abandoned libraries, editor integration issues, compiler bugs, etc. if you are already struggling to understand some of the basic principles behind the language.
The only exception is if you use it purely as a companion to the Type-Driven Development book. As long as you don't stray too far from the book you generally won't run into any of these other issues and it's more plausible to think of it as a first foray into pure functional programming.
Idris 2 is supposed to be better in that regard. I could not see in the article if 1 or 2 was used but I think it was 1; 2 is a lot faster and fixed a lot of issues from 1.
I believe the plan is to release an Idris2 edition of the book. The Idris2 repository currently has all of the book code as part of its test suite and is making progress towards compiling all of it (currently 12 of the 15 chapters).
I wouldn't think so. As a beginner you can probably just treat Idris like a superset of Haskell and learn the parts that are common to both. For example you can use the `data T =` syntax and not worry about the more advanced `data T where` syntax for GADTs. You can turn off totality checking. You can use simple data types like lists rather than length-indexed vectors.
I quite like the book Type-Driven Development with Idris by Edwin Brady. It doesn't assume you already know Haskell. But it does teach you a nice mindset of thinking about types first and use that to drive the implementation.
