Is The Little Typer the static typing book I've been waiting for?

Dan Friedman's The Little Typer is coming out in September. I'm very excited about this book. It's about dependent types, and it claims to "demonstrate the most beautiful aspects". I can't wait!

Transcript

Eric Normand: Is "The Little Typer" the functional programming with types book I've been waiting for? Hi, my name is Eric Normand and these are my thoughts on functional programming.

There's a new little book coming out by Dan Friedman. The little books are books like "Little Schemer," "The Season Schemer," "The Reason Schemer," one more, "The Little Prover."

These are all little books. It's a style of book that Dan Friedman writes. He always uses different co-authors. They're just teaching functional programming stuff and is very cool style. I have a book. I'm not going to bring it out. I have two of them, but it's like question and answer.

You can cover up the answer. You ask yourself the question and then try to answer it. Then you see the answer. You get another question and then you try to answer it. One little bit at a time, you're developing the pathways, the thought pathways in your brain and your mind about how to reason about this code.

Scheme is a really small concise language

In The Little Schemer, it's just scheme, very basic operations on lists and things like that. The other one I have is The Little Prover which is all about proofs. It's very cool. This new book is coming out. It looks like it's coming out in September, so almost here, and it's all about dependent types.

One of the things I've been waiting for in typed languages is basically a structure and interpretation of computer programs. About static typing. SICP, that's an abbreviation for "Structure and Interpretation of Computer Programs," is a classic book teaching how Lisp works, how to implement a Lisp using an interpreter, a compiler.

It's basically computer science through the eyes of Lisp. What's cool is it uses Scheme which one of the authors co-developed. Scheme is a really small concise language. It's perfect for this kind of thing. There's not a lot of fluff to get in the way. It's easy to implement Scheme. Because it's so simple, it was used as a language for exploring language features.

In SICP, in the book, he started exploring, what if we add call by name instead of call by value, things like that, just messing with how things got evaluated and you get to explore how things work. Everything was so small and concise. You really got this sense of understanding the fundamentals without a lot of fluff around it.

Haskell is bigger compared to Scheme

I feel like the typed world doesn't have anything like that. Haskell is a big language compared to Scheme, has a lot of extensions. It has a lot of libraries. It has a lot of concepts in it. The syntax is big compared to Scheme. If you compare any language to Scheme, it's got a lot of syntax.

I've never seen a book that's saying, what is the minimum type system we can have to start seeing benefits? What is the essence of it? It's great to have lots of features, want to understand that essence, but what is the essence? What is that thing that makes it important?

I know from Dan Friedman's other work, from The Little Schemer, from The Little Prover, the two that I've read, that it really is trying to get at the essence. It's trying to find that core of what it means to be Scheme, which is basically doing a lot of consing and traversing cons cells, and recursively.

The book is going to have some core

What does it mean to do proofs? Theorem proving about your code. There's a very small language in that comes with it that you can start to reason about code with. I'm optimistic that this book is actually going to have some core.

This is what dependent types are, and this is why they're cool before you have to go and learn Idris, which I think is a very powerful language. It's also a maximal language in the way that Haskell is.

What can we do with types once we have them? I want to see what's the minimum what is that, and I'm just really looking forward to this book. It's got a nice pedigree. I've been looking at the author, the co-author, David Thrane Christensen, very interesting. It's got an afterword by Conor McBride, who is a type theorist.

I'm just really looking forward to it. I'm going to get it as soon as it comes out. I hope I don't go into a cocoon while I'm reading it. It's that kind of book because I still have other work to do. This could be it. This could be the book that makes types and what you can do with them makes sense to a lot of people.

First class functions

In SICP, in the first chapter, you start with a function, a mathematical function like some curve. You derive the function that takes the derivative of any function using the limit theorem of calculus, something like that. The definition of calculus of the derivative that's using the limit, you take the limit to epsilon, to zero and anyway you choose a small epsilon and you develop a function.

That's like first class functions in the first chapter, but in a very clear way. If you are into this stuff, you already know the calculus enough to follow along. I want to see something like that. He's going to approach it at a very piecemeal as he usually does, just one small step at a time building up this dependent type system and what you can do with it. That's going to be great.

Am I weird for not liking types that much?

I actually have met Dan Friedman at a couple of conferences. I spent a good two hours with him at one strange loop. I asked him about what he thought about types because I was thinking about types all the time myself. I had recently left my Haskell job. I was enjoying Clojure and just wondering, "Am I weird for not liking types that much?"

I asked him and he said, "You know, the type system like Haskell..." but I asked a bunch of people and he was one of them, he said, "With a type system like Haskell all of the claims that people make about the kinds of mistakes that you avoid."

He said that he doesn't make those mistakes. Meaning choosing the wrong type, like type errors. He doesn't make the kind of mistake where I thought it was a list but it really was a string. I thought it was a number, but it turned out to be a symbol. He doesn't make those mistakes

Dependent types

I found, for me, that was true and especially with the kinds of code that you can see him write in his work. He uses a very small subset of Scheme. It's hardly a small language and he uses a small subset. He's not doing higher order stuff you get in Haskell, where you need a type system because you're doing something very abstract, like using type classes and stuff like that.

Anyway, he says he doesn't make that kind of mistake, but he said, tomorrow there's a talk on dependent types. I had never heard of dependent types of that time. There's a talk about dependent types and he says their claims are mistakes that I make.

They can eliminate off by one errors. They can eliminate, you have a no terminated list, nil terminate list. You can tell whether you've got another element in the types. He said that that was the kind of mistake that he does find himself making, and so he was very interested in dependent types.

A few years later, here it is what The Little Typer. I'm very excited to see what he's come up with and how to teach this, how to find the core of it. If you're excited, let me know.

If you think that this doesn't make any sense, also let me know. Are you going to buy the book, The Little Typer? Have you read any other little books? Get in touch with me. I'm @ericnormand on Twitter and you can also email me. I'll see you later.