I haven’t been paying attention to the functional programming world for the past few years, but it turns out there’s fun new stuff! Dependent typing seems like it’s actually becoming (become?) useful and not just for type theorists! I’ve been spending this weekend checking out Idris, going through the Idris book. I recommend both.
It’s the first time since I first checked out Rust that I’ve been this excited about a programming language. Idris doesn’t strike me as super practical at this point, but the pieces seem to hang together very well, and there’s lots of good work for other languages to build on.
If you feel pretty comfortable with Haskell and are looking for something like it but that fixes its main mistakes (e.g. strict by default) and with a type system with a bunch of fun new stuff on top, Idris is for you!
My head is very fuzzy from hacking on this all weekend, may write up more later. This book is actually making me feel a little dizzy.
















