[HN Gopher] The Little Typer (2018)
___________________________________________________________________
The Little Typer (2018)
Author : aarestad
Score : 111 points
Date : 2024-09-28 14:54 UTC (8 hours ago)
(HTM) web link (thelittletyper.com)
(TXT) w3m dump (thelittletyper.com)
| Jtsummers wrote:
| Three past discussions with discussion:
|
| https://news.ycombinator.com/item?id=18046745 - Sept 22, 2018
| (132 comments)
|
| https://news.ycombinator.com/item?id=31465368 - May 22, 2022 (23
| comments)
|
| https://news.ycombinator.com/item?id=33162971 - Oct 11, 2022 (96
| comments)
| kevindamm wrote:
| 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 wrote:
| 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/
| crdrost wrote:
| 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 wrote:
| 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!
| kccqzy wrote:
| 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 wrote:
| Is there an online community for this where you can ask
| questions? E.g. a discord server or an IRC channel?
| soegaard wrote:
| You are welcome in the Racket Discord.
|
| https://discord.com/invite/racket-571040468092321801
| RedNifre wrote:
| Thank you! I joined, but don't see a place for Pie, so I just
| asked about it in the beginner channel instead.
| nextos wrote:
| 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 a la Erlang. They already
| have functional programming, typed functional programming,
| declarative programming, dependent types, theorem proving,
| object-oriented programming and machine learning.
| ysangkok wrote:
| The Gay Haskell discord server has a channel for dependent
| types. There is also a discord server for Type Theory Forall, a
| podcast.
| ducktective wrote:
| 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 wrote:
| This one comes with its own language, "Pie", which you can use
| in DrRacket with #lang pie
| 4ad wrote:
| 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 wrote:
| Gerbil scheme works great with the Schemer series of books.
| nextos wrote:
| 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 wrote:
| Guile is my Scheme of choice.
| wk_end wrote:
| A book like this doesn't need to be "practical" and "useful" -
| I don't think, say, the shortage of libraries for Chez Scheme
| is going to hamstring you in anyway.
| ProllyInfamous wrote:
| 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 wrote:
| 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 wrote:
| >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 wrote:
| 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
| jfoutz wrote:
| Friedman's books are all great. All of them. But they don't
| work for everybody.
|
| If you can be relaxed and think of the interaction as play,
| they're very good. If you're feeling more of a "serious
| business" mindset, it can be hard to get in the groove of
| his style.
|
| There are a lot of jokes about food and encouragement to
| take breaks. If you can get into the learning as play
| mindset, I'd strongly encourage taking the recommended
| breaks. maybe grab a snack, but spend some time noodling
| around with the ideas in each section. I think that's the
| real point, food is a good excuse to pause and get your
| hands off the keyboard.
|
| Racket should be easy to install. Big download button for a
| ton of platforms here - https://racket-lang.org
|
| I believe HN still runs on the racket runtime. it may
| appear to be a toy, but thoughtful design can take you a
| long long way. it's well supported and a great way to get
| started.
|
| If Friedman doesn't work out for you, the racket docs link
| to how to design programs -
| https://htdp.org/2024-8-20/Book/index.html Which is also
| pretty darn good.
|
| The other classic is the wizard book -
| https://sarabander.github.io/sicp/html/index.xhtml the
| structure and interpretation of computer programs. This'll
| walk you up to and somewhat through compilation.
|
| There are a ton of programming languages all with amazing
| assortments of features.
|
| Scheme is much more "there's nothing left to take away". I
| think it's very much the undisputed champion in that
| regard. While still being able to ship software. Scheme may
| not be the optimal choice for all people in all situations
| (obviously). It's a spectacular place to start though. It
| may not turn out to be the language for you. That's totally
| fine! But it'll get you deep enough to figure out what you
| like and don't like. And, when it comes down to it, you can
| shape it into pretty much anything.
|
| Yeah, I hope you enjoy the little schemer.
| bmitc wrote:
| Check this course out:
|
| https://www.edx.org/learn/coding/university-of-british-colum...
|
| I think you'll really like it. It uses Racket and is based upon
| the _How to Design Programs_ book. It is absolutely perfect for
| someone new to coding.
| philip-b wrote:
| 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.
___________________________________________________________________
(page generated 2024-09-28 23:00 UTC)