fun with dependent types

It had been a while since i last had this much fun with a programming languages book, and learnt so much in the process. It sure helped that i am a complete neophyte on the subject matter of dependent types: i had recently started playing with Idris, but reading this book really clarified the basics for me. I still remember how, after The little schemer kindled my love for parenthesis, The seasoned schemer made me finally grasp the meaning of continuations. I've got the feeling that the typer has done again the trick, this time giving me the jump start i needed on Curry-Howard, programs as proofs and the beauty of dependent types. As with continuations back in the day, i had read a lot about those things, and thought i had understood them, only to realise that i had not really.

The authors, Daniel P. Friedman and David Thrane Christiansen, have also created a language, Pie, and implemented it in Racket and in Haskell. I've used the latter in a couple of ways: first, it's a very fun learning experience as a weak haskeller (or as a fading racketeer, for that matter) to go over the code (make sure to check Checking Dependent Types with Normalization by Evaluation: A Tutorial, by David himself, if you're interested in how these things are implemented). And, second, the Haskell-based REPL has been my constant companion while reading the book, thanks to a little package that i put together to use it in Emacs, complete with syntax highlighting and a bit of completion for the predefined forms of Pie (it might have a couple of rough corners, but the plan is to submit it to MELPA at some point).

Or you can also use the DrRacket interface if that's your thing, but, be it as it may, don't miss this book!