12 ms·
The Little Typer (2018)
- adamgordonbell 4y agoA very mind-blowing and challenging book about Types. The strange loop talk and my own interview of the authors might give some sense of what it's all about. There is also some interesting work online showing how the language used in the book can be created. https://www.youtube.com/watch?v=VxINoKFm-S4 https://www.youtube.com/watch?v=VxINoKFm-S4 https://corecursive.com/023-little-typer-and-pie-language/ https://corecursive.com/023-little-typer-and-pie-language/ https://davidchristiansen.dk/tutorials/nbe/ https://davidchristiansen.dk/tutorials/nbe/
- specialp 4y agoI was at that talk by David which is the first link. Highly recommended watch, he is such a good presenter. The way he went full circle there and had the room in raucous applause at the end was something I never forgot.
- d_christiansen 4y agoThanks for the links! If Haskell is more your style than Racket, there's a Haskell version of the implementation tutorial at https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf https://davidchristiansen.dk/tutorials/implementing-types-hs... .
- nequo 4y agoThe Strange Loop talk was very enjoyable. You are a gifted public speaker. And I just want to say that I am excited to read your book on Lean in full, too!
- indoorskier 4y agoA beautiful book, written in the "The Little..." series' question and answer format. A challenging topic but just about as accessible as I can think anyone can make it. Warmly recommended if you want to know what dependent types are all about.
- sva_ 4y ago(2018)
- thomasfromcdnjs 4y agoThis is just a market site yeah? nothing that I can sample?
- nequo 4y agoClick "Look inside" on the book's Amazon page.
- benjaminjosephw 4y agoHere's a Strange Loop talk where one of the authors covers some of the content of the book: https://www.youtube.com/watch?v=VxINoKFm-S4 https://www.youtube.com/watch?v=VxINoKFm-S4
- svnt 4y agoNot even a description anywhere that I can find on mobile.
- petesergeant 4y agoThere is a large sample of this available on Amazon's "Look Inside"
- pkrumins 4y agoThis space reserved for JELLY STAINS!
- deleted 4y ago[deleted]
- weavie 4y agoI'm intrigued. Will this book do anything to help me become a better Rust developer, or will it only be valuable if I start using languages like Idris or Agda?
- tominated 4y agoI've read through maybe half and doubt you'll find it useful for Rust development. If you're interested in learning a dependently typed language it is fantastic though.
- haskellandchill 4y agoActually the dependent type view gives clarity to thinking of type level functions, like container types parameterized over an element type.
- tel 4y agoIt may help you to have a more firm grasp of how a type system and its value language interact. Which is important in understanding any language with a sophisticated type system, Rust included. But it'll be fairly marginal, I suspect.
- emmanueloga_ 4y agoNo and no. Err, no. :-p IMHO learning Rust is the most effective way of learning Rust... This is half tongue in cheek but really, this book is not even my fav when it comes to learning about type checking and type inference, simply and quickly (see my other comment in this post). Also I feel like the really different thing about rust when comparing to other strictly typed languages is actually the borrow checker. Honestly i have no idea how it's implemented, or if this book will help you build one. Maybe someone in here may know.
- kccqzy 4y agoNo. In fact if you're intrigued I recommend you read the TAPL book first as a prerequisite for this book: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ Even then, it might not be suitable for you because learning to be a developer in a language is very different from being an expert in the implementation of a language (specifically the type checker). Just flip to the appendix of the book and look at those type deduction rules; do they interest you?
- ekidd 4y agoThis is one of my two favorite books in The Little <X>er series. The other is The Reasoned Schemer. The Little Typer provides an introduction to dependent types. These can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Two interesting languages using dependent types are: - Idris. This is basically "Haskell plus dependent types (and minus lazy evaluation)": https://www.idris-lang.org/ https://www.idris-lang.org/ - ATS. This is a complex systems-level language with dependent types: http://www.ats-lang.org/ http://www.ats-lang.org/ This fills a niche (vaguely) similar to Rust and Ada Spark, with a focus on speed and safety. The Reasoned Schemer shows how to build a Prolog-like logic language as a Scheme library. This is a very good introduction to logic programming. And the implementation of backtracking and unification is fascinating. (Unification is a powerful technique that shows up in other places, including type checkers.) This is an excellent series overall, but these two books are especially good for people who are interested in unusual programming language designs. I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they're still fascinating.
- sixbrx 4y agoFor others: I think what was meant was "The Reasoned Schemer": https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/ https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/
- ekidd 4y agoFixed. Thank you!
- haskellandchill 4y ago> I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages I do, these are low hanging fruits for improving software engineering practices.
- 4y ago
- ahelwer 4y agoI've been reading through this and greatly enjoy it - up until chapter 9, which is like a giant boulder that tumbled to block a nice hiking trail. The definition of replace is very weirdly presented compared to everything that has come before, and in reality it isn't even very difficult to understand! It's just a way of rewriting expressions using known/existing statements of equality, which is a very basic operation in dependently-typed proof languages like Lean. A few other reviews I've found online also mention difficulty with chapter 9. Maybe I'll write a blog post that re-writes the introduction to this chapter so others aren't stopped in their tracks like I was. If I weren't on sabbatical and had other work concerns I probably would have quit reading the book here. Chapters 1-6 I only needed to read once, chapter 7 (introducing induction) I had to read twice, and chapter 8 (introducing inductive proofs of equality) I also read twice. Chapter 9 I'll probably read at least twice (although getting started reading it was the hard part) and allegedly the book is much less difficult after this point. I'm using this book to deepen my understanding of the Lean theorem proving language. It's a testament to how well the dependent type checking/theorem proving equivalence works that I've used Lean a fair bit without understanding at all that I was just writing a program to construct a value whose type is the theorem I am trying to prove.
- ThatGeoGuy 4y agoYup - I had a similar experience [1]. Chapter 9 is certainly the weakest part of the book but it picks up very quickly thereafter. [1] https://www.thatgeoguy.ca/blog/2021/03/07/review-the-little-typer/ https://www.thatgeoguy.ca/blog/2021/03/07/review-the-little-...
- ahelwer 4y agoWell, I did it. I wrote an extended dialogue explaining the replace function as a blog post: https://ahelwer.ca/post/2022-10-13-little-typer-ch9/ https://ahelwer.ca/post/2022-10-13-little-typer-ch9/ I'd found your review a week or so ago which was nice since it reassured me I wasn't the only person having trouble with it.
- nickdrozd 4y agoIdris has a replace function, and it's hard to understand and use there too. I consider its use to be a code smell, and in my experience replace expressions can always be rewritten in other ways to be clearer and less verbose.
- airstrike 4y agoPie reference docs, in case you'd skim something before committing to the book: https://docs.racket-lang.org/pie/ https://docs.racket-lang.org/pie/
- ogogmad 4y agoHoTT?
- all2 4y agoWhat is this?
- mcguire 4y agoHigher Order Type Theory. No idea beyond that.
- jsmorph 4y ago[0] https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory [1] https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/
- all2 4y agoFrom [1] > Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids. Homotopy type theory offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant. We believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians. This sounds fascinating, especially the idea of swapping out set theory as a foundational idea.
- mbrodersen 4y agoA number of modern languages (F-star, LEAN, Coq, Agda, Idris, …) use Dependent Types. It enables you to prove code correct using just the type system. Very cool. I highly recommend the book “Type Driven Development”. I prefer that to “The Little Typer”.
- nickdrozd 4y agoDependent types are very cool and very frustrating. Once you get it, it opens up a whole new way to express program behavior; but until then, it all seems like pointless busywork. The Little Typer is somewhat tougher to get through than other Little books because the benefits of the paradigm it explains aren't apparent until you understand everything. For anyone struggling to make sense of it, I suggest looking at the end of chapter 15, where a proof that the Principle of the Excluded Middle is not false is derived step by step. I found it analogous to the derivation of the Y combinator from The Little Schemer in terms of being a "holy shit" moment. ThatGeoGuy's review gives a nice overview of the book's contents. I also wrote a detailed review that discusses what's cool and what's frustrating about the book: https://nickdrozd.github.io/2019/08/01/little-typer.html https://nickdrozd.github.io/2019/08/01/little-typer.html
- dang 4y agoRelated: Book review: The Little Typer (2021) - https://news.ycombinator.com/item?id=31465368 https://news.ycombinator.com/item?id=31465368 - May 2022 (23 comments) The Little Typer - https://news.ycombinator.com/item?id=18046745 https://news.ycombinator.com/item?id=18046745 - Sept 2018 (132 comments)
- deltasevennine 4y agoIs there a book like this that's for people who know absolutely nothing, but has more explanations?
- all2 4y agoThe Little Schemer is probably this.
- ripley12 4y agoHmm, I don't think so. This book is about dependent types, The Little Schemer is more about introducing Lisp/Scheme fundamentals. FWIW I found The Little Schemer remarkably devoid of essential context; I found myself wondering "that's interesting, but why is it important?" far too often.
- all2 4y agoI've run into something similar going through these books. For me to be successful in going through these and understanding the importance of each piece, I think I'd need a project per-chapter to help me gel what I've learned.
- deltasevennine 4y agoYeah I read this, scheme doesn't involve types.
- mcguire 4y agoFor dependent types? I'm really fond of Type Driven Development With Idris.
- emmanueloga_ 4y agoFor a way more practical introduction to coding a simple type checker I like [1]. For a practical intro to type inference I love the articles on Eli Bendersky's blog [2]. Follow the links to learn also about underlying concepts (unification, logic programming, etc). -- As an aside, I know a lot of people love the "The little ...X..." series of books but in my personal opinion they are unnecessarily cryptic. For me, the supposedly pedagogical style of teaching feels confusing and frustrating. Not sure what came first, but that book series make me think of a trend that possibly started with "_why's poignant guide to Ruby". I just feel like at this point of my life I'm a cranky programmer that just wants to get things done. The extra "sugar" and whimsy does nothing for me. I know, I know... I must sound like a party pooper... Sorry if you like these books... I just feel like there's a lot of praise for them and not much of a counter opinion, so i thought i would share mine :-). -- PS. I used to be dismissive of blog posts when comparing to books, but I eventually discovered that there are subjects that are way better documented from individual blog authors, often demoing with ++working code++ in languages widely popular like python or JavaScript! I'm very grateful to these people that take the time and effort to share they knowledge and I'm sorry I did not come to this realization earlier in my career. -- 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/
- transfire 4y agoI agree with you. I’ve gotten about halfway and I don’t like the style. It lacks some much needed explanations. And while I can appreciate levity, too much of this book is frivolous chatter, IMO.