The Little Typer
by Daniel P. Friedman, David Thrane Christiansen · first published 2018
48% recommend52% neutral
Why HN recommends it
Fun, example-driven introduction to dependent types that builds up step by step in a small Racket-based language, bridging math and code; suits readers curious about type theory, though it is demanding.
Summarised by Claude from recommending comments
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
Mentions per year
What Hacker News says
Related books
Gentle Introduction to Dependent Types with Idris
Recommended by 1 · mentioned by 21 recommend · 2 mention1 recommend · 21 recommend
Little Prover
Daniel P. Friedman, Carl Eastlund, Duane Bibby
Recommended by 9 · mentioned by 189 recommend · 18 mention9 recommend · 189 recommend
2023–2026Little Learner
Daniel P. Friedman, Anurag Mendhekar
Recommended by 10 · mentioned by 1510 recommend · 15 mention10 recommend · 1510 recommend
2007–2026The reasoned schemer
Daniel P. Friedman
Recommended by 45 · mentioned by 7945 recommend · 79 mention45 recommend · 7945 recommend
2007–2026The seasoned schemer
Daniel P. Friedman
Recommended by 33 · mentioned by 4733 recommend · 47 mention33 recommend · 4733 recommend
2008–2025The little MLer
Matthias Felleisen
Recommended by 6 · mentioned by 116 recommend · 11 mention6 recommend · 116 recommend
2007–2026The Little Schemer
Daniel P. Friedman, Matthias Felleisen
Recommended by 288 · mentioned by 438288 recommend · 438 mention288 recommend · 438288 recommend
2014–2025How Not to Be Wrong
Jordan Ellenberg
Recommended by 20 · mentioned by 2420 recommend · 24 mention20 recommend · 2420 recommend
I’ve been impressed with A Philosophy of Software Design. The Little Typer The Little Typer (The MIT Press) https://www.amazon.com/dp/0262536439/ref=cm_sw_r_cp_api_pXxS... looks promising
on “Ask HN: What are the great software development books written in last 5 years?” ↗The Little Typer by Daniel P. Friedman and David Thrane Christianse. It's basically one long book of examples building on each other to show the semantics of a dependently typed programming language. It inspired me to…
on “Ask HN: Books that made you fascinated to learn more mathematics?” ↗…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!…
on “Why is it worth spending time on type theory? (2013)” ↗…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.
on “Introduction to Formal Verification with Lean Part 1” ↗This is one of my two favorite books in The Little <X>er series. The other is The Reasoned Schemer. The Little Typer provides an introduction to dependent types. These can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". It is also possible, to some…
on “The Little Typer (2018)” ↗…interested, you can take a look at Lean [1], Idris [2], and a few others [3,4]. Often these languages have esoteric syntax, but there are projects using a more conventional syntax, too, e.g. Cicada [5]. "The Little Typer" [6] is a pretty good introduction to this topic. [1] https://leanprover.github.io [2] https://www.idris-lang.org [3] https://github.com/agda/agda [4] https://coq.inria.fr [5] https://cicada-lang.org [6]…
on “Ask HN: What technology is “cutting edge” in 2022?” ↗I highly recommend reading The Little Typer if you want a great book that bridges math and code. It starts out describing Pi, a Lisp with some interesting restrictions (limited recursion, types can have values, etc.). They build up some cool stuff…
on “Math-as-Code (2015)” ↗Thanks for this! Hoare (partially) answers a question I asked in the comments on "The Little Typer" (a good treatment of programming with dependent types). That approach to dependent types brings our code closer to being verifiable. Unfortunately as a number of commenters testified it also makes…
on “How did software get so reliable without proof? (1996) [pdf]” ↗…Agda[5], Coq[6], Idris[7], or Lean[8]. All of these languages are designed to be consistent. Of course, implementation bugs do happen[9]. If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11]. [1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co...…
on “Brouwer–Hilbert controversy” ↗…things: 1. Types can be used to classify programs. 2. Dependent types can be used to classify programs by running other programs on them. If you would like to learn more about dependent types, ‘The Little Typer’ is newly out and a lot of fun to read: https://mitpress.mit.edu/books/little-typer
on “Dependent Haskell” ↗The Little Typer teaches dependent types with a Racket based language called Pig. Do recommend, fun book.
on “Racket 7.6” ↗All books in this series is of high quality and very enjoyable. I am going through Little Typer at this time.
on “Ask HN: What is the best programming book you've read?” ↗…implementation but therefore also a nice (imho) syntax, are still hard for most without theoretical background (I was raised and educated by Dijkstra pupils so it was pounded into me from very young); I found The Little Typer a good read on the subject, but that might be impossible for people without background as well; I cannot really estimate that.
on “A dependently typed language for proofs that you can implement in one day” ↗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/
on “Ask HN: Which books have made you a better thinker and problem solver?” ↗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…
on “Can we create a thread for some of the best materials on CS available online?” ↗