The Little Typer (2018)

(thelittletyper.com)

175 points | by aarestad a day ago ago

41 comments

  • ProllyInfamous a day ago 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 a day ago 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 a day ago 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 a day ago ago

          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

          • nextos a day ago ago

            With no Scheme or programming background, I'd study HtDP (https://htdp.org) as an interlude, after The Little Schemer. Pace is gentle, and explanations about program design are long and very lucid. After those two, I'd try The Little MLer. The other books are quite advanced, better to build solid foundations first.

        • masto 11 hours ago ago

          The Little Schemer is one of my top two favorite programming books. But it's not something I'd recommend as a way to learn how to do the programmer job. It's fun and useful in the way that dropping acid is fun and useful, at least from what I've been told as a teetotaler who's never tried anything stronger than Tylenol. When I read that book, it has a long-lasting aftereffect on how I approach problem solving and maybe the world in general.

          I have non-data-driven (but informed) opinions on how to pick up coding as a new skill. I think it helps to find a hobby space you're interested in that will motivate you to push through when you get stuck on something. There are some great platforms for live-tinkering with electronics, CircuitPython for example. Or web stuff, if there's a way to get into it in 2024 without being overwhelmed by frameworks and complexity.

        • jfoutz a day ago ago

          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.

          • anta40 11 hours ago ago

            So, what's the recommended Scheme implementation to "get things done", and not only for learning CS stuffs?

            For example, now our backend system is mostly implemented in Go (some with Fiber, some with Echo). The rest are pretty common: Postgres, Mongo, Firebase etc.

            Perhaps Gambit? BTW, I have nothing against experimentation. Not everything have to do with practical purpose on mind. That's why I'm also tinkering with Haskell & Ocaml :D

            • rgrmrts 11 hours ago ago

              Racket, Guile, Gambit, Chicken Scheme, chez are all pretty solid with different trade-offs. I think Racket has a fairly decent developer experience and others like chez and gambit are great implementations but may be lacking in tooling (in the sense that you won’t get a nice package manager or build tool). Options exist (like Akku) but IMO the scheme ecosystem is somewhat disjointed.

              Guile integrates well with C, and uses the same build tools as a lot of the GNU ecosystem (make and autotools).

              I recognize the answer isn’t maybe the most helpful but it does exemplify, in my opinion, one of the challenges with using Scheme for getting things done.

              • jfoutz 9 hours ago ago

                100%

                If I had to put scheme in production, I think I'd pick racket. I think that would give me the best chance at helping other dev's get set up, explain the problem, and show the solution. anta40 asked about packages, and racket has the db interaction as part of the normal distribution, I see there's a mongo client in the package manager, but no idea about firebase. I guess wrap the cli?

                Racket has been ported over to the chez backend, and got a big performance pop. And they've done stuff with arrays instead of lists, immutable lists. Pointer chasing is always going to have certain tradeoffs.

                As much as I love scheme, it's going to be a fringe language. Small shop, that can be ok. You need to hire 50 people? yeah, that's not really going to work out I think.

                anta40 also mentiond stuff like Haskell and Ocaml. I feel like those are much easier to refactor, the compiler helps so much, you just chase errors and feel good about code staying correct. scheme, I feel like I just throw it away and start over.

                For personal stuff, language doesn't matter, think harder, you'll find a way out.

                For "team" stuff. Ugh. That really depends on how dysfunctional the team is. I think go is a pretty solid default. But everything is very textured and nuanced. Just you? go with what you know. Wasting time ramping up on a shiny new thing won't ship. You have a mostly working team? Keep doing that. add linters or whatever to improve code quality.

                Screwing around with a weekend project that might turn into something big? Racket seems like the path of least resistance. it's a hard question to answer optimally.

            • tmtvl 8 hours ago ago

              Maybe Gauche (https://practical-scheme.net/gauche/)? It kinda depends on what you want to get done, though. If the thing you want to get done is to make an operating system I guess Loko would be your go-to.

              EDIT: There's also GNU Kawa, which runs on the JVM, so you get all of that Java-y goodness in a language that's actually nice to use.

      • gorjusborg 13 hours ago ago

        I'll second The Little Schemer. I found it weird and wonderful in beautiful way.

    • neilv 11 hours ago ago

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

      If you're retired and don't need to do the Webrogrammer grind of employable skills, that's a great time to learn advanced/alternative topics of programming like this.

      (But if you instead want a paying second career, you probably want to either focus on Web or phone app development instead of this, or have a personal connection to get a job in some less-common area of software development. The Little Typer probably won't help you with that.)

      I suspect that the book will do a good job of explaining its topic, from scratch. Here's how to install the software that the book uses:

      1. https://download.racket-lang.org/

      2. > Open DrRacket and select "Install Package" from the "File" menu. In the package name field, type pie and then click the "Install" button.

    • dunefox 16 hours ago ago

      I'd say a Lisp and books like little Schemer, etc. are a perfect way to study programming and computer science. Later on you could have a look at SICP (Structure and Interpretation of Computer Programs) which also uses Scheme, but is more advanced than Little Schemer. It's one of my all time favourite CS books.

    • bmitc a day ago ago

      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.

  • kevindamm a day ago 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.

  • emmanueloga_ a day ago 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-pa...

    2: https://eli.thegreenplace.net/2018/type-inference/

  • kccqzy a day ago 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.

  • Jtsummers a day ago ago

    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)

    • a day ago ago
      [deleted]
  • ahelwer a day ago 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/

    • crdrost a day ago 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 a day ago 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!

  • RedNifre a day ago ago

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

    • nextos a day ago 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 a day ago ago

      You are welcome in the Racket Discord.

      https://discord.com/invite/racket-571040468092321801

      • RedNifre a day ago 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 a day ago ago

      The Gay Haskell discord server has a channel for dependent types. There is also a discord server for Type Theory Forall, a podcast.

  • philip-b a day ago 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.

  • ducktective a day ago 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

    • sporkl a day ago ago

      Racket! This is the language that the common author (Dr. Daniel Friedman) uses, and many of the Little books use custom DSLs implemented in Racket.

      Racket now runs on Chez under the hood (inheriting the performance), and has a pretty decent ecosystem as far as schemes go.

      (I TA for Dr. Friedman’s programming languages course)

    • RedNifre a day ago ago

      This one comes with its own language, "Pie", which you can use in DrRacket with #lang pie

    • AlchemistCamp 16 hours ago ago

      This is the last thing I'd worry about. The series isn't about teaching you a language you can use later in industry. It's about teaching you higher-level concepts you can take with you to any languages you may encounter in the future.

    • nextos a day ago 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.

    • wk_end a day ago ago

      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.

    • tmtvl 17 hours ago ago

      Guile probably has the best Emacs integration through Geiser. While you don't really need it and you can just follow along with a terminal REPL, using something like Geiser helps keeping the experience smooth.

      MIT/GNU Scheme comes with its own editor, edwin, which is a terminal-only Emacs-like. I don't know how much it complies with the various RnRSes, but I do believe it's good enough to work for the Little series.

      Gauche is R7RS-small (and I believe -large up to Tangerine) compliant so it should just work. It also has fairly good Geiser support and comes with an enormous standard library, 'batteries included' as they say, though its performance is a bit lower than some of the other implementations.

      Cyclone is R7RS-small compliant so it should work. It seems fairly fast and it has a package manager, but because it's fairly new I don't know how well it works with Geiser.

      Loko is R6RS compliant so it should work. I believe the documentation says that it should work with Geiser using the Chez module, but I may be mistaken.

      Gerbil is R7RS-small compliant (and I believe -large through Red, maybe through Tangerine?) so it should work. I believe it's also quite performant, though I haven't used it.

      Kawa is R7RS-small compliant if I'm not mistaken. If so it should work for the Little series. It also has a Geiser module.

      And then there are a few implementations of which I'm not entirely sure which version of the spec they comply with and how well they're supported by various editors (though I think SLIME has Scheme support, although that may only be for MIT/GNU Scheme): Gambit (I think R5RS? Gerbil is built on top of it), Bigloo (I think R6RS?), Larceny, Chibi Scheme, Biwa Scheme, S7, and IronScheme. For any of those, as long as they support post R4RS macros (so using `define-syntax' and `syntax-rules' instead of `defmacro)' they should work for the Little series without any adjustments. If they're still using `defmacro' then you'd need to translate the macro definitions from Reasoned (and later?), which isn't that hard... but if you're gonna do that you may want to read On Lisp after Seasoned.

    • 4ad a day ago 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 a day ago ago

        Gerbil scheme works great with the Schemer series of books.

    • davexunit a day ago ago

      Guile is my Scheme of choice.

    • a day ago ago
      [deleted]
  • 758758 a day ago ago

    [flagged]