I read this book twice, one of my favorite reads. If you can look past the student-teacher discussion format (which I personally enjoy) it's an excellent introduction to dependent types.
I'm a fan of "The Little X" series so I bought this one when it just came out.
I believe the author did tried their best and a great job they did - which made me work through half of the book (which is a lot for me, and for this topic). However, I did gave up eventually and decide to revisit it in the long future.
My guess is people should discuss more about dependent types - I remember functional programming concepts were also hard for me as well. But after being exposed to those conversations for a while (functional programming was one of the hot topic a dacade ago), I find those concepts were not that hard to understand, they're just different from C-like's perspective.
I feel that way about anything that tries to explain concepts with cartoons. “why's (poignant) Guide to Ruby” as a prime example of something I can’t look at for 5 minutes without wanting to burn it. Yet I know that lots of people are big fans of this approach. So I can only deduce that the world don’t move to the beat of just one drum. What might be right for you may not be right for some.
Personally, I put The Little Lisper/Schemer on the “Greatest Programming Books Ever” shelf, next to The C Programming Language. I found the style captivating — and insidious. The first time I read it, I thought I was learning a programming language, but it subliminally reprogrammed my brain to see recursion everywhere.
The Little Schemer was what finally got me to internalize how to solve problems recursively. I'd taken a couple of college classes and could do it some already, but it took a lot more thought than solving those same problems in other ways.
About a third of the way through The Little Schemer, things just clicked, and what had been hard became pretty instantly easy.
Some of that was it building on existing knowledge, but I found the structure very helpful. The narrative is really just the glue around a well-designed series of incremental problems.
As a separate path, I finally learned to internalize recursion by building a R7RS Scheme (and a good chunk of its standard library) and spending a year doing projects for fun in various Schemes and Standard ML.
I'm not saying every dev needs to do this but if you do want to get better at recursion, reading this book isn't the only path (good news for me because I really didn't like The Little Xer format).
> The narrative is really just the glue around a well-designed series of incremental problems.
I felt like The Little Schemer should have given those (nicely incremental) problems more real-world context. I worked my way through it and was frequently left wondering "OK, that's clever - but why should I care?"
Clearly a lot of people find the book useful, I might be the odd one out, but I was mostly left scratching my head.
Just yesterday I read "In Praise of Mathematics" [0]. It is written as an interview / dialogue, but a very pleasant read. I think the main difference is that here the pieces are large enough to convey fully formed thoughts and ideas, not ideas hacked into very small pieces as in The Little XXX.
i think the discussion style of the "the little" series is quite nice to introduce concepts. it feels like i'd observe a discussion between two experienced people.
The concepts in the "Little" books are essentially math, and the best way to explain math is by showing formulas.
The "Little" books do exactly this, except a person has taken the painstaking time of breaking everything into digestible, bite-sized portions to optimize for learning.
I don't think that the best way to explain math is to show formulas. If that were so, then the best way to learn math would be to look at mechanised formalisations of math, which is clearly not the case.
It's exhaustive, concrete, logically ordered, and pedagogically consistent. It has its virtues. You explain by enumerating the maximal compact extension of cases rather than providing an intension and making your reader generate all that work. Maybe it's good if they do, but how would a book give feedback if they fail? By providing an instance in the extension to compare to...
I read a few of the series, sometimes it was boring, sometimes it was surprisingly beautiful. I don't know what to conclude, but the subject is worth it nonetheless.
I remember when I read The Little Schemer, the parts I had no trouble with were the ones I’d already had a decent grasp on. The last few chapters I could only scan, with little in the way of comprehension, and the style was not an insignificant part of the reason.
I don’t know if I’d have an easier time with those parts now, but I suspect a lot of readers completely unfamiliar with concepts like recursion would get little out of the book.
Dependent type systems don't deal well with non termination. In general you can't prove a program will or won't terminate. The solution is to disallow recursion except through a few eliminators which do recursion in a well founded way that is guaranteed to halt.
The reason they don't work well with recursion is you could have something like:
false :: _|_
false = false
Where false is a function we are defining of the uninhabited type.
For more complicated versions stuff like this see Girard's paradox.
> In general you can't prove a program will or won't terminate.
As a point of clarity for folks who come to this (the commenter clearly knows this) one can’t _automatically_ prove for an arbitrary program whether or not it terminates. It’s definitely possible to prove this manually per program and most dependently typed languages will do the work for you as a matter of sound over approximation as long as one of the arguments is shrinking in an obvious way.
