CoRecursive: Coding Stories - Tech Talk: The Little Typer With Daniel Friedman and David Thrane Christiansen

Episode Date: December 1, 2018

Tech Talks are in-depth technical discussions. When it comes to type systems "I am, so far, only in the dependent types camp" - Daniel P. Friedman You can write more correct software and even rigorous mathematical proofs.  Prepare for some mind stretching. Previous guests like Edwin Brady and Stephanie Weirich have discussed some of the exciting things a dependent type system can do Miles Sabin said dependent types are surely the future. This interview is to get us ready for the future. Daniel P. Friedman is famous for his "Little" series of books. Little Schemer, Little prover, Little MLer and so on. These books are held in high regard. Here is a quote from Doug Crockford:  "Little Schemer teaches one thing, a thing that is very difficult to teach, a thing that every profession programmer should know, and it does it really well. These are lessons that stick with you." The latest one is the little typer and its about types. Specifically dependent types. Dan's coauthor is David Thrane Christiansen, Idris contributor, and host of a podcast about type theory that is way over my head. Together they are going to teach us how the programming skills we already have can be used to develop rigourus mathematical proofs. Stay tuned to the end for my guide to working thru the book. Originally published at CoRecursive here Join Our Slack Community

Welcome to Code Recursive, where we bring you discussions with thought leaders in the world of software development. I am Adam, your host. Hey Dan, why aren't you allowed to use Recursion? Because you're not allowed to use Recursion. Yeah, but why not? Because you're not allowed to. So if you want your programs to correspond to proofs, then direct uses

of actual recursion where something refers to itself corresponds to circular reasoning. You can write more correct software and even rigorous mathematical proofs previous guests like edwin brady and stephanie wyrick have discussed some of the exciting things a dependent type system can do miles sabin said dependent types are surely the future this interview is going to get us ready for that future. Dan Friedman is famous for his little series of books, including The Little Schemer, The Little Prover, Little MLer, and so on. These books are held in high regard. Here's a quote about The

Little Schemer from Amazon Book book review little schemer teaches one thing a thing that is very difficult to teach a thing that every professional programmer should know and it does it really well so his latest book is called the little typer and it's all about types specifically dependent types dan's co-author is david christiansen an idris contributor and host of a podcast about type theory that is frankly way over my head together they're going to teach us how the programming skills we already have can be used to develop rigorous mathematical proofs. Also, stay tuned to the end of the episode and I'll give a little brief overview of how I worked through the book. Tips and tricks. If you haven't subscribed to this podcast yet, I recommend you do so, so that new episodes will be delivered automatically

to you. Also, I've set up a Slack channel for the podcast. If you want to chat about this episode or any episodes or just chat with fellow listeners, you can join the Slack channel. You will find the link on the website. So Dan and David, welcome to the podcast. Thanks for having us on. Appreciate it. I have this book that you guys wrote, The Little Typer, all about dependent types. So I thought I would start off by asking you guys, what are dependent types? So dependent types are types that are able to contain ordinary programs. So in a language like Haskell or

something, you might have a type list of A, where A could be any old type. But in a dependently typed language, you could also have things other than types there. So you might say the list of N A's, where N is the number of things in the list. And then your type system all of a sudden needs to know about numbers and what it means to do arithmetic on numbers. So for example, appending two of these lists, then you'll be able to see in the type that the length of the output is the sum of the lengths of the inputs and that sort of thing. Why is that useful? So that one is less useful than you might think, given how often it comes up as an example,

just because it's such a good example. But dependent types are useful because they allow you to write very precise types that say a lot more about your program than you'd otherwise be able to say. Yeah, that one is, I think, the more important point. And, you know, languages like Agda or Idris have more types, but it's just more types that give you this capability, plus, you know, industrial strength underneath it. We're trying very hard to make this book be something that's relatively easy to understand,

to get the feel for what it means to be writing programs with dependent types. And dependent types are also about more than just writing down a very precise type. Doing that is nice because you can get more help from your programming language implementation in writing your program, and you can make really nice interactive environments on top of that. But the other way that you can use a type system is as a logic for doing mathematics. And a dependent type system is a very rich, expressive logic that lets you talk about all sorts of different things. So you can also go and do something that feels very much like writing a program, but you've actually proved a theorem,

which I think is really fun. Yeah, that is the coolest part. There's no question, in my mind anyway, that you just have a program of a certain type. And if that type is thought of as a theorem, then that program is thought of as the proof. And I just love that metaphor. Just love it. and dan um like a lot of your your previous books are about scheme which i guess isn't really uh it's it's not a language known for its type system i guess so that's certainly true although racket does have a type system it uses something called occurrence types. And in fact, we used a lot of the types that are in Racket in order to implement our system. So are you pro types in general or just dependent types? I'm so far only in the dependent types camp. I just like the idea that you can just write a type and prove it correct.

I think that's fabulous. Because the language of types is much broader than the language that are used in more conventional languages. I'm still not a big fan. Partially because the programs that I wanted to write with types, it was impossible. In fact, there's published papers on the fact that you can't write what I call reflection. There are published papers that say you can't use Henley-Miller types to prove properties that you want to prove. And that's one of the reasons why I like dependent types, because there doesn't seem to be

a big circle you can draw around it that says you can't do this and stuff like that. So you think that non-dependent types are limiting, but dependent types are empowering. Is that kind of the idea? It's how I feel. I don't know. I can't speak for David. He indeed is not speaking for me there. I, I, I like programming lots of different ways and I have fun in languages which either don't have types or just have one big type, depending on which philosophical camp you're in or those like, you know, I write a lot of Haskell at work and I think that's a lot of fun.

And I do pen types as well. I like lots of ways to program. I like types. Also dependent types. I find I'm not quite sure how they work yet, but I'm working through your book. So hopefully by the end, it's all going to make sense.

So in, in the book um you you introduce this uh language pie that you created for the book so yes specifically so what's the intent behind that so the reason why we thought we needed to make our own language for this book, rather than using sort of an off-the-shelf, well-developed language like Coq or Agda or Idris or one of those, was that those languages put a lot of effort into automating away all of the parts that can be tedious or difficult or require understanding. And in the interest of getting work done, you're not forced to confront the inner workings of the system until later on. And we thought that it's going to be easier to give a very minimal

language that people... And when I say easier, I mean actually more difficult. Easier for you to learn things by having to work hard at it. And additionally, it let us have an implementation. We'd initially hoped to have the entire implementation of the language be the last chapter of the book. Unfortunately, we didn't manage to get it quite small enough, so we have quite a lot of description of how you would implement it. And then there's an online tutorial I wrote as well. Oh, is there really?

Yeah. About how the language was created? Well, there's a tutorial if you want to make your own. Oh. And if you want to understand the source code. The source code of the language is freely available. Anyone can download it and modify it and hack on it as they want. There's at least one variant dialect already in the wild.

And I hope that there'll be a lot more in the future. The interesting thing is, is cause I did look at the GitHub repo. Like it's not very big. Thank you. So by all means, we both worked on it. I know Dan is a,

has very exacting standards for simplicity and smallness of code that are very useful when working on a project. So the actual implementation up there is also about half of that code is sort of interactive user interface kind of stuff, right? It includes some parts that are not really exposed and documented yet, but that I hope to make more public in the future for doing things like having editable PI code inside of a slide if you're doing a talk somewhere. So you can sort of edit code in front of people and watch the type checker respond. And it has a plugin for Dr. Racket so that you can put the mouse over expressions and see what their types are and those sorts of things. And the actual core of the system is, you know, as small as we could possibly make it. While some of those things are a little hairier, just because dealing with graphical user interfaces requires just more code. And this language is, like, so the implementation is written in Racket. And to use it, I downloaded Dr. Racket.

And I put like LangPy at the beginning. And that was about it. That's right. The Racket developers have a background in education. So they're very motivated to make things simple to set up and easy to work on multiple machines and that sort of thing. One thing I found interesting about the language is just the words it uses

for things. Instead of having a type annotation, you have a claim. Was there reasons behind the verbiage used in the language? Well, yeah.

I mean, reasons behind the the verbiage used in the language well yeah i mean so yeah we've so we've i think we've implemented this thing about what do you what do you say dan 10 to 12 times and thrown them away yeah four or five seven don't know, some ridiculously large number. But we originally had one expression that captured both the type and the program. And it was getting clumsy. And we finally sat down and chatted about that and and we changed it to be with two different things. I don't think of a claim kind of as a type annotation, but more like we're trying to get a good expression that represents what the theorem we want to prove, so to speak. So claim is, for those listening to this who haven't read the book or worked with Pi. In Pi, if you want to do a top level definition, the first thing you do is you use the language, the keyword claim, and then you put claim and then the name and then the type. And then later you define and then the name and then some expression which should have that type. And so initially, we had one way of introducing a definition where you put down the type and the program together.

And it just got to be too big in the book. And it turned out to be better for the writing if we could separate the two from each other. You know, these little boxes can be quite a challenge that are in the little books. Yeah, I bet. So this is actually the first time that I've read. I bought both the little typer and the little learning about things in a very iterative fashion. So where does that structure come from? Well, I used to be a professor of public policy before I got my doctorate. And I was teaching the students at the Linda Mays Johnson School of Public Affairs. And one day the students said, can we do something together on this?

And I said, sure. And I grabbed a room and we worked for a solid week and we wrote The Little Whisper. By walking from one end of the room to the other where there was a blackboard and people were chiming in with different things. For example, I really can't remember when we decided to put in the food, but it certainly was by somebody in that room.

It may have been me. I couldn't possibly remember it was 1973 when we wrote it and 74 when it came out but um and it was all done on an ibm selectric and there's a lot of other stories to go with that but i'll save that for something a little more interesting but yeah it was was quite a task back then. I didn't even type it. Someone else typed it in the IBM Selectric. I like the, like, it gave me a good sense for, like, to be honest, I found some parts.

I'm working through the book. So I have a book, I have a book mark here on page 151 but i've scanned through a little bit further i've jumped ahead a little bit even though the book said not to i agree completely it's it's hard enough so so i found the book to be a challenge at times but i found that this this back and forthness um it kind of keeps the pace going so so um i felt like even though I was struggling, at least I was struggling in very small chunks. It does.

I actually sometimes suggest that if you don't feel like you've got 100% of it, you should really go back and read that chapter over again. I have gone back. It is definitely, there are very few words in the book. And there's no harm in rereading it. And maybe even taking some notes as you're going along. So earlier I said something like that the claim was a type. And Dan said, no, it's a proof.

And that maybe gets at the heart of the matter, doesn't it? No, it's a theorem. Oh, it's a theorem. Well that maybe gets at the heart of the matter, doesn't it? No, it's a theorem. Oh, it's a theorem. Well, it's not a theorem until you prove it. Right. But it's a statement. Yeah. I get pedantic about these things.

It's an occupational hazard. It's fine. That's fine. So we do have a way of doing type annotations in Py, which is that expression called the. And the reason we called it the was

because we figured if Idris and CommonLisp both call their type description operator the, then we're in good company. Okay, nice. And maybe, yeah, so I guess that's how we do our type annotations. Maybe that's why you were objecting to it being called type annotation before, Dan?

I don't know. Yes, absolutely. I figured if we're going to talk about it, we should talk about what we have. So the correspondence between types and theorems, I guess, is... Curry-Howard isomorphism you're talking about now. I am, but I was hoping to get one of you to maybe expand on it because I, I know nothing and I have some experts here.

I suspect you know some things. Well, but basically in the metaphor, it's two names and one concept. So theorem and type is basically one name and program and proof are one concept. And of course, it's the proof of the program, proof of the type or the, sorry, proof of the theorem or program of the type. So you have both of them.

And as I said, that's called the Curry-Howard isomorphism, where you can get a lot of mileage out of this. The interesting thing that I'm learning from this book, I guess, is that some of my skills that i've developed for for writing software i guess can translate via this isomorphism to to to do math i guess yeah real math it's the first time i'd ever seen real math um that didn't come with an awful lot of um bells and whistles. This is very direct, very simple, and our assumption is that you've had some experience with using a language like Scheme or Racket or Lisp or any of the sort of the parenthesized guys, and you're very comfortable with recursion. And I'm sure you read that far where you discovered the comfort with recursion is necessary,

but I won't go into any more details than that. So as far as Curry-Howard goes, I think there's something important, Dan, that a lot of people gloss over and that I didn't hear you say. So, Curry-Howard correspondence is really... So, Curry and Howard both observed this, that not only do statements written in intuitionistic logic map directly to types and proofs written in intuitionistic logic mapped directly to programs in the simply typed lambda calculus, but also that normalizing expressions in simply typed lambda calculus corresponds to cut elimination. One of the most important results we have in logic is that any proof written using the cut rule, which is the rule that allows you to make local assumptions, can be simplified to a proof that doesn't use the cut rule, but that

still proves the same thing. And it turns out that that process of normalizing proofs is the same process of normalizing programs. So not only do we have that every proof corresponds to a program, but also that writing our proofs out and pushing them down into the most direct form corresponds to running our programs until they're done. And that's a very important aspect of it. Yeah, I think that you covered it a lot better than I did, truthfully. But it's still the two boxes I put up in my class. Yeah, it's the two boxes, but it's more than just the two boxes. It's also that they behave the same way,

which I think is what's really cool about that. And we have similar correspondences. So you had Phil Wadler on your show recently, and he talked quite a lot about this for a lot of other logics as well. And so I think anyone who's really interested in this should go listen to that interview. So we have a more interesting version of intuitionistic logic where you can talk about individuals. That gives you dependent types because you're able to have statements that

aren't just A and B, but also predicates about sub-objects. You could say that two numbers are equal. That's a good example. You have to be able to talk about the individual numbers. Or you can say things like, for all numbers n and m, adding n to m is equal to adding m to n. And these sorts of things, saying like for all and exists and having individual things you're talking about, that's really what you get from adding dependent types to the mix. But if you want to get other logics, you can also figure out how to run those as programs. And that's really, really cool, I think. So you mentioned normalization. And something that was interesting to me in the book was this concept of normalization. I wonder if you could describe what it is with an example and how it relates to evaluation.

Sure. have types in a language like pi, the types don't just sort of classify expressions saying, you know, this one is a number, or this one is a list of numbers, or this one is a function where you give it a number and it gives you back a list of numbers. They also tell you which of the things they describe are the same as which other things they describe. So you know that 5 plus 8 is the same natural number as 13, and you know that appending the list containing 1, 2, 3 to the list containing 4, 5, 6 is the same as the list containing 1, 2, 3, 4, 5, 6. You can look at these groups of things that are the same as each other as being buckets. And you take all of your lists of numbers and you put them into the buckets, divide them up such that each one is grouped with the ones that it is the same as. And then for each of these

buckets, we have a simplest, most direct representative that we can pick out of that bucket and a way to find that representative given anything in there. And that's what we call the normal form. So we pick one representative from each collection of things that are the same as each other. And because we have a way of finding that representative for anything in the bucket, we can tell whether two things are in the same bucket by finding their normal forms. And it turns out that a good way to pick those normal forms is to do all your computation until it's all done. Although some of the types in Py, they have some additional rules that are more than just running the program.

For example, lambda x f is the same function as just f on its own. In order to find the normal forms of functions, we have to wrap them in a maximal number of lambdas until they get figured out. And the unit type, which we call trivial in pi, because it corresponds to sort of a trivial theorem or a trivial statement that's really easy to prove, since it's only got one constructor, then we just go ahead and say, well, everything in it's the same as everything else, whether or not it's that constructor, because eventually it would be. To find the normal form of something with the unit type, you just take the unit constructor

and those sorts of things. But most types, you just run the program until it's done, and then you have the normal form. But running the program until it's done also includes going in underneath lambdas and running those, which makes it extra fun. I thought you were going to

skip the Ada long, but I thought you were going to skip the Eta long, but I guess you didn't. So Dan says Eta long. That's that process of putting all of the maximum number of lambdas around the functions for those not in the know.

And actually, the reason why we put in all of these Eta rules was that at Indiana University, they were kind enough to let us test out a draft of our book on a class of students. We didn't even have to go through an IRB for that. But there have been two additional ones. Sure, sure. But during that semester, we discovered certain things. One of them is that it's much friendlier to students to give them a test suite that their program should pass. And one way to make it much easier

to run these tests is if you have a lot of those rules that tell you... In particular, the rule for the function, which says you have to put all the lambdas on the outside to find the normal form, the rule for a unit, which says they're all the same, and the rule for the empty type which says they're all the same too because you're never going to get one anyway. Doing that allowed us to actually write much simpler test suites that we could give them to have their programs pass because the computer does more work making things be the same as each other, and the human human does less work which is always a good thing i want to get back to the sameness but so at some point in my before we do that while i was working through this book i got stuck at some point and then so i went into github and i searched for like files with the pi type as the extension and i found somebody i guess who probably took this

course you're talking about and their exercises and actually actually, it helped me out a lot to see this. So thank you to, I wrote this down here, Jacob Adley, whose exercises helped me understand the like. Jacob who? Adley. I don't know this person. Yeah, I don't know this person. Yeah, I don't know. But thank you. Jacob, if you did take our class and we've forgotten you,

I'm very sorry. So on the normalization points, to make sure I understand, in a simple example, you could have plus 2, 2 and 4. And you're saying 4 is the normal form, but 4 is also an evaluation of this statement. So somehow equality has been linked to evaluation

in a way I'm not familiar with, I guess. So I think that there's when you're, when you're making a logic and you want to be able to talk about programs, you have sort of two ways you can do it. One of them is you can write up all the ways that programs compute and then say to the person writing the proof, you get to now demonstrate how the, how these programs give you the right answer by sitting down and saying, well, now I'm going to use this rule, then I'm going to do a beta reduction here, I'm going to rewrite by the definition of plus right here,

I'm going to unfold the definition of times to see that it's actually a loop that does a bunch of pluses over here, and then I'm going to reduce here. Or you can rig up your logic so that everything automatically respects computation and then have the computer do all of that work. And one of the wonderful things about type theory that we can thank Pema Tliliv for is coming up with this judgmental structure or coming up with this way of putting the logic together where the computation is something that can just happen in the background without this judgmental structure or coming up with this way of putting the logic together where the computation is something that can

just happen in the background without a human having to go apply all the steps one at a time. And that's why the notion of sameness in the type theory is probably the most important thing. When people are first learning, I know when I

first learned it at least, I had this idea like, well, let's see. I thought the important thing was what types do we have and what programs have those types. But in fact, it's much more important to think about which programs are the same as which other programs and why that is the case. And the other part just kind of falls out from that. And that's because it allows you to know when computation is going to happen, and it allows you to know when the computer is going to do the work, and when the computer is not going to do the work, so you have to do the work yourself, and that sort of thing. Yeah, I don't think I've fully wrapped my head around it.

It's interesting. Also, the sameness, like I described this example with 2 plus 2, but actually the sameness applies to whole functions. Yeah, everything. So one way to think about it is that when you're, let's say you're writing a type checker, the type checker has got to sort of answer two questions, at least. And one of those questions is, how do I find the type for this expression? But it also has to be able to answer the question, when are two types the same type? Because I may expect one type and I get that the expression has some other type. How do I compare those two types?

And for something like simply typing them to calculus, the way you compare them is just recur over them and check that the structure is identical. But when your types get to contain programs, then checking for sameness of types means checking for sameness of programs as well. Ah, I see now. Yeah, so that has to be. Say I write a function, and as its argument, I need to be it's like say i say i write a program i write a function and it and it needs to as its argument i need to pass it you know four pieces of cake let's say i've got a type that represents pieces of cake right so i pass it like chocolate and i pass it rainbow and i pass it double chocolate and i pass it quadruple chocolate i like your consistency of food, keeping all the examples on food. And then, but then I actually, what I end up past, so I think that's what I want to do.

But my cakes are coming from two different places. So, you know, I've got one source of two pieces of cake, which is my chocolate and my rainbow. And I've got another source of two pieces of cake, which is my double chocolate and my quadruple chocolate. And so I'm going to call a function that will append these, which gives me something that has two plus two pieces of cake in it. But my function needs four pieces of cake. And when we look at that, we think, well, of course, those are the same type because two plus two is the same as four. But the type checker needs to be built in a way that it can understand that, which means that the logic or the type systemer needs to be built in a way that it can understand that, which means that the logic or the type system itself needs to be built in such a way that 2 plus 2 and 4 are the same

thing. And there's some systems out there where I'd have to sit down and sort of manually prove that 2 plus 2 and 4 are the same before I could pass that result of putting those lists together into my function. But in this system, we don't have to, because 2 plus 2 and 4 are just the same as each other without any work needing to be done by the user. In Py, you have something called evidence. Is this related? So evidence is the reason why a thing is true. So we wrote the book from the perspective of someone doing intuitionistic logic.

And if we're doing that style of logic, then it's not the case that everything is true or false. There are some things that we don't yet know whether are true or false. There are open problems about which we just... They're not true, and they're not false until somebody proves that they're true or false by providing evidence that they are true or evidence that they are false. And hopefully not both evidence that they are true and evidence that they are false, because then somebody's made a real big mistake. Yes, I'd say. So I guess... See, this is my fault for skipping ahead, because I might have misunderstood the evidence. Especially in chapter 8, you've got to read that one really carefully. So when we define what it means to be even in type theory, we do that by saying what counts as evidence of evenness.

Okay. And so one way to say what counts as evidence of evenness is to say, well, a number is even if we can cut it directly in half without anything left over. In other words... No crumbs. Yeah. So let's say we want to provide evidence that four is even. Well, that evidence is the number two, because doubling two gets us four. And if we want evidence that 108 is even, that evidence is the number 54, along with some evidence that doubling 54 gets us 108,

which is what we wanted. And we don't have evidence that 1 is even because there isn't any number that doubling it gives you 1. So the way you define a new concept or a new predicate, you know, a predicate is like a statement with a hole in it that you fill out with an object to get a complete statement. The way we define that is we do it precisely by stating what counts as evidence for that statement. So, if I were... Maybe I should just finish reading the book. You can call us back. I'm really enjoying the book. It's's stretching my mind I'm finding it a challenge that's my summary of it

music to my ears so like if I were to if I were to want to write out a something a proof that like the square root of 2 is irrational is that something that can be done in pi?

It would take a fair bit of effort. So I don't want to say yes because I haven't done it. Nor have I. I think that in principle, you could probably do it. But when you start getting to more complicated things, then I think it would be better to use a system that does more of the work for you. So I would use... This is where I would stop using Py,

and I would go write it in Coq or Agda or Idris or one of these systems. We are trying in our book to help people get the more philosophical ideas or the underlying ideas behind dependent types

rather than to give you a practical tool. Although in theory I think you can do this, probably. And if you can't, then we could change the language a little bit and make it so you could. Yeah. I'm hoping that people will pick up the implementation and say, oh, I'd like to have streams in the language or something or other types that we don't have. And all of a sudden they will see, oh, now I've got it. I got the types because I understand how the rest of the system works in terms of the internals. And then they would be

able to enlarge their definition of pi. And hopefully they would share that with others. But yes, that is the kind of thing that could be done in languages like Py. And the intent here, I mean, isn't that right? So if I understand the intent is to present a very small language so that people can understand this core. Absolutely. And the core of Py looks very much like the core of something like Cocker Agdar Idris. The difference really, there's one really important difference, which is that Py comes with a fixed collection of data types sort of installed in the factory. And if

you want more, you have to open it up and add your own. Whereas those other languages allow you to extend the collection of data types. And we didn't add that feature, or we did add it actually at one point, and I ripped it out again, because we wanted the implementation to be small and understandable. But other than that, it's basically the same kind of system. I wanted to find out what the definition of one of these like end and add is. I don't know how you pronounce these things. That's good enough. And I was looking for like a prelude, but there's no... It's built into the language. Kind of like in Haskell, like if you want to go find if,

if isn't really defined anywhere. Yeah. Well, but that's not 100% accurate. In Appendix B, you can read the inference rules which describe the implementation. So that gives you a little bit more material to stare at, to give you a sense of what is going on. But it's not the case that inNet is the kind of thing that you could sit down and define your own version of. You can define a function that works just like inNet, except it'll be a little bit noisier because it'll need more arguments.

That's true. And one reason, one thing we really tried to work hard to do with Py was make it so that programs in it were short, even though the implementation was very simple. And lots of these little core type theories like Py end up being very verbose to write programs in, but being verbose to write programs in isn't going to work when you have to fit them in half of a piece of smaller-than-usual paper. Is that a good thing or a bad thing? Are the constraints... I think that the constraints

were useful here. What it led to was a language which had some built-in things where the implementation uses a technique called bidirectional type checking, which I think people interested in how these implementations work can go read my tutorial that I've made. And it uses that to avoid having the user have to write quite as much stuff down, while at the same time not needing any unification, which is one of the spots where implementations of dependent types can get complicated.

So I think now we understand kind of the context of the language. I'm not going to write a web server in this. This is a tool to teach us about this type system and how it works. And to teach you about the way to and how it works. And to teach you about the way to think about these sorts of type systems, which will hopefully make it easier to learn the industrial strength ones when you're done.

Yeah, I think that characterizes our goal completely. We want students to really work through it and understand it, and then they can move on to the industrial ones. After my interview with Philip Wadler,

I was wondering about dependent types. It seems like, have we reintroduced undecidability? If types and values are the same thing so when you say undecidability do you mean undecidability of type checking um my question may not be coherent which is perfectly possible that's okay let's let's work it out phil was telling me this story about there was paradoxes and one way to remove these paradoxes was to

remove self-reflexivity reflexivity we are consistent so that doesn't come up we do not have a proof that our language is completely without paradox we've done all the standard things that one does to avoid it, and I'm pretty sure.

I'd bet a decent amount of money that at least the idea is if modulo, maybe there's a bug left. There could definitely be bugs, but modulo that. Right. So the origin of

type theory goes back to this paradox of having a set that contains all sets that do not contain themselves. Also known as the Barber paradox. Yes. By Bertram Russell. Yeah, Russell's paradox. And so the way that Russell's type theory gets around this is by saying that every set doesn't get to refer to things willy-nilly. It gets to refer to things that are smaller than it.

So a set of type 0 only gets to refer to ordinary things and not to other sets. A set of type 1 gets to refer to sets of type 0 and ordinary things, or refer to, I mean, contain. A set of type 2 gets to contain sets of type 1, sets of type 0, and so forth. And then this paradox goes away because it doesn't even make sense to ask the question of whether the set contains itself. So then I guess my question is, can't types refer to themselves in this world? No, actually, and that's a very good question. In the very first version of dependent type theory that Per Mateloev cooked up, you actually did have a type which classified all the types or described all of the types, including itself. And Gérard came along and showed that based on an earlier system he'd made which had a feature like that,

that he showed to be inconsistent. He showed that Matin-Loeuf's early system was also inconsistent for exactly that very reason. So what we do in pi is we have a type that describes most other types, but not itself, and also not types that contain itself. So we have this type U, which is the universe, and nat, the type of natural numbers, is part of the universe. Atom, the type of atoms, is in the universe. List of nat is in the universe, but u itself is not. And neither is list of u or functions that take u as an argument or return u and these sorts of things. Oh, and we just have this one universe type because that's all we need in order to teach the lessons in the little typer. The industrial strength

systems that I was talking about earlier, they all have infinitely many universe types where each of them talks about the ones that are smaller than itself. So you have universe 0, which talks about things like NAT, universe 1, which talks about things like universe 0 and NAT, and so on and so forth. And we had that in early version of Pi, and then we ran a little test with all of the homework assignments from our students and with all the code in the book, and we found out that nobody ever actually used anything more than one universe,

so we just ripped the rest out. And there's also sort of a folklore theorem that you never need more than five levels of universes. Yeah. Yeah, I think... Oh. Someone was saying that they'd gone and checked every proof ever done in New Perl, which is another implementation of type theory, which is very unique and very different than many of the other ones. They'd only ever used five or seven universes or something like that. So maybe infinitely many is too many. I'm

not sure. It has a nice simplicity to it. So one thing that I found challenging, I guess, in this PyLanguage is just recursion is a bit more involved than I'm used to. Is that... You're not allowed to use recursion. I think. Is that right?

Hey Dan, why aren't you allowed to use recursion? Because you're not allowed to use recursion. I think. Is that right? Hey, Dan, why aren't you allowed to use recursion? Because you're not allowed to use recursion. Yeah, but why not? Because you're not allowed to. So if you want your programs to correspond to proofs, then direct uses of actual recursion where something refers to itself corresponds to circular reasoning. And that's not good enough. That's the biggest shock for me, incidentally, that there has to

be a way around recursion absolutely all the time. There's no ifs, ands, or buts about it. So it ends up looking like recursion, but you're just working down a natural number? Yeah. One of the things about the industrial strength ones is that they allow recursion, where we have taken away recursion so that you really have to get into the nitty gritty details. And I think that in order for this discussion to make perfect sense, there's something we should probably clarify. our programming language pedant hat on, then the term recursion has a very specific meaning, which is that it means that something that you're defining or something that you're writing is able to refer to itself directly. And so in order to do that in something like Coq or Agda or Idris, then there's a check that happens in the implementation

of the language. And it makes sure that every time you're calling a function recursively, every time it's invoking itself, it's doing so on a smaller input. And then it makes sure that all the inputs are finite in size. And thus, if you're going down a finite number of steps, you'll eventually hit the bottom, and then it's okay. Because at the bottom, you'll have something that isn't self-justifying or that isn't a reference to itself. Yeah, back in 74, that was the driving force that I used for teaching recursion. I actually thought that recursion was really Yeah. Now I can't use it. So in those languages, you do have recursion, but it has to be recursion that lives up to certain checks to make sure that it's okay to do, that it's always going to be safe. self-referential argument, like the one I had with Dan just a moment ago, is only a problem

when the program falls into an infinite loop that sits there doing nothing except heating up your room. So a circular argument corresponds to an infinite loop that does nothing. And if you rule out those infinite loops that do nothing, you're also ruling out the

circular arguments. And in pi, in order to make the implementation simpler and also which I think is even more important, in order to make the definition of the language correspond more closely to some of the literature that you have on dependent types and also to some of the implementations. So the style of recursion that we have in Py is the style used in Lean, which I've been really remiss in not mentioning because Lean is also a great system, another dependent type language from Microsoft Research. And this way of formulating things is nice, where you have a few built-in ways of doing recursion, at least one for each finite data type. It's wonderful because you're able to have very simple rules that describe when the recursion, you're always going to have, because it's impossible to tell whether an arbitrary program falls into an infinite loop spinning there doing nothing,

you instead get conservative approximations. And those conservative approximations, in order to allow you to write more useful programs, get more and more complicated over time. You're like, oh, we can allow this. Oh, we can allow this. Oh, we can allow this. And you have to be very careful to get it exactly right and still be useful. Whereas the version with the eliminators like we use in Pi, and they use in Lean, and like Epigram used behind the scenes, that's nice because the rules saying when is something that has a recursive behavior acceptable are very, very simple. You haven't mentioned yet about totality of functions that I think is relevant in this point. Do you want to say a little bit more about that, David? Sure. Yeah, so a function is, you know, we've got the domain, we've got the range, and it's a function if every element of the domain

is paired up with exactly one element of the range. And it's a total function if all of them are, every single thing. The function doesn't get to say nope, it doesn't get to sit there spinning its wheels, but every input you give it, it'll always give you back an output. And because we're dealing with programs, we want to get back that output in finite time.

And finite time isn't a very strong guarantee. I mean, you can easily, in a language like Pi, you can write a program that will take until you're old and gray to give back an answer, if not until your great-great-great-grandchildren are old and gray. I mean, after all, we do have Ackerman in the book. Yeah. Yeah. You can write very, very slow programs that take a very long time, even in a total language.

But the important thing is that this correspondence between programs and proofs is a truth with modification. We don't have a correspondence between any old program and any old proof. What we have is a correspondence between total functional programs and intuitionistic proofs. And that don't make use of non-constructive reasoning proofs. So we can have, you know, we're not able to make use of, like, the principle of the excluded middle, which lets us, or we're not allowed to make use of, you know, double negation elimination, where you go from not not a to just a, things like that, because those correspond to things that aren't sort of directly representable in a type lambda calculus. And this is a really long, deep thing, and you can get a lot of those principles by adding things like continuations to your language, which is really fun. But for purposes of what we're doing here, we need to have the total functions on the one side, because a function may not be total in a couple of ways.

One is that it might, for certain inputs, just say, nah, I'm not going to be defined here. And in that case, then our proof doesn't work because functions are the way we prove a for all statement. So we might say for all even numbers, adding one to that number gets you an odd number. That'll be a function where you give it a number, you give it evidence the number is even,

and it gives you back evidence that one greater than that number was odd. And if it just didn't work for 24 for some reason, then we'd have a problem. So it's got to cover all of the possible inputs. But also, if the case for 24 just sort of sat there spinning its loop by saying well hey if I'm going to check whether 25 is odd I'm going to do that by checking whether 24 is even again first then that would also be an unsatisfactory proof

I'd say it wouldn't be a proof it simply wouldn't be so in order for all of our programs to correspond to proofs in Py, we make sure that you can only write total functions. And these elimination forms, like the intnat that you were talking about earlier, those allow you to make sure both that you're covering all the possible gnats and that any recursion you do is controlled in such a way that recursive

calls are all happening on one smaller number. If we allowed recursion. Yes. Well, I mean, the behavior acts recursive, right? To me, it feels like recursion because, like, I don't know. I don't want to, like, you know, I'm

programming in Scalab day-to-day, and I don't tend to write, like, direct recursion where I'm calling myself. I tend to in Scallop day-to-day and I don't tend to write direct recursion where I'm calling myself. I tend to use a fold or something. And the arguments are similar, right? You end up giving it a natural number and you need to give it a function that returns the next type, I think.

I'm trying to remember. So for in that, or let's take in the list because we're talking about folds. And most people are more used to thinking about folds in terms of lists rather than in terms of numbers. Although the underlying idea is essentially the same idea. So when you're doing a fold on a list. Is that a fold R or fold L?

Let's go for R here. Okay, that's what I thought. And I'll try to keep them straight because I always mess them up. But my usual way of thinking, like, do I want to use fold L or fold R here. And I'll try to keep them straight because I always mess them up. My usual way of thinking, like, do I want to use foldL or foldR here is I'll always sort of like, well, I'll try one. If it doesn't work, I'll do the other one. Or I'll do some sort of little test to make sure which one it is because my brain just isn't wired to remember those. But yeah, so when we're doing using this reclist operator, which we have, which is the non-dependently typed fold,

then we give it a value to return when the list is the empty list. We give it something that takes the head of a list and the tail of a list, and the result of doing the fold over the rest of the list and gives us back a new output. And then by doing those at each step, we get down to the right, we finally, you know, it'll, it'll do the step, do the step, do the step until it hits the base case for the empty list. The dependently typed version of that takes one additional argument, which is what we call the motive, or we don't call it, you call it. That's what it's called. Well, you're talking about

induction now, right? Yes. And so dependently typed fold is induction. The motive explains what the type is in terms of the list that you're recurring over.

Which means that the type at each step could be a little bit different. So for instance, if we wanted to write a proof that appending the empty list to any old list gives you back that same list, then the motive is going to be, you know, lambda x's append empty list Xs is equal to Xs. And then when we do that for the base case, we then apply the motive to the empty list to figure

out what the type of the base case is, which is going to be the empty list append empty list is equal to empty list. And then for the step, we're going to apply it to one unknown list to find out the type of the result of the rest of the recursion, and then apply it to sticking the extra element onto that to get the type for the result that we need, and we get that back. And so then by combining these at each step, you get the relationship between the resulting type and the list that you're looking at right now is maintained appropriately. And so the real difference between this recursion operator and the typical fold R is that it takes a couple more arguments, or it takes another argument, which is sort of the tail of the list. You're not usually having that one included as you go but putting it here

makes life easier and you can get the other one out of this one as well so i really liked the book thanks um i'm gonna i'm gonna keep working on it like i have found it i'm uh i'm gonna make it through it i'm gonna try to try. I hope so. You might mention how many pages it is so that people understand what you mean when you say I'm going to make it through it. I'm exaggerating here, but I did get the little schemer and the little typer,

and I think the little typer is twice as long. But I think there's a lot of appendix. Yeah, there's a fair amount. We wanted to include the source code to Py in the back of the book so that people could have an easier time understanding and playing with the implementation. But just like you don't put the scheme compiler in the back of the scheme book, then it was too big. So we tried to do the next best thing, which was give a mathematical description of the language and then some text explaining how to read the math, because that

ends up being a lot shorter than the code. And probably for the people who want to know just exactly what's in the language, that appendix B is pretty useful. If you have the right background. And otherwise, we did our best explaining it so that you could figure it out. But we try to give you the background as well in that section. Yeah. So hopefully we came pretty close. Yeah, and there's something interesting on the back of the book here where it says that you were trying to do something not practical or rigorous, but beautiful.

Yeah. What did you guys mean by that? Yes. Well, there are these other systems, Idris, et cetera, the ones we keep mentioning, and they are practical. That is also a truth of modifications. They are practical for the right kinds of people in the right kinds of situations. And hopefully someday they will be practical for more people in more situations. Yes.

I'm just saying this because I lurk on the Id mailing list a lot. And if a bunch of people show up and start saying, the great Dan Friedman said this was practical, but I'm having a difficult time writing a brand new web browser and writing an operating system in it, then... Well, there's that, of course. We are moving toward practicality in more domains, but they are still research software. Right. That's for sure. But we didn't try that.

We tried to make it so that you would understand pretty much what the excitement is about with respect to dependent types. I'd like to tell a little story, if I may. When I had just finished a book called Little Prover with Carl Eastland, I had sent it to my friend Adam Folzer. And I got an email from him as soon as he got it. And he said, so what's your next book going to be about? Next little book. And I said, well, I've seen an awful lot of excitement about dependent types and um he said don't move what do you mean don't move so i'm thinking to myself if i want a glass

of water i can't get it or something so um uh he sent me a letter and to David at the same time, introducing us. And that afternoon we decided to write the book. So that was a nice little story. And I, I wouldn't, I would be uncomfortable if we did not mention Adam's, Adam's involvement.

He, he deserves, he deserves a lot, the credit that accrues, though, not the blame, depending on how you feel about that. None of the blame. Yeah, so I knew Adam because I was an intern at the time at Galois, which is where I'm working right now. And he worked there at the time, and so we met each other that way. Dan, are you a convert now? Like you mentioned at the beginning, types maybe not your favorite always?

Well, I usually think in terms of the structure of the problem. And sometimes the structure of the problem is long as the people who are reading the books that I'm writing can understand what we're trying to say with whatever tricks we come up with. Sometimes the types are a perfectly good choice, but sometimes they aren't. It's just that simple. We only have so many pages. We only have so many. The size of programs can only be a certain size. And as long as the language is communicating as clearly as possible what's going on,

then I don't think it's necessary. That's how I feel. When it is necessary, like in the little MLR with Matthias Fallheisen sure, that's a good time to do it and even in a little Java few patterns we ended up using types but by and large it's the ideas behind the problem

that matter to me the most and if my co-author on one of the little books doesn't see any need for the types and I don't see any need for the types, and I don't see any need for the types, then I think we can get the same concepts across. And then if you're going to be writing a program in a type language,

it should be relatively easy because we are very conscious of the types as we're thinking about how we're explaining the ideas. Not all types need be checked by machine. That's a good way to rephrase it. I like that, David. I stole that from Matthias. Oh, okay.

All right, guys. Well, thank you so much for your time. The book's great. I recommend people check it out. And thank you very much for having us on here and also for putting in so much effort to read through the book. Well, just keep trying.

You'll be fine. Just remember what I said about chapter eight. Read it very carefully. And if I may insert a one little plug. Oh, yeah. I had a talk at Strange Loop recently where we had a demo of Pi and the language used in the book and sort of our explanatory style. So if you want to get a little preview of how things work,

then you can go find that. It's on YouTube. And, you know, if you're, because I know 40 bucks is a lot of money for a lot of people. And if you aren't, you know, sure whether or not you want to invest that in the book, you know, there's libraries,

but also you can go on YouTube and check that out. And maybe it'll make you sort of be able to make a more informed decision. All right, that was the interview. I'd like to thank the many people who promoted the last episode with Wade Waldron on Twitter, especially the Code Maverick, who has mentioned the show in a half a dozen tweets, most of which are in Spanish, but I'm going to assume that he's saying nice things. I was also recently at the Scale by the Bay conference in San Francisco and the John DeGos functional programming training. Let me just say that both were amazing. There were so many interesting talks at Scale by the Bay. It was a bit of an overload, which when it comes to

conferences, I think is really a good thing. Then I followed the conference by doing the John DeGos training, which was great. I interviewed him back in episode nine and taking a four day training session with him was a great experience. It was a bit exhausting and actually I still haven't completed all of the provided exercises, but I learned a lot. And I would recommend the training to anyone who wants to learn about functional programming, especially using Scala. All right. Using the Py language. So the little typer uses this custom built language, as was discussed, called Py.

So here is my overview for working through the book. First of all, you want to download Dr. Racket, then install the Pi language. And then at the top of your file, you just have to put like pound lang Pi. Easy enough. Now, as you're working through the book, my first tip is to read deeply and methodically. So the book is in kind of a two-column dialogue format. And what you want to do as you read it is try to guess the answer that's in the right column as you go through. And if you can't guess the answer, that's fine.

But make sure that you understand the answer. And I mean, if you can't understand the answer, what I often did was just, you know, progress a little bit more through the book and either it will get more clear or less clear very quickly. And if it's less clear, then you should backtrack. And as you heard from the authors, rereading chapters is recommended. The book is, it has a very conversational tone, but I would say it's dense. So the other thing is running the code. So as you work through the book, there are snippets of code that are in a solid, they're outlined in a solid box. So you want to type all those into Dr. Racket. You can use lowercase words in place of the Greek letters like lambda and pi. And then what I found helpful was just playing with the code,

so trying to run things through the REPL to get a feel about what we were defining and trying to write my own variations on it and making sure that it compiled and that I could run it. I also found it useful to write up the types in a language I was more familiar with in the comments above the claim. There is also a function called checkSame that is useful for testing

if the results of a function call have a certain value. So I found that quite useful for getting my intuition. I would type out a function from the book. I would then try running it in the REPL with some arguments and then kind of solidify that knowledge. I would put in a check same, this internet call equals this result. All right, so those are my tips.

Thank you for listening to the podcast this far. If you enjoyed it, spread the word, tell your friends.