Hacker News Reader

This book is a real joy to read. I got to peek at a draft at OPLSS 2017 and have been waiting impatiently for it to come out. The detailed, carefully worked examples one after another that this style of book is famous for is adapted beautifully to dependent type theory. Check it out! The code implementing the language in the book is here: https://github.com/the-little-typer/pie

View on HN

Does the book discuss the implementation of the language or just usage of the language?

I believe it's more just how to use a dependently typed language (my copy is still in the mail). Like the Little Schemer, it's written in the Socratic style. I think the idea is that you can do it all in your head if you want, with a piece of paper covering up the column with the answers.

If you are interested in the implementation, you can read more about it from one of the authors: http://davidchristiansen.dk/tutorials/nbe/

Reply on news.ycombinator.com