5 ms·

The Little Typer (2018)

179 points by aarestad 2y ago

Jtsummers 2y ago
Three past discussions with discussion: https://news.ycombinator.com/item?id=18046745 https://news.ycombinator.com/item?id=18046745 - Sept 22, 2018 (132 comments) https://news.ycombinator.com/item?id=31465368 https://news.ycombinator.com/item?id=31465368 - May 22, 2022 (23 comments) https://news.ycombinator.com/item?id=33162971 https://news.ycombinator.com/item?id=33162971 - Oct 11, 2022 (96 comments)
- deleted 2y ago
  [deleted]
kevindamm 2y ago
I liked the dialogue-driven format of this and the others in the series (I've read Schemer and Learner too), at least once I got used to the split-mind feel of it, but I feel it would be better as an interactive media instead of the books. There's an expectation that you're following along and typing nearly every line into the appropriate REPL. I found this difficult to do while juggling the hardcopies and not any easier on an ebook reader -- I could stop worrying about cracking the spine but the digital copies I sampled or purchased always completely ruined the typesetting. All the REPL interactions are transcribed as images, and the constant focus-and-pinch-zoom disrupts the engagement. I ended up just reading through and hoping to catch enough of the gist of things then doing my usual side-project-as-learning instrument thing. I hope somebody tries to build an interactive playground for this book or the Little Learner, complete with guiding dialog. The typesetting in the hardcopies is really unique and impressive.
ahelwer 2y ago
I worked through this a few years ago and it is wonderful, but I found chapter 9 on the replace function totally impenetrable, so I wrote a blog post in the same dialogue style intended as a gentler prelude to it. A few people have emailed me saying they found it and it helped them. https://ahelwer.ca/post/2022-10-13-little-typer-ch9/ https://ahelwer.ca/post/2022-10-13-little-typer-ch9/
- crdrost 2y ago
  This is great for me for a completely auxiliary reason, which is that I wanted to know whether this was just gonna be a book about programming Fibonacci numbers into types or some ish... and in some ways it's kinda worse, at chapter 9 you are still proving that different takes on x→x+1 are the same. (But using rewrite rules seems kinda interesting in the abstract I guess.)
  - ahelwer 2y ago
    This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same author, which is freely available online!
758758 2y ago
[flagged]
kccqzy 2y ago
I bought this book when it first came out. Unfortunately this book required a time commitment greater than what I had available at that time and I didn't finish. It's thoroughly enjoyable (at least the first few chapters) but it requires a level of thinking that might not be available if you just finished a day of work.
RedNifre 2y ago
Is there an online community for this where you can ask questions? E.g. a discord server or an IRC channel?
- nextos 2y ago
  I don't think there's a centralized community for the Little Series. I think this is unfortunate. With a community, some great titles like The Little MLer (typed FP) and A Little Java, a Few Patterns (OOP) would be much better known. I found those two outstanding. I think A Little Java has been reprinted. But last time I checked, The Little MLer was bloody expensive. Standard ML, OCaml and F# need a lot more exposure. They are simple and practical. The Little MLer does a great job introducing the basics. To close the circle, the Little Series is missing a book about concurrent and distributed paradigms à la Erlang. They already have functional programming, typed functional programming, declarative programming, dependent types, theorem proving, object-oriented programming and machine learning.
- soegaard 2y ago
  You are welcome in the Racket Discord. https://discord.com/invite/racket-571040468092321801 https://discord.com/invite/racket-571040468092321801
  - RedNifre 2y ago
    Thank you! I joined, but don't see a place for Pie, so I just asked about it in the beginner channel instead.
- ysangkok 2y ago
  The Gay Haskell discord server has a channel for dependent types. There is also a discord server for Type Theory Forall, a podcast.
ducktective 2y ago
What modern scheme is best to use for these "the little x'er" book series? Some of them suggest their dialect (like learner suggests Racket I think), but what about others? In short, what scheme is the most practical and useful nowadays? Here is the result of my research so far, in order of preference according to the above requirements: Guile: most active community, GNU glue language, Guix Chicken: most pragmatic one with a package manager but older Chez: most performant one, less active community and libraries
- RedNifre 2y ago
  This one comes with its own language, "Pie", which you can use in DrRacket with #lang pie
- 4ad 2y ago
  I don't know what is the best Scheme implementation, but this book has little to do with Scheme though. Pie uses S-expressions for syntax, and happens to be implemented in Racket, but you don't interact with Racket directly.
  - matrix12 2y ago
    Gerbil scheme works great with the Schemer series of books.
- deleted 2y ago
  [deleted]
- nextos 2y ago
  Guile is great, but I think outside Guix it's pretty niche. Racket is probably the most frequent choice. But I really like some aspects of Chicken, Gambit and Bigloo. Even Clojure or CL could also be used, with a bit of friction of course.
- davexunit 2y ago
  Guile is my Scheme of choice.
- wk_end 2y ago
ProllyInfamous 2y ago
As a retired electrician attempting hobby-level "learn to code" (i.e. I don't know anything about modern programming and did not even understand anything from OP's link), this Amazon review helped me understand OP's link: >..I’ve been (slowly) working my way through The Little Typer. It’s a deep dive on dependent types, starting with the very basics and building up a toy language one step at a time. I can feel it gradually changing how I think about programming (heck, how I think about thinking). >..It’s really, really enjoyable. The format is very approachable, even fun. Rigorous and demanding, yet doesn’t take itself too seriously. Some lisp experience is helpful, but probably (maybe?) not necessary. But do yourself a favor and learn lisp anyway ;-) Maybe some day I'll motivate myself to even figure out how to first install Racket/Pie (first, I have to figure out what even these are). Thanks for the motivation/educational resource, OP.
- rgrmrts 2y ago
  I’d recommend the earlier book in the series, The Little Schemer, for what it’s worth! It’s more aimed towards beginners. Similar format to this book.
  - ProllyInfamous 2y ago
    >The Little Schemer Inially wasn't sure if your comment was "a joke," but thanks for the real introduction: amazon.com/Little-Schemer-Daniel-P-Friedman/dp/0262560992/ [link to book]
    - Jtsummers 2y ago
      https://mitpress.mit.edu/author/daniel-p-friedman-4089/ https://mitpress.mit.edu/author/daniel-p-friedman-4089/ - one of the authors on all the books in the series. The Little Schemer and The Seasoned Schemer are both beginner books using Scheme. The Reasoned Schemer uses Scheme + Minikanren, an extension of Scheme that allows for logical/relational programming (look up Prolog and Datalog as languages in the same vein). The Little Typer is the linked book covering type systems and, specifically, dependent typing. The Little Learner covers machine learning. The Little Prover uses the same format and has you develop proofs. Little, Seasoned, and Reasoned are, IMO, the better books in the series to start with. I found the later ones to be good but very dense and not always as clear, had to step back a lot more and reread sections. That's mostly due to the material being much harder and more technical than the earlier books, not a quality issue with the writing itself. My recommend reading order for someone with no Racket, Scheme, or Lisp experience wanting to tackle the series would be: Little -> Seasoned -> [Optional: Reasoned] -> {Any order: Prover, Typer, Learner}. I think Prover may be better before Typer, but it's been a while since I looked at either, so a soft recommendation of Prover -> Typer. If you have some Racket, Scheme, or Lisp experience, I'd suggest to either skim the first couple books to get used to the format or skip them entirely and use Reasoned as your first book in the series. http://minikanren.org http://minikanren.org
philip-b 2y ago
I read it 2 years ago while I was sick with COVID. It was a lot of fun, it was pretty easy, but also very interesting. It was not a big time commitment. I learned a lot about dependent types. I recommend it.
emmanueloga_ 2y ago
For those looking for a more straightforward approach to type systems, here are two resources I like: 1: Terence Parr's chapter "Enforcing Static Typing Rules" from Language Design Patterns. 2: Eli Bendersky's Python implementation of Hindley-Milner type inference. -- 1: https://pragprog.com/titles/tpdsl/language-implementation-patterns/ https://pragprog.com/titles/tpdsl/language-implementation-pa... 2: https://eli.thegreenplace.net/2018/type-inference/ https://eli.thegreenplace.net/2018/type-inference/

179 points by aarestad 2y ago

Three past discussions with discussion: https://news.ycombinator.com/item?id=18046745 https://news.ycombinator.com/item?id=18046745 - Sept 22, 2018 (132 comments) https://news.ycombinator.com/item?id=31465368 https://news.ycombinator.com/item?id=31465368 - May 22, 2022 (23 comments) https://news.ycombinator.com/item?id=33162971 https://news.ycombinator.com/item?id=33162971 - Oct 11, 2022 (96 comments)

deleted 2y ago
[deleted]

kevindamm 2y ago

I liked the dialogue-driven format of this and the others in the series (I've read Schemer and Learner too), at least once I got used to the split-mind feel of it, but I feel it would be better as an interactive media instead of the books. There's an expectation that you're following along and typing nearly every line into the appropriate REPL. I found this difficult to do while juggling the hardcopies and not any easier on an ebook reader -- I could stop worrying about cracking the spine but the digital copies I sampled or purchased always completely ruined the typesetting. All the REPL interactions are transcribed as images, and the constant focus-and-pinch-zoom disrupts the engagement. I ended up just reading through and hoping to catch enough of the gist of things then doing my usual side-project-as-learning instrument thing. I hope somebody tries to build an interactive playground for this book or the Little Learner, complete with guiding dialog. The typesetting in the hardcopies is really unique and impressive.

ahelwer 2y ago

I worked through this a few years ago and it is wonderful, but I found chapter 9 on the replace function totally impenetrable, so I wrote a blog post in the same dialogue style intended as a gentler prelude to it. A few people have emailed me saying they found it and it helped them. https://ahelwer.ca/post/2022-10-13-little-typer-ch9/ https://ahelwer.ca/post/2022-10-13-little-typer-ch9/

crdrost 2y ago
This is great for me for a completely auxiliary reason, which is that I wanted to know whether this was just gonna be a book about programming Fibonacci numbers into types or some ish... and in some ways it's kinda worse, at chapter 9 you are still proving that different takes on x→x+1 are the same. (But using rewrite rules seems kinda interesting in the abstract I guess.)
- ahelwer 2y ago
  This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same author, which is freely available online!

758758 2y ago

[flagged]

kccqzy 2y ago

I bought this book when it first came out. Unfortunately this book required a time commitment greater than what I had available at that time and I didn't finish. It's thoroughly enjoyable (at least the first few chapters) but it requires a level of thinking that might not be available if you just finished a day of work.

RedNifre 2y ago

Is there an online community for this where you can ask questions? E.g. a discord server or an IRC channel?

nextos 2y ago
I don't think there's a centralized community for the Little Series. I think this is unfortunate. With a community, some great titles like The Little MLer (typed FP) and A Little Java, a Few Patterns (OOP) would be much better known. I found those two outstanding. I think A Little Java has been reprinted. But last time I checked, The Little MLer was bloody expensive. Standard ML, OCaml and F# need a lot more exposure. They are simple and practical. The Little MLer does a great job introducing the basics. To close the circle, the Little Series is missing a book about concurrent and distributed paradigms à la Erlang. They already have functional programming, typed functional programming, declarative programming, dependent types, theorem proving, object-oriented programming and machine learning.
soegaard 2y ago
You are welcome in the Racket Discord. https://discord.com/invite/racket-571040468092321801 https://discord.com/invite/racket-571040468092321801
- RedNifre 2y ago
  Thank you! I joined, but don't see a place for Pie, so I just asked about it in the beginner channel instead.
ysangkok 2y ago
The Gay Haskell discord server has a channel for dependent types. There is also a discord server for Type Theory Forall, a podcast.

ducktective 2y ago

What modern scheme is best to use for these "the little x'er" book series? Some of them suggest their dialect (like learner suggests Racket I think), but what about others? In short, what scheme is the most practical and useful nowadays? Here is the result of my research so far, in order of preference according to the above requirements: Guile: most active community, GNU glue language, Guix Chicken: most pragmatic one with a package manager but older Chez: most performant one, less active community and libraries

RedNifre 2y ago
This one comes with its own language, "Pie", which you can use in DrRacket with #lang pie
4ad 2y ago
I don't know what is the best Scheme implementation, but this book has little to do with Scheme though. Pie uses S-expressions for syntax, and happens to be implemented in Racket, but you don't interact with Racket directly.
- matrix12 2y ago
  Gerbil scheme works great with the Schemer series of books.
deleted 2y ago
[deleted]
nextos 2y ago
Guile is great, but I think outside Guix it's pretty niche. Racket is probably the most frequent choice. But I really like some aspects of Chicken, Gambit and Bigloo. Even Clojure or CL could also be used, with a bit of friction of course.
davexunit 2y ago
Guile is my Scheme of choice.
wk_end 2y ago

ProllyInfamous 2y ago

As a retired electrician attempting hobby-level "learn to code" (i.e. I don't know anything about modern programming and did not even understand anything from OP's link), this Amazon review helped me understand OP's link: >..I’ve been (slowly) working my way through The Little Typer. It’s a deep dive on dependent types, starting with the very basics and building up a toy language one step at a time. I can feel it gradually changing how I think about programming (heck, how I think about thinking). >..It’s really, really enjoyable. The format is very approachable, even fun. Rigorous and demanding, yet doesn’t take itself too seriously. Some lisp experience is helpful, but probably (maybe?) not necessary. But do yourself a favor and learn lisp anyway ;-) Maybe some day I'll motivate myself to even figure out how to first install Racket/Pie (first, I have to figure out what even these are). Thanks for the motivation/educational resource, OP.

rgrmrts 2y ago
I’d recommend the earlier book in the series, The Little Schemer, for what it’s worth! It’s more aimed towards beginners. Similar format to this book.
- ProllyInfamous 2y ago
  >The Little Schemer Inially wasn't sure if your comment was "a joke," but thanks for the real introduction: amazon.com/Little-Schemer-Daniel-P-Friedman/dp/0262560992/ [link to book]
  - Jtsummers 2y ago
    https://mitpress.mit.edu/author/daniel-p-friedman-4089/ https://mitpress.mit.edu/author/daniel-p-friedman-4089/ - one of the authors on all the books in the series. The Little Schemer and The Seasoned Schemer are both beginner books using Scheme. The Reasoned Schemer uses Scheme + Minikanren, an extension of Scheme that allows for logical/relational programming (look up Prolog and Datalog as languages in the same vein). The Little Typer is the linked book covering type systems and, specifically, dependent typing. The Little Learner covers machine learning. The Little Prover uses the same format and has you develop proofs. Little, Seasoned, and Reasoned are, IMO, the better books in the series to start with. I found the later ones to be good but very dense and not always as clear, had to step back a lot more and reread sections. That's mostly due to the material being much harder and more technical than the earlier books, not a quality issue with the writing itself. My recommend reading order for someone with no Racket, Scheme, or Lisp experience wanting to tackle the series would be: Little -> Seasoned -> [Optional: Reasoned] -> {Any order: Prover, Typer, Learner}. I think Prover may be better before Typer, but it's been a while since I looked at either, so a soft recommendation of Prover -> Typer. If you have some Racket, Scheme, or Lisp experience, I'd suggest to either skim the first couple books to get used to the format or skip them entirely and use Reasoned as your first book in the series. http://minikanren.org http://minikanren.org

philip-b 2y ago

I read it 2 years ago while I was sick with COVID. It was a lot of fun, it was pretty easy, but also very interesting. It was not a big time commitment. I learned a lot about dependent types. I recommend it.

emmanueloga_ 2y ago

For those looking for a more straightforward approach to type systems, here are two resources I like: 1: Terence Parr's chapter "Enforcing Static Typing Rules" from Language Design Patterns. 2: Eli Bendersky's Python implementation of Hindley-Milner type inference. -- 1: https://pragprog.com/titles/tpdsl/language-implementation-patterns/ https://pragprog.com/titles/tpdsl/language-implementation-pa... 2: https://eli.thegreenplace.net/2018/type-inference/ https://eli.thegreenplace.net/2018/type-inference/