The Little Typer
An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time. A program's type describes its behavior. Dependent types are a first-class part of a language, and are much more powerful than other kinds of types; using just one language for types and programs allows program descriptions to be as powerful as the programs they describe. The Little Typer explains dependent types, beginning with a very small language that looks very much like Scheme and extending it to cover both programming with dependent types and using dependent types for mathematical reasoning. Readers should be familiar with the basics of a Lisp-like programming language, as presented in the first four chapters of The Little Schemer. The first five chapters of The Little Typer provide the needed tools to understand dependent types; the remaining chapters use these tools to build a bridge between mathematics and programming. Readers will learn that tools they know from programming—pairs, lists, functions, and recursion—can also capture patterns of reasoning. The Little Typer does not attempt to teach either practical programming skills or a fully rigorous approach to types. Instead, it demonstrates the most beautiful aspects as simply as possible, one step at a time.
Stats for nerds
16recommend
37mentions
33people
2018–2026years
46% recommend54% neutral
Mentions per year
What Hacker News says
- If you like Lean, here are two more great, short books on proving things about your program (not with Lean, though):
1. https://mitpress.mit.edu/9780262527958/the-little-prover/
2. https://mitpress.mit.edu/9780262536431/the-little-typer/
David Thrane Christiansen, co-author of the second, also wrote Functional Programming in Lean (Lean 4) among many other tutorials and things.
- > to introduce early stage students to Scheme before Python, or deep learning before calculus.
This book is part of the classic "Little" series of books starting with the "Little Schemer" which, despite its name and style, is certainly not a novice beginner book.
The later books: "Seasoned Schemer", "Reasoned Schemer", "The Little Typer" and "The Little Prover" are all very advanced books. They share the same style of illustrations and Socratic method, but you will absolutely need to work through them slowly and careful to get value out of them.
The "Little" books are generally targeted to an audience of computer language nerds and pretty much assume you have a solid understanding of programming, familiarity with scheme and the books come from a time when every serious engineer had basic calc knowledge.
These are classics (and I was really impressed with "The Little Learner") but are very serious and challenging texts, that outside the first book, are aimed at advanced readers (and for those readers are true delights).
- Books. Some books on my shelf covering these topics:
"Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)
First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers
For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof
"Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo
"Type-Driven Development with Idris" by Edwin Brady
"Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski
"Types and Programming Languages" by Pierce
"Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)
"The Little Typer" by Friedman and Christiansen
"Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)
For Category Theory:
"The Joy of Abstraction" (2023) by Euginia Cheng
"Basic Category Theory for Computer Scientists" by Benjamin C. Pierce
"Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel
"Categories for the Working Philosopher" by Landry
- It's been amazing learning about this. From "The Little Typer" book to Computerphile's videos on dependent (and homotopy, somewhat related?) type theory, to discovering Lean for interactive (math) proof construction, the history of it all dating back to Bertrand Russel trying to explain math from first principles, just wow. So lucky to live in a world where this is true.
- Lots of great suggestions here.
I'll throw out a recommendation for The Little series of books (e.g., The Little Schemer, The Seasoned Schemer, The Reasoned Schemer, The Little Typer, etc.)
The first book is all you need to grok recursion. You can just toss a copy at any student who struggles with it.
The second book ends with some really non-trivial CS stuff.
They're fantastic examples of the power of good pedagogy to explain interesting and difficult concepts normally relegated to drier texts.
- Came here to say the same thing. The other books in the series are pretty good too.
E.g. The Little Prover https://mitpress.mit.edu/9780262527958/the-little-prover/
and
The Little Typer https://mitpress.mit.edu/9780262536431/the-little-typer/
Related
2015–2026
Little Prover
9 recommend · 20
Little Learner
10 recommend · 17
The Little Schemer
288 recommend · 652
Type theory and functional programming
2 recommend · 6
Type Theory and Formal Proof
11 recommend · 15
The reasoned schemer
45 recommend · 107
The seasoned schemer
recommend · 60
