14 ms·
The Little Typer
- plafl 8y agoI'm going to order it right now. I highly recommend the little schemer and the seasoned schemer too! I have read all the titles (MLer and Java too) in the series and those are my favorites. The only one I have not finished is the reasoned schemer although I hope to try again in the future.
- nils-m-holm 8y agoDon't miss The Little Prover! :)
- jsntrmn 8y agoI am just now (as of reading your comment) becoming aware of the "Little" series. Is there a particular order in which one should read the books?
- plafl 8y agoLittle Schemer first and Seasoned Schemer second. The other ones are about different independent topics and can be read in any order once you have read the first two ones.
- nigwil_ 8y agoWill there be a Kindle edition eventually?
- georgewsinger 8y agoWhat language does this book use? A dependently typed LISP? Or something Haskelly?
- cmrx64 8y agoit’s a pretty standard type theory lambda calculus, written as sexps because it’s inside racket, but it’s its own thing.
- lylecubed 8y ago> An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time. Is there a companion book detailing the ugly downsides of dependent types and how to avoid them, one step at a time?
- z5h 8y agoCan you elaborate? Do you have war stories?
- KirinDave 8y agoHere is a quick guide to avoiding them: "Unless you are using Haskell at a very high level of abstraction, Coq, Agda, Pie or Idris: congratulations you have avoided them." It's not really clear why you'd want a book about the downsides of a quite recent development in practically usable programming models. Is it just because you are a hater?
- bbeonx 8y agoMy guess is because OP has been burned by the "LEARN THIS NEW THING, IT'S REALLY COOL AND POWERFUL AND ALL OF THE COOL KIDS ARE DOING IT (and oh by the way many of the simple things you do all the time are incredibly inconvenient...)" narrative one too many times. Adopting something purely on it's merits is a bad idea, but nobody ever writes the book about a language/paradigm's downsides. I'm pretty sure that was the joke, but I might be off.
- jackfraser 8y agoUnless said language is PHP, in which case there's no end of diatribes about it
- owl57 8y agonobody ever writes the book about a language/paradigm's downsides Indeed. One can argue that books like "optimizing X" or "secure X" are about ways to easily write slow or insecure code in X, but this is somewhat narrow. Is there never enough demand for a broader book on downsides of X?
- KirinDave 8y agoThe book is fantastic. If you think this model is interesting, please consider trying Idris and reading the Idris book: https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...
- etatoby 8y agoI learned a bit of Idris on the book you link, but I gave up after trying to implement Quicksort (the classical Haskell one-liner) in Idris vectors. You need to manually write a page of theorems for Idris to accept it. It's crazy.
- KirinDave 8y agoSo don't write quicksort in Idris. It's not going to work very well anyways. It's not at all well-suited, and isn't really even an especially important sorting algorithm in a world where linear time sorting and constant time indexed searches are a thing. But most of the work you'd be doing to write quicksort is writing the machinery for structurally recursive sorting, which a lot of tutorials write not because you have to, but because it's a very good exercise for learning how to write total functions that are recursive in a way DT systems can prove totality on. Most of these tools are in the contrib library (and the book mentions this). For example the preorder interface you need: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Decidable/Order.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/con...
- sandGorgon 8y agoI know that typescript doesn't have advanced types, but can a book like this be adapted to use typescript ?
- IlGrigiore 8y agoThis book does not talk about static typing, but about dependent types. Dependent types are more powerful and expressive than simple types because they convey more information. For example you could have [Int] to represent a list of numbers, but you could also have [x: Int, x > 20 && x < 50]. Or you could have an ordered array and know this fact by the type associated to the array. Moreover, you need to use a theorem prover to show that applying a function to a particular dependent type will result in the output dependent type. This kind of programming is not well suited to be implemented into typescript.
- k__ 8y agoSo dependent types aren't static? How does Idris solve this problem when compiling to JavaScript?
- nardi 8y agoDependent types are static. GP was trying to say that this book is about more than just normal static typing (of the kind that TypeScript adds to JavaScript). There is no problem compiling dependent (or static) types to JaveScript, as the type checks are done at compile time, and don’t require any support from the JavaScript runtime.
- Naomarik 8y agoThat sounds like clojure spec.
- IlGrigiore 8y agoClojure spec is contract programming. You write pre and post conditions to ensure at runtime that Pre -> Program -> Post and every time you call a function pre and post conditions need to be checked. Dependent types analyze that relationship at compile time by proving that given the preconditions the function will produce the desired output. Since this is a compile time check you will not have a runtime penalty.
- sillysaurus3 8y agoSad to say the book isn't on Library Genesis, so you'll have to drop $40 if you want the knowledge. http://libgen.io/search.php?req=little+typer http://libgen.io/search.php?req=little+typer Also Library Genesis is amazing: http://libgen.io/search.php?req=knuth http://libgen.io/search.php?req=knuth It's everything I dreamed of when I was a kid. I used to spend hours at the local library scouring through crummy "Learn C++ in 24 hours" type books. http://custodians.online/ http://custodians.online/ is worth a read too.
- adamnemecek 8y agoIt came out today.
- Hates_ 8y agoSeems like libgen is blocked in the UK. I get redirected to http://www.ukispcourtorders.co.uk/ http://www.ukispcourtorders.co.uk/
- jacoblambda 8y agohttp://gen.lib.rus.ec/ http://gen.lib.rus.ec/ seems to work fine
- hackermailman 8y agoThe knowledge is freely available, here's Dan Licata giving an introduction to Dependent Types for functional programmers https://youtu.be/LXvP1A97oAM https://youtu.be/LXvP1A97oAM Even though watching that, I probably think I understand Dependent Types then I'll read the Little Typer and discover my intuition was wrong like when I read the Seasoned Schemer and thought I already knew everything there was to know about the concept of higher order functions.
- bordercases 8y agoIt'll happen.
- anothergoogler 8y agoThe book didn't materialize from thin air, the authors are even named on its cover.
- cmrx64 8y agoThis book is a real joy to read. I got to peek at a draft at OPLSS 2017 and have been waiting impatiently for it to come out. The detailed, carefully worked examples one after another that this style of book is famous for is adapted beautifully to dependent type theory. Check it out! The code implementing the language in the book is here: https://github.com/the-little-typer/pie https://github.com/the-little-typer/pie
- dunham 8y agoDoes the book discuss the implementation of the language or just usage of the language?
- bjz_ 8y agoI believe it's more just how to use a dependently typed language (my copy is still in the mail). Like the Little Schemer, it's written in the Socratic style. I think the idea is that you can do it all in your head if you want, with a piece of paper covering up the column with the answers. If you are interested in the implementation, you can read more about it from one of the authors: http://davidchristiansen.dk/tutorials/nbe/ http://davidchristiansen.dk/tutorials/nbe/
- zitterbewegung 8y agoIs there a place where you can download the source code that is used in the book?
- mullr 8y agohttps://github.com/the-little-typer/pie https://github.com/the-little-typer/pie
- zitterbewegung 8y agoSource code of pie (used in the book) at https://github.com/the-little-typer/pie https://github.com/the-little-typer/pie
- pkrumins 8y agoThis space reserved for JELLY STAINS!
- deleted 8y ago[deleted]
- Mythroat 8y agoIs there a reason dependent types are not more common?
- daxfohl 8y agoThey can make libraries a pain. Like imagine if someone write a library in C#2025 with dependent types where functions took parameters like [i: i%2 == 0] or whatever. And your big project has no existing dependent types. There's no way to adopt this library unless you pull dependent types all the way in. Or even if you did, but your types were [i: i%4 == 0] or [i: (i+1)%2 == 1] or whatever, you'd have to write proofs that they types were compatible. Even some simple things are just not worth it.
- 21 8y agoMaybe some form of gradual typing like TypeScript is somehow possible? And also like TypeScript, a repository for declarations for popular libraries.
- danidiaz 8y agoIf the project had no existing dependent types at all, couldn't you just perform a runtime check before calling the library? The check would return evidence that [i: i%2 == 0] for the particular i, or fail at runtime. If it succeeded, then you could invoke the library using the new evidence. One appealing aspect of dependent types is that they let you decouple validation of inputs from the function calls themselves, while still disallowing passing wrong inputs to the function by mistake.
- bjz_ 8y agoYup, lots of people are under the impression that you need to prove everything when it comes to DTs. That's not true - you can indeed push these checks to runtime, and just have the compiler make ensure you do it.
- Zalastax 8y agoYou could just assert that i%2 == 0 via some postulate - as long as the proof is irrelevant for the code that is. Doing so is similar to converting from any in a gradual type system: if the assertion is correct you get correct code with little work and if you're uncorrect you're no worse off than if you had no types at all. There are difficulties with dependent types, but having to go all in can be avoided via a shift in culture.
- DoofusOfDeath 8y agoI can't tell if my question is off-topic or not, but.. Can anyone recommend a book (or whatever) that introduces the aspects of type theory relevant to a would-be language designer?
- wcrichton 8y agoStrongly recommend Types and Programming Languages [1]. I think it's the most useful + accessible book on type theory out there. [1] https://www.amazon.com/Types-Programming-Languages-MIT-Press/dp/0262162091 https://www.amazon.com/Types-Programming-Languages-MIT-Press...
- bjz_ 8y agoI hear that Practical Foundations of Programming Languages by Robert Harper[0] is highly recommended. I have Types and Programming Languages, but found it a little dry to be honest. I do use it as a reference manual in my work though. [0]: http://www.cs.cmu.edu/~rwh/pfpl.html http://www.cs.cmu.edu/~rwh/pfpl.html
- etatoby 8y agoI recommend these introductory lectures to Category Theory. I'm going through them right now. I assume you know some math/set theory and some Haskell, otherwise you may want to work though some of the chapters in Real World Haskell first. Oh and put the videos at 1.25× or 1.5× otherwise you will fall asleep. https://www.youtube.com/user/DrBartosz https://www.youtube.com/user/DrBartosz
- bjz_ 8y agoDon't get me wrong - CT is a super handy thing to learn, and it pops up a ton when thinking about any software, including type checkers and compilers, but the OP was specifically asking about type theory and programming language implementation. Yes, you can express lots of category theory in terms of type theory (the dream is to implement all of it in terms of TT so that we can mechanise it), but it won't be the best use of your time if you want to build a type system.
- urda 8y agoI'm glad I checked HN today because this sounds like a fantastic read. I went ahead and picked up a copy of it for myself!
- mcguire 8y agoAs an aside, it's great that Duane Bibby is still providing the art for these. Without him, nothing would be the same.
- leoc 8y agoHere's a 2006 TeX-user-group interview with Bibby: http://tug.org/interviews/bibby.html http://tug.org/interviews/bibby.html
- jedharris 8y agoSeveral comments elaborate on the big gap between normal programming practice (e.g. structurally recursive algorithms) and the great difficulty of dependent typing those practices. Some of these comment on how dependent types are "just out of the lab". This brings into focus a question I've had for a long time: Why this gap, and especially in this direction? E.g. in aerodynamics we had Bernoulli's principle for a couple of hundred years before we could build airplanes, which depend on it. In formal language theory we had lambda calculus, Turing's universality results, etc. decades before we had Lisp and Fortran. We often see the difficulty of building a practice to exploit theory. So it seems very strange to me that we are able to write / plug together literally world-spanning software systems -- which do have bugs but fact work correctly nearly all the time. But we can't easily well-type even simple algorithms with extremely well understood properties. Why this huge gap, in this direction?
- KirinDave 8y agoI'd argue that there aren't many "simple" programs with "well-understood" properties in use in industry. Software is a bit different from architecture in that partial failures tend to work and can be refined around repeatedly (a partially failed building tends to rip itself apart, partial failures in software can linger for years and only cease when their dependencies fault out). People are just more amenable to altering their processes, products and lives around bad software. I think dependent typing reveals to us, to some extent, what a house of cards we truly have built for ourselves.
- jedharris 8y agoSeveral interesting points but maybe they show something different from what you intend. Network stacks, databases etc. that correctly handle trillions of interactions, some of them adversarial, have indeed been "refined around [their failures] repeatedly" and have gotten pretty robust along the way. On the other hand useful formal accounts of their behavior (distributed, highly parallel, loosely coupled, asynchronous) seem far, far way. It would be helpful to have an account of approximation to formal properties, especially if that can help us understand how repair and refactoring can lead to progressively better approximations. Perhaps the house of cards that is revealed is formal methods not software.
- jedharris 8y agoSee related HN thread <https://news.ycombinator.com/item?id=18050706> https://news.ycombinator.com/item?id=18050706>