Hacker News
2 years ago by isaacimagine

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.

2 years ago by MarquesMa

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.

2 years ago by auggierose

I find the style of the book so exhausting. How can you bring a narrative across like this?

2 years ago by masto

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.

2 years ago by samdk

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.

2 years ago by eatonphil

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).

2 years ago by ripley12

> 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.

2 years ago by auggierose

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.

[0] https://www.goodreads.com/en/book/show/30084187-in-praise-of...

2 years ago by aastronaut

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.

2 years ago by auggierose

I don't like it. If you have a concept worth teaching, explain it properly. Then we can discuss it afterwards, where I can ask the questions myself.

I mean, two pages to discuss what an Atom is?

2 years ago by dymk

“Properly” is doing a lot of heavy lifting in your post. What’s proper? The Little Typer does a fine job at explaining the concepts in my opinion.

2 years ago by undefined
[deleted]
2 years ago by beepbooptheory

Plato would disagree with this! Learning is the forming thoughts, not the copying them over.

2 years ago by drcode

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.

2 years ago by tgb

Can someone elaborate on the meaning of the "Recursion is not an option" quote?

2 years ago by mbrudd

Listen to <https://corecursive.com/023-little-typer-and-pie-language/> for a good explanation -- and a good recursion joke at the beginning!

2 years ago by isaac21259

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.

2 years ago by johnbender

> 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.

Daily Digest

Get a daily email with the the top stories from Hacker News. No spam, unsubscribe at any time.