What do you think?
Rate this book
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.
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.
424 pages, Paperback
First published September 18, 2018
79 people are currently reading
743 people want to read
About the author
Daniel P. Friedman
16 books95 followersDaniel P. Friedman is Professor of Computer Science in the School of Informatics, Computing, and Engineering at Indiana University and is the author of many books published by the MIT Press, including The Little Schemer and The Seasoned Schemer (with Matthias Felleisen); The Little Prover (with Carl Eastlund); and The Reasoned Schemer (with William E. Byrd, Oleg Kiselyov, and Jason Hemann).
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 12 of 12 reviews
September 24, 2018
This was my first introduction to dependent types so I can't tell you how well it explains the topic.
The presentation was, as usual, excellent. Though, also as usual, I feel like I haven't been given any theory or even key words that I could use to dig deeper. The Curry-Howard correspondence is stated on page 175 and heavily used for the rest of the book but never mentioned by name so it doesn't even show up in the index. Many other interesting things were claimed in the book and I'm sure they also have nice names and wikipedia articles but without those names it's unnecessarily difficult to try to learn more about them.
The book does a wonderful job of starting simple and slowly building up. It got progressively harder to read but I never felt like I had hit a cliff.
Don't be afraid of being confused for a few pages, they often clear up the tricky parts with great examples. When I had a hard time proving to myself that something made sense I would spend some time flipping back and rereading. Once I had grasped what the authors were trying to say I would continue reading and usually find a lovely and clear explanation of the thing I had just struggled with. I should have had more faith in them :)
The presentation was, as usual, excellent. Though, also as usual, I feel like I haven't been given any theory or even key words that I could use to dig deeper. The Curry-Howard correspondence is stated on page 175 and heavily used for the rest of the book but never mentioned by name so it doesn't even show up in the index. Many other interesting things were claimed in the book and I'm sure they also have nice names and wikipedia articles but without those names it's unnecessarily difficult to try to learn more about them.
The book does a wonderful job of starting simple and slowly building up. It got progressively harder to read but I never felt like I had hit a cliff.
Don't be afraid of being confused for a few pages, they often clear up the tricky parts with great examples. When I had a hard time proving to myself that something made sense I would spend some time flipping back and rereading. Once I had grasped what the authors were trying to say I would continue reading and usually find a lovely and clear explanation of the thing I had just struggled with. I should have had more faith in them :)
Read
December 3, 2019Didn't actually finish it. Not that it's a bad book. It certainly doesn't seem so.
It just became less and less useful and interesting to me as I progressed.
The style of the book is very unique, working as a sort of dialog. It introduces concept from type theory slowly and carefully explaining their details. But unless you're directly applying this to your actual work, or you just like type theory in general, then the book probably doesn't have that much to offer
For the same reason, I'm not giving it a rating.
It just became less and less useful and interesting to me as I progressed.
The style of the book is very unique, working as a sort of dialog. It introduces concept from type theory slowly and carefully explaining their details. But unless you're directly applying this to your actual work, or you just like type theory in general, then the book probably doesn't have that much to offer
For the same reason, I'm not giving it a rating.
August 6, 2022
I do really like the question-and-answer, dialogue-style approach of "The Little X" books, and this one fits into that tradition very well. I also like that they made their own little programming language, Pie, that's tailored for the pedagogical purposes of the book -- it works well for this very theory-centered book where a full-featured language with dependent types kinda already has too much machinery and obscures some of the ideas.
That said, I think I don't have enough background in type theory; I enjoyed this book but I think I didn't 100% "get it"; there seems to be a profound idea of the connection between types and proofs and programs...and I'm not getting it. I don't blame Friedman and Christiansen, but I would like to understand that better.
If you're not up to reading this book, it does seem like you can get a very good summary with this talk: "A Little Taste of Dependent Types" by David Christiansen where he summarizes the book; he also did an interview on the Corecursive podcast.
That said, I think I don't have enough background in type theory; I enjoyed this book but I think I didn't 100% "get it"; there seems to be a profound idea of the connection between types and proofs and programs...and I'm not getting it. I don't blame Friedman and Christiansen, but I would like to understand that better.
If you're not up to reading this book, it does seem like you can get a very good summary with this talk: "A Little Taste of Dependent Types" by David Christiansen where he summarizes the book; he also did an interview on the Corecursive podcast.
October 1, 2022
Not a bad book, but between lack of depth, annoying syntax, and no exercises, your time would be better spent working through Software Foundations Volume 1 if you want to spend any time understanding dependent types for some reason.
April 7, 2019
I enjoyed "The Little Schemer" and "The Seasoned Schemer." I found "The Little Typer" to be annoying and frustrating. The schemer books were able to introduce a relatively small number of primitives and build up from them in a style that felt like "try this and see what happens." The typer book required far too many primitives. Many of the primitives had implicit type parameters, something which is not possible within the language. The problem with that is it leaves you scratching your head as to what the types of the primitives are in a book where the constant question is: what is the type of every value and function? Many of the examples amount to wrapping a primitive in a function that does the same thing in a less flexible way because it requires explicit type parameters.
Instead of being "try this and see what happens", the book is constantly forcing you to guess at logical and typing propositions. For me, that is not a good way to learn what is essentially math. Particularly egregious were the chapters where they would say "foo" is a type assuming X, but wouldn't say what it was the type of until much later!
I think either this subject is not well suited to this style, or the choice of subject sequencing was bad. I can imagine a book in this style could be good if it had started by showing how to declare new sum types. The examples in the book could then have been built up from those few primitives. Instead, the language doesn't even support the declaration of new sum types!
Don't assume that you'll enjoy this book because you enjoyed the schemer books.
Instead of being "try this and see what happens", the book is constantly forcing you to guess at logical and typing propositions. For me, that is not a good way to learn what is essentially math. Particularly egregious were the chapters where they would say "foo" is a type assuming X, but wouldn't say what it was the type of until much later!
I think either this subject is not well suited to this style, or the choice of subject sequencing was bad. I can imagine a book in this style could be good if it had started by showing how to declare new sum types. The examples in the book could then have been built up from those few primitives. Instead, the language doesn't even support the declaration of new sum types!
Don't assume that you'll enjoy this book because you enjoyed the schemer books.
January 7, 2019
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 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.
August 17, 2020
I can't remember why I gave this such a low rating, because it is an immensely impressive book that establishes dependent typing from first principles. This is an amazing achievement in itself. Most likely I fell off and should have read it more thoroughly again, because this is high quality work, but I do remember that I'd rather read a conventional book on type theory instead, perhaps something more practical.
November 3, 2019
I must admit that Daniel P. Friedman's and David Thrane Christiansen's The Little Typer was the first book I read from "The Little X" family.
The Little Typer, and from what I know - all the Little books, has a atypical format for a technical book: each chapter introduces a concept via Socratic Dialogue. The pages are split, vertically, into two parts and the Tutor and the Student exchange quips and discuss the issue a hand.
The format get's getting used to and sometimes I felt the quirky humor was forced yet the illustrations and overall feeling of the book captures some sort of childhood charm.
The book lacks exercises, so for each chapter I tried reimplementing what the authors described on my own. For me, the book, wasn't prohibitively hard, although there was only one place where I really had to do a leap of faith and reread the chapter a couple of times to get why a particular substitution was necessary.
Pie, the language introduced by the book, is small enough subset of Scheme that programming in it felt like using lambda calculus. The language verges on the Turing tar pit and often times I felt I was battling with the language and not the problem at hand.
The Little Type has 16 chapters, and the first ones introduce basic types and values of Pie, rules of judgment, constructors and eliminators, normal forms and induction while the latter ones are more about reasoning and proving with Pie.
Sadly, the book doesn't offer depth in the content matter it introduces, and after each concept is introduced and explained once, it switches to another concept - and often times I found myself wishing for additional exercises or at east solving another, similar problem, to see if I "get it".
All in all, the Little Typer is a delightful book that gently introduces dependent type theory, although it suffers from a lack of depth.
The Little Typer, and from what I know - all the Little books, has a atypical format for a technical book: each chapter introduces a concept via Socratic Dialogue. The pages are split, vertically, into two parts and the Tutor and the Student exchange quips and discuss the issue a hand.
The format get's getting used to and sometimes I felt the quirky humor was forced yet the illustrations and overall feeling of the book captures some sort of childhood charm.
The book lacks exercises, so for each chapter I tried reimplementing what the authors described on my own. For me, the book, wasn't prohibitively hard, although there was only one place where I really had to do a leap of faith and reread the chapter a couple of times to get why a particular substitution was necessary.
Pie, the language introduced by the book, is small enough subset of Scheme that programming in it felt like using lambda calculus. The language verges on the Turing tar pit and often times I felt I was battling with the language and not the problem at hand.
The Little Type has 16 chapters, and the first ones introduce basic types and values of Pie, rules of judgment, constructors and eliminators, normal forms and induction while the latter ones are more about reasoning and proving with Pie.
Sadly, the book doesn't offer depth in the content matter it introduces, and after each concept is introduced and explained once, it switches to another concept - and often times I found myself wishing for additional exercises or at east solving another, similar problem, to see if I "get it".
All in all, the Little Typer is a delightful book that gently introduces dependent type theory, although it suffers from a lack of depth.
May 28, 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.
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.
February 14, 2022
Really wanted to give this 5 stars but this book is (for me) a hard way to learn type theory.
This is my first "the little __er" book so the dialog style was new to me.
The dialog style and the fact that actual definitions are presented after they are used prevent me from given this 5 stars.
The subject is fascinating (write correct programs and prove mathematical theorems while programming) and the book is well written and really funny at times.
I do recommend this book for anyone wanting to learn more about type theory and dependent types but if you learn better by definition-theorem-proof (and then finally examples) example kind of learning this book might not be for you.
This is my first "the little __er" book so the dialog style was new to me.
The dialog style and the fact that actual definitions are presented after they are used prevent me from given this 5 stars.
The subject is fascinating (write correct programs and prove mathematical theorems while programming) and the book is well written and really funny at times.
I do recommend this book for anyone wanting to learn more about type theory and dependent types but if you learn better by definition-theorem-proof (and then finally examples) example kind of learning this book might not be for you.
November 7, 2022
For me with no background in programming languages or type theory it was difficult to really get the point of the book. It was difficult for me figure out how the proposed definitions constitutes proofs of anything and I am still unsure if I really got it. More technical background, for example on how to decide if a value is of a certain type, would have been appreciated but then again maybe I am just the wrong audience for these `The Little ...er` books.
April 2, 2020
If you want to understand how dependent-type works, read and enjoy it.
Displaying 1 - 12 of 12 reviews