Just bought the MEAP. I’m really liking it so far. I think I’m finally starting to wrap my mind around dependent types. The printf function is so cool.
I also made a video on how to implement the printf function in Idris if you’re interested:
I’ve also been enjoying the MEAP. It has the most readable explanation of totality I’ve found so far. (Someone asked me to define this on Twitter a while back, and I had a hard time finding an explanation aimed at programmers instead of mathematicians.) I especially liked this bit: “…knowing that a function is total allows us to make much stronger claims about its behaviour based on its type.” Very clear and focused on the practical benefits to the programmer.
Have to say I agree with the totality explanation being quite good. Overall it is a pretty good start.