To calculate the overall star rating and percentage breakdown by star, we don’t use a simple average. Instead, our system considers things like how recent a review is and if the reviewer bought the item on Amazon. It also analyzes reviews to verify trustworthiness.
Following the "Little Schemer" series, this book introduces under the form of a dialogue, and using a toy language, the mysteries of dependently typed languages. Both extremely pleasant to read and challenging.
Let me be clear; this is not a book for everyone. It did happen, though, to be *exactly* the right book for me. It's written, like the other books in the "Little X-er" series, in the form of a dialogue between a teacher and an (extremely good) student. This means that every point in the book invites you to figure out what the answer should be for yourself; this kind of mental struggle is incredibly valuable in learning material and making it your own.
The topic is Type Theory; specifically, the kind of intuitionistic type theory that underlies languages like Agda, Idris, and Coq. This book provides a lovely gem of a language (pie) in which to explore these ideas. If you're interested in proof-oriented languages like these and you have substantial familiarity with functional languages, I HIGHLY recommend this book.
The way this book teaches a complex topic like dependent types is just fantastic. If you take the time to read through each frame and think about the next frame before you read it, you'll learn so much and so well. Take the time to read and understand every frame. Highly, highly recommended.
I’ve been (slowly) working my way through The Little Typer. It’s a deep dive on dependent types, starting with the very basics and building up a toy language one step at a time. I can feel it gradually changing how I think about programming (heck, how I think about thinking).
It’s really, really enjoyable. The format is very approachable, even fun. Rigorous and demanding, yet doesn’t take itself too seriously. Some lisp experience is helpful, but probably (maybe?) not necessary. But do yourself a favor and learn lisp anyway ;-)
If you’re someone who is already proficient with dependent types, Idris, Coq, etc it might be too basic for you - but it never hurts to solidify your foundations, right? Or maybe wait for The Seasoned Typer ;-)