[HN Gopher] The Little Typer (2018)
___________________________________________________________________
The Little Typer (2018)
Author : bmer
Score : 258 points
Date : 2022-10-11 13:15 UTC (9 hours ago)
(HTM) web link (thelittletyper.com)
(TXT) w3m dump (thelittletyper.com)
| indoorskier wrote:
| A 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.
| emmanueloga_ wrote:
| For 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-
| pa...
|
| 2: https://eli.thegreenplace.net/2018/type-inference/
| deltasevennine wrote:
| Is there a book like this that's for people who know absolutely
| nothing, but has more explanations?
| all2 wrote:
| The Little Schemer is probably this.
| deltasevennine wrote:
| Yeah I read this, scheme doesn't involve types.
| ripley12 wrote:
| Hmm, 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 wrote:
| I'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.
| mcguire wrote:
| For dependent types? I'm really fond of _Type Driven
| Development With Idris._
| nickdrozd wrote:
| Dependent 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
| pkrumins wrote:
| This space reserved for JELLY STAINS!
| sva_ wrote:
| (2018)
| weavie wrote:
| I'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?
| tel wrote:
| It 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.
| kccqzy wrote:
| No.
|
| 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/
|
| 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?
| emmanueloga_ wrote:
| No 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.
| tominated wrote:
| I'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 wrote:
| Actually the dependent type view gives clarity to thinking of
| type level functions, like container types parameterized over
| an element type.
| thomasfromcdnjs wrote:
| This is just a market site yeah? nothing that I can sample?
| benjaminjosephw wrote:
| Here'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
| svnt wrote:
| Not even a description anywhere that I can find on mobile.
| nequo wrote:
| Click "Look inside" on the book's Amazon page.
| mbrodersen wrote:
| A 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".
| petesergeant wrote:
| There is a large sample of this available on Amazon's "Look
| Inside"
| adamgordonbell wrote:
| A 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://corecursive.com/023-little-typer-and-pie-language/
|
| https://davidchristiansen.dk/tutorials/nbe/
| specialp wrote:
| I 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 wrote:
| Thanks 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...
| .
| airstrike wrote:
| Pie reference docs, in case you'd skim something before
| committing to the book: https://docs.racket-lang.org/pie/
| ekidd wrote:
| This 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/
|
| - ATS. This is a complex systems-level language with dependent
| types: 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 wrote:
| For others: I think what was meant was "The Reasoned Schemer":
| https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/
| ekidd wrote:
| Fixed. Thank you!
| klabb3 wrote:
| > [Dependent types] 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".
|
| As a curious bystander, what else? When are dependent types
| useful in practice? How do they fit into software development
| practices such as testing and DRY?
|
| As an example of what I'm looking for, I see _regular static
| typing_ as a way to move a class of runtime errors to compile
| time errors, increasing your confidence in aspects that
| otherwise would need repetitive unit tests.
| mcguire wrote:
| One interesting aspect, at least for us old systems guys
| where runtime is important, is that you can not only move
| errors into compile time, you can move validation checks into
| compile time.
|
| Simple example: returning the head of a list is partial;
| normally, you have to have a check if the list is empty and
| return an error. With dependent types, you can guarantee that
| the list is not empty, moving that test to some higher level
| where it's actually meaningful.
|
| If you're manipulating arrays, you can guarantee at compile
| time that the indices have the right values, moving the tests
| outside of a function that gets called often. (In fact, when
| I was playing with ATS, this is what I did: I picked one
| boring validation test in the code at a time and moved it
| into the type. It vastly simplified the code.)
| [deleted]
| Atiscant wrote:
| One way to think about it is that you can extend your testing
| to prove the correctness of your program up to some notion of
| what "correct" means. You can reason about your program in
| your program and that allows you to capture another class of
| errors than regular static typing does. In principle, a
| strong enough dependent type systems allows you to encode
| mathematics, and you can then prove thing about your program
| in the same language as your are writing it. As for practical
| examples, you should look at Idris and some of the talks
| given about it. They do very fancy things while still being
| somewhat performant. Besides errors and testing, having
| dependent types also allows your IDE to reason about your
| program and can give much stronger hints and code completion.
|
| But I agree that it is often a hard sell for normal
| developers. Given the choice, I would happily write large
| code bases in a dependent language, but I am also very biased
| having worked a lot in them.
| Warwolt wrote:
| One really nice "everyday" example that comes from Idris
| that I really like is the ability to typecheck a printf
| function. You provide the format string, and then the
| typechecker will know what to expect from the rest of the
| arguments!
|
| Usually that is implemented in C compilers, so that
| "printf("%d", 2.3f)" becomes an error, but with dependent
| types you can do it on the user level in library code.
| dwenzek wrote:
| And here is a gist that demonstrates how simple it is to
| implement such a type-safe printf function:
|
| https://github.com/mukeshtiwari/Idris/blob/master/Printf.
| idr
| zasdffaa wrote:
| It seems to be doing string ops at compile time and
| emitting a suitable function eg. format
| ('%' :: 'd' :: cs ) = FInt ( format cs )
|
| Does that make it a bit like template metaprogramming if
| TM could disassemble strings?
| ZitchDog wrote:
| This is also possible in typescript which is a little
| more mainstream than Idris.
| naasking wrote:
| TypeScript's type system is not consistent though.
| klabb3 wrote:
| I was gonna say that's possible in Rust and also isn't a
| big problem but the more I think about it the more this
| comes up.
|
| First, languages where a compiler plug-in or linter do
| this don't really count, because you can't extend it and
| they rely on specific tools. Even Rust, which has
| relatively good meta-programming, is very cumbersome to
| use. Writing proc macros is known as an archaic skill
| that - even though it is technically also in Rust (which
| is nice) - involves heavy manipulation of ASTs and has
| numerous pitfalls. It would be better to leave the ASTs
| for compiler folks if possible.
|
| It get the sense that these features can be really useful
| for deserialization, which is a very common use-case in
| regular software development. Even where it's safe, like
| in Rust, deserialization is prone to logic errors and
| often requires lots of boilerplate (unless you use an
| existing library but then you must rely on unintelligible
| proc macro wizardry).
| gdprrrr wrote:
| One example I like is a binary search Funktion which only
| allows to pass a sorted list
| dunham wrote:
| Internally, the Idris2 compiler uses deBruijn numbering for
| its terms, which is tricky to get right once you start trying
| to manipulate terms. To help with this, it keeps a list of
| the names corresponding to the deBruijn indices at the type
| level. The type checker catches mistakes as you write code to
| manipulate them (inserting names, removing names, or renaming
| things).
|
| I ran through some exercises teaching this technique[1]. My
| take-away as a beginner was that it was a pain to make the
| compiler happy and my code that the compiler didn't like was
| actually wrong.
|
| I remember reading someone had written a functional red-black
| tree (with proof of correctness leveraging dependent types)
| and said the delete algorithm naturally followed from the
| types. That has was not my experience (delete wasn't
| immediately obvious to me), but I need to find some time to
| give it another go.
|
| The Idris2 docs have an example of a lambda expression
| interpreter[2] whose terms have a vector of the types in the
| environment as a type parameter (erased at runtime), to
| ensure everything is type safe in the resulting interpreter.
|
| Typescript has added some bits of dependent typing. For
| example, asserting a function returns true if the argument
| has type X, that a function throws if the argument is falsy,
| and I think type level string manipulation. They are fairly
| pragmatic, it's not a research language, so I presume that
| specific functionality is useful to a lot of people. I've
| used it a little bit of it to help the type checker infer
| non-null after my assert function was called.
|
| All of that said, I think people are still exploring how
| dependent types can be used in practice.
|
| [1]: https://github.com/edwinb/SPLV20/blob/master/Code/Lectur
| e2/E... [2]:
| https://idris2.readthedocs.io/en/latest/tutorial/interp.html
|
| There is a copy of #1 at github.com/dunhamsteve/SPLV20 that
| is updated to work with the latest Idris2.
| agumonkey wrote:
| I have a different pov about this. It's an intellectual need
| to encode logic at the type level. It's not showing lots of
| practical value yet.. just like most interesting and generic
| techniques in the mainstream today.
| Warwolt wrote:
| Dependent types allow for more nuanced statements made by
| types. You can for instance have a lists that are sorted in
| ascending order as a type, or implement messaging protocols
| at the type level where you can only construct a reply in the
| message exchange if you've received the correct preceding
| message.
|
| It's very cool, but it's very expensive to compile, which is
| why it's still research stuff, I believe.
| zasdffaa wrote:
| IIUC, you can use it to ensure you never index outside the
| limits of your static array at runtime, this check being done
| at compile time.
| [deleted]
| wk_end wrote:
| > It is also possible, to some extent, to use dependent types
| to replace proof tools like Coq.
|
| Not sure what you mean here - Coq is a proof tool _based on_
| dependent types. It's a dependently typed programming language
| with a mechanism for constructing proof terms in an (arguably)
| more pleasant or natural way bolted on top.
| Jtsummers wrote:
| They probably mean that bringing dependent types into a
| programming language, proper, partially obviates the need for
| Coq and similar systems since it renders them (at least
| partially) redundant. Having dependent types, and having
| mechanics in-language to produce proofs, would cover a large
| part of what people (who are producing programs and not
| focused strictly on the theorem proving side for other
| purposes) are using Coq & others for.
| PaulHoule wrote:
| I think variants of Datalog have some traction
|
| https://en.wikipedia.org/wiki/Datalog
|
| full Prolog though is not that great of a language. At first it
| looks clever that you can write imperative code by taking
| advantage of the implementation but it's actually really
| awkward. It was hoped that you could parallelize Prolog but you
| can't unless you weaken the language and make it even more
| awkward.
| haskellandchill wrote:
| > 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.
| ekidd wrote:
| Here's my reasoning on why dependent types may still be a
| couple of language generations from the mainstream:
|
| - Dependent types are hard to retrofit onto an existing
| language. (Retrofitting generics has had very mixed results,
| and dependent types are likely harder to retrofit?)
|
| - It takes a good 10 years for a new language to really hit
| the mainstream, even if everything goes right. (This could
| change if a big player pushes a language.)
|
| - All type systems represent a tradeoff, "Roughly how much
| extra confidence can I get in this program, and for how
| little extra time spent learning and coding?" Dependent types
| give you some very interesting new guarantees, but they
| require picking up new skills. But a future language in this
| space might make these tradeoffs more appealing!
|
| - I'm not sure that any of the existing dependently-typed
| languages have hit the magic combination of features and
| tools that would be needed to break out.
|
| In the nearer term, I can imagine dependent typing showing up
| in at least two niches:
|
| 1. If you're currently writing extremely high-assurance
| software, the sort of thing where you write a proof in Coq
| and then use that to generate C code, then something similar
| to Idris might be a win. Ditto for some people using model-
| checker tools like TLA+?
|
| 2. I could imagine a dependent type system being "bolted on"
| to unsafe Rust to formally verify correctness of code that
| regular Rust can't verify. This might require using Rust
| attributes and an external tool. But I could see it happening
| if somebody loved the _The Little Typer_ and wanted an
| ambitious thesis project, for example.
|
| But even though I don't expect dependent types to go
| mainstream in the next 5-10 years, they're one of those ideas
| than might occasionally contribute a major inspiration to a
| challenging project.
| ajross wrote:
| > Dependent types are hard to retrofit onto an existing
| language.
|
| Dependent types are hard to retrofit onto existing
| _problems_. Software everywhere wants to work with data of
| indeterminate size /parametrization at runtime. You want
| your system that tracks inventory stock to work with three
| warehouses or four, etc... Dependent types make all that
| stuff part of the type system, so now "list of 3
| warehouse_t" and "list of 4 warehouse_t" are no longer
| equivalent.
|
| Obviously that's all "solvable", but not in a way that
| matches the intuition of generations of hackers who have
| been building these systems. It's in some sense analogous
| to Haskell's "Death by a Thousand Monad Tutorials". At some
| point you just have to recognize that this isn't the right
| metaphor for the problem areas it's trying to address and
| move on.
| [deleted]
| mcguire wrote:
| Your point is good, but your example isn't. :-)
|
| A dependent type can easily express "list of n
| warehouse_t's where 0 < n <= 1,000,000,000".
| ajross wrote:
| Not if the input data isn't known at compile time it
| can't. I get what you're saying, and admit that my
| example was glib and short, but the point remains:
| putting "state" data into the type system forces
| programmers to be explicit about things that were just
| part of the algorithm before.
|
| The word "automagical" is a term of art for a reason.
| It's an ideal that our ancestors have been baking into
| the concept of "good code" for decades and decades, and
| dependent types throw it in the trash in favor of a
| variant idea of "correctness" that IMHO doesn't
| correspond to what society actually wants its computers
| to do for it.
| rowanG077 wrote:
| Sure it can. It can be as simple as this (pseudo code):
|
| warehouses = get_warehouses_via_io()
|
| if len(warehouses) == 0: -- Here you
| have a proof warehouses is empty return
| Err("Oh no couldn't get warehouses")
|
| else if len(warehouses) > 10000: --
| Here you have a proof warehouses contains more then 10000
| elements.
|
| else: -- Here you have a proof that the
| amount of warehouses is not 0 and not larger then 10000
| or you have between 1 and 10000 inclusive warehouses
| do_stuff(warehouses)
|
| Even Haskell which barely has dependent typing can do
| that. You simply have to introduce a proof that your
| lists length is between those.
| ajross wrote:
| Once again, I'm not saying you can't do it. I'm saying
| that doing it requires filling your app with that sort of
| boilerplate nonsense when five decades of software
| engineering have been trying to remove it and considering
| it good practice to have done so.
| rowanG077 wrote:
| If statements are boilerplate? How else would you do
| branching? Gotos? There are definitely cases where
| dependent types add a lot of boilerplate. But it's not
| these simple cases. And guess what. You pay for what you
| use. If you don't want to prove something and just run
| your program then you can just do it.
| mcguire wrote:
| By "boilerplate nonsense" do you mean input validation?
|
| Because that is all that is.
| haskellandchill wrote:
| > Not if the input data isn't known at compile time it
| can't
|
| look at the idris example of printf (https://gist.github.
| com/chrisdone/672efcd784528b7d0b7e17ad9c...) for how to
| do this, the idris book has some really good example of
| how you can handle what you would think is "not known at
| compile time" but can actually be parameterized
| mcguire wrote:
| The big problem I see with dependent types is that they
| ultimately require doing proofs whether you're using proof
| assistants like Coq or model checkers like (normal :-))
| TLA+. Proofs are hard, for those who haven't had the
| training and experience (the coding bootcamp goes right
| out), and proof software is bizarre, opaque, and normal
| manual proof techniques don't apply or are difficult to
| translate.
|
| That being said, things like Ada SPARK and Frama-C are the
| same sort of tools as dependently typed languages, but are
| more from the assertion model and so use imperative code
| rather than tossing functional language on top of
| everything else.
| jjtheblunt wrote:
| > 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.
|
| why have an expectation one way or the other? the
| sophistication of compile-time analyses added to, e.g., Rust
| seems a plausible place such might appear.
| ogogmad wrote:
| HoTT?
| all2 wrote:
| What is this?
| mcguire wrote:
| Higher Order Type Theory.
|
| No idea beyond that.
| jsmorph wrote:
| [0] https://en.wikipedia.org/wiki/Homotopy_type_theory
|
| [1] https://homotopytypetheory.org/book/
| all2 wrote:
| From [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.
| dang wrote:
| Related:
|
| _Book review: The Little Typer (2021)_ -
| https://news.ycombinator.com/item?id=31465368 - May 2022 (23
| comments)
|
| _The Little Typer_ -
| https://news.ycombinator.com/item?id=18046745 - Sept 2018 (132
| comments)
| [deleted]
| ahelwer wrote:
| I'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 wrote:
| Yup - 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-...
| nickdrozd wrote:
| Idris 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.
___________________________________________________________________
(page generated 2022-10-11 23:00 UTC)