The Little Typer

This review was written in June of 2020

Fun, difficult, but be careful: much more difficult than it is fun. It tries to act all light n breezy, approachable, but since it's taking such a bare-bones implementation of dependent type theory it's actually much more difficult than e.g. Software Foundations (tactics, a form of metaprogramming popular in type theory, is easy mode, believe me). Not for noobs, you want to have some degree of indoctrination into functional programming and types before chasing after this book.

I wish Sigma types got more action.

Recommended to intermediate programmers. Better read after Software Foundations volume 1, IMO.

Primitive recursion is hard.

It's ok to read if you hadn't read a little book before, too.

I read it a little too fast. I think i'd have gotten more out of it if I wasn't speed reading. You really have to type everything into your Dr. Racket environment in order to absorb anything at all.

I usually like to leave things feeling like I could get away with at least TAing a course in it, and by that metric I didn't absorb this book nearly enough. So I might come back and read it again someday.