The Little Typer

[KirinDave]

The 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-i...

[etatoby]

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

[cmrx64]

This 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

[dunham]

Does the book discuss the implementation of the language or just usage of the language?

[plafl]

I'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]

Don't miss The Little Prover! :)

[jsntrmn]

I 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?

[jedharris]

Several 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]

I'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.

[DoofusOfDeath]

I 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]

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

[bjz_]

I 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

[etatoby]

I 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

[zitterbewegung]

Source code of pie (used in the book) at https://github.com/the-little-typer/pie

[Mythroat]

Is there a reason dependent types are not more common?

[bjz_]

They've been historically hard to implement in a way that is both efficient, sound, integrates with effectful code, promotes code reuse (like in Haskell), and has good developer UX (good error messages and IDE support). I believe we are getting to a point where it is feasible, hence I'm messing around with it myself [0], but it can be challenging to navigate the terrain of papers and theory as a language designer. While DTs themselves are quite simple, the integration with other features users expect is tricky, and producing a production-grade compiler is definitly not as straightforward as making a regular Hindley-Milner style language.

[0]: https://github.com/pikelet-lang/pikelet/

[daxfohl]

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

[elcritch]

Wondered that myself. It’s surprising there’s not more languages with dependent types (and the associated requisite libraries).

I suspect it’s taken a while for the theory behind dependent types to become widespread enough for some enterprising hacker or grad student to make a useable language for them (e.g. Idris). Even if a new theory comes along it takes time for appropriate metaphors and methods of using them to be created and disseminated.

Though does computing the dependent types at compile time take more process.

[mcguire]

Imagine having to prove a Coq theorem for every function call.

No, it's not really that bad. But almost. I really suggest you play with Idris some; what you can do with it is brilliant, for simple tasks. For complicated tasks, like the fully general propositions you need for library functions, it can get much more complicated than the code itself.

[etatoby]

Try to write the classic Haskell Quicksort in Idris:

    qsort :: Ord a => [a] -> [a]
    qsort [] = []
    qsort (p:xs) = qsort (filter (< p) xs) ++ [p] ++ qsort (filter (>= p) xs)

and let me know how it goes, if you will. That's when I gave up on Idris.

[tree_of_item]

They're very difficult to use and they make code more complicated.

[mcguire]

As an aside, it's great that Duane Bibby is still providing the art for these. Without him, nothing would be the same.

[leoc]

Here's a 2006 TeX-user-group interview with Bibby: http://tug.org/interviews/bibby.html

[nigwil_]

Will there be a Kindle edition eventually?

[kqr2]

There doesn't appear to be kindle versions of older books including The Little Schemer, The Seasoned Schemer, etc. so most likely not.

[lylecubed]

> 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?

[urda]

I'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!

[georgewsinger]

What language does this book use? A dependently typed LISP? Or something Haskelly?

[cmrx64]

it’s a pretty standard type theory lambda calculus, written as sexps because it’s inside racket, but it’s its own thing.

[zitterbewegung]

Is there a place where you can download the source code that is used in the book?

[mullr]

https://github.com/the-little-typer/pie

[jedharris]

See related HN thread <https://news.ycombinator.com/item?id=18050706>

[pkrumins]

    This space reserved for JELLY STAINS!

[sandGorgon]

I know that typescript doesn't have advanced types, but can a book like this be adapted to use typescript ?

[sillysaurus3]

Sad 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

Also Library Genesis is amazing: 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/ is worth a read too.

[xevb3k]

I feel like there’s so much to say about this comment, that I don’t even know where to start.

So firstly I agree, $40 seems like a lot. I personally couldn’t justify it at the moment. Particularly when the reproduction cost is nearly zero.

But $40 also doesn’t seem like a lot to pay for a book that will probably not sell more than a few thousand copies. Most likely revenue generated won’t fully cover the time and effort required to create such a book.

But... the author is also a professor at MIT. I feel like if this work wasn’t somewhat publicly funded, it really should have been.

In the end, I’m left morally confused. But it feels like something is wrong in the world when a book like this is available only to a select few, when for the same capital outlay it could be available to everybody.

[mjfl]

It took a lot of work for the author to draft this. Would it kill you to compensate them for it?

[hackermailman]

The knowledge is freely available, here's Dan Licata giving an introduction to Dependent Types for functional programmers 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.

[mi_lk]

Sad because it's not available for free? What is this attitude?

At least local libraries actually buy the book to support the authors.

[Hates_]

Seems like libgen is blocked in the UK. I get redirected to http://www.ukispcourtorders.co.uk/

[anothergoogler]

The book didn't materialize from thin air, the authors are even named on its cover.

[adamnemecek]

It came out today.

[deanmen]

According to WorldCat Library search it's not even in libraries other than Library of Congress and "College of Western Idaho". So it is probably not popular enough to be uploaded to a pirate site either. In fact it just came out on 18 September, so in order for a copy to be uploaded anywhere someone would have had to buy it and then immediately scan it, or the authors would have to put a draft copy on their website.

[snpriyanshu]

I would recommend you to shop from used book stores like thriftbooks.com. I got the knuth's books for like $30(3 volumes) and many more.

[sriram_malhar]

As an author of a book on which I worked incredibly hard, FUCK you. If you want it so bad, buy it. Or wait a few years, buy it used. Or borrow it from a library. Don't fucking steal it.

Carpenters and other craftspeople who earn far less than the denizens of Hacker News buy whatever they need to further their business. They don't steal others' tools.

[bordercases]

It'll happen.