Introduction
Adam: Welcome to Code Recursive, where we bring you discussions with thought leaders in the world of software development. I am Adam, your host.
David: Hey Dan, why aren’t you allowed to use recursion?
Dan: Because you’re not allowed to use recursion.
David: Yeah, but why not?
Dan: Because you’re not allowed to.
David: 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.
Adam: You can write more correct software and even rigorous mathematical proofs. Previous guests like Edward Brady and Stephanie Weirich have discussed some of the exciting things a dependent type system can do. Miles Saben said, “[inaudible 00:01:00] surely the future.” This interview is going to get us ready for that future.
Dan Freeman 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 review, Little Schemer teaches one thing, a thing that is very difficult to teach a thing that every professional programmers 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 00:01:43] and Idris contributor and host of a podcast about [Type Siri 00:01:49]. 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.
What Are Dependent Types?
David: Thanks for having us on.
Dan: Appreciate it.
Adam: 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 so, what are dependent types?
David: So dependent types are types that are able to contain ordinary programs. So we might in a language like [Haskell 00:03:09] or something, you might have a type list of A where A could be any old type, but in a dependently type language, you could also have things other than types there. So you might say like the list of nAs, 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, a pending 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.
Adam: Why is that useful?
David: 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.
Dan: Yeah, that one is I think the more important point. And languages like [inaudible 00:04:10], or Idriss have more types, but it’s just more types that gives you this capability, plus industrial strengths 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.
David: And dependent types are also about more than just writing down a very precise type. Doing that as nice, because you can get more help from your programming language implementation and writing your program. And you can make really nice interactive environments on top of that. 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.
Dan: Yeah. That is the coolest part. There’s no question in my mind anyway that you can… You just have a program of a certain type and that 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.
Dependent Types or No Types at All
Adam: And Dan a lot of your previous books are about scheme, which I guess it’s not a language known for its type system, I guess so.
Dan: That’s certainly true. Although Racket does have a type system. This is something called occurrence types. And in fact, we used a lot of the types that are in Racket in order to implement our system.
Adam: So are you pro types in general or just dependent types?
Dan: I am 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. And I think that’s… I’m still not a big fan. I’m partially because of 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 [inaudible 00:07:03] 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.
Adam: So you think that non-dependent types are limiting, but dependent types are empowering, is that the idea?
Dan: That’s how I feel. I can’t speak for David.
David: He indeed is not speaking for me there. I like programming lots of different ways and I have fun in languages, which either don’t have time to just have one big type depending on which philosophical camp you’re in or those like I read a lot of Haskell at work and I think that’s a lot of fun and I do dependent types as well. I like lots of ways to program.
Adam: I like types also. Dependent types I find I’m not quite sure how they work yet, but I’m working through your books. So hopefully by the end, it’s all going to make sense.
David: I hope so.
Adam: So in the book you introduce this language pie that you created for the book.
Dan: Yes. Specifically,
Adam: What’s the intent behind that?
David: 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 CORC, or [inaudible 00:08:32], Idriss, or one of those was that those languages put a lot of effort into automating a way, all of the sort of parts that can be tedious or difficult or require understanding, and in the interest of getting work done, you’re not sort of 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 [inaudible 00:09:03] 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 had 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.
Adam: Oh, is it really?
David: Yeah.
Adam: About how the language was created?
David: How old is it the tutorial, if you want to make your own 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 if 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.
Adam: The interesting thing is, because I did look at the GitHub repo, it’s not very big.
David: Thank you.
Dan: Well, thank David by all means.
David: We both worked on it.
Dan: I know.
David: Dan 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? So it includes some parts that are not really exposed undocumented yet, but that I hope to make more public in the future for doing things like having editable Pie 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 plugin for [DrRacket 00:10:38] 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 as small as we could possibly make it. Well, some of those things are a little hairier, just because dealing with graphical user interfaces requires just a more code.
Adam: And this language is, so the implementation is written in racket and to use it, I downloaded DrRacket and I put like Lang Pie at the beginning, and that was about it.
Dan: Mm-hmm (affirmative). That’s right.
David: 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 sorts of thing.
Adam: One thing I found interesting about the languages is just the words it uses for things like instead of having a type annotation, you have a claim, was there reasons behind the verbiage used in the language?
Dan: Yeah. I mean-
David: So, yeah. I think we’ve implemented this thing about… What do you say Dan? 10 to 12 times and thrown them away? Yeah.
Dan: … four or five, seven, I don’t know some ridiculous 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 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 [inaudible 00:12:39] we want to prove so to speak.
David: So claim is… For those listening to this who haven’t read the book or worked with Pie. In Pie, if you want to do a top level definition, the first thing you do is you use 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.
Dan: These little boxes can be quite a challenge that are in the little books.
On ‘The Little’ Book Format
Adam: Yeah, I bet. So, this is actually the first time that I’ve read… I bought both the Little Typer and the Little Schemer and I was working through them. So this is my first introduction to that format. And I thought it was super fun. So where does this like… So for people who aren’t familiar it has kind of a dialogue format where you’re talking back and forth and learning about things in a very iterative fashion. So where does that structure come from?
Dan: Well, I used to be a professor of public policy before I got my doctorate, and I was teaching the students at the Lyndon Baines Johnson School of Public Affairs. And one day the students [inaudible 00:14:14], “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 the room. It may have been me. I couldn’t possibly remember it. It was 1973 when we wrote it and 74 when it came out. And it was all done on an IBM Selectric. And there’s a lot of other stories that go with that, but I’ll save that for something a little more interesting, but yeah, it was quite a task back then. I didn’t even type it someone else typed it in the IBM Selectric.
Adam: I like the, like it gave me a good sense for… To be honest, I found some parts… I’m working through the book. So 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.
David: Don’t do that.
Dan: [crosstalk 00:15:32]. [inaudible 00:15:34], you don’t want to do that.
Adam: So I found the book to be a challenge at times, but I found that this back and forthnes it keeps the pace going. So, I felt like even though I was struggling that at least I was struggling in very small chunks.
Dan: It does. I actually sometimes suggest that if you don’t feel you’ve got 100% of it, you should really go back and read that chapter over again.
Adam: I have gone back.
Dan: 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.
Adam: 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?
Dan: No, it’s a theorem.
Adam: Oh, it’s a theorem.
David: It’s not a theorem until you prove it.
Dan: Right. But it’s [inaudible 00:16:31].
David: It’s a statement. I get [inaudible 00:16:35] about these things. It’s a occupational [crosstalk 00:16:37].
Dan: It’s fine.
David: So we do have a way of doing type annotations in Pie, which is that expression called the and the reason we called it the was because we figured if Idris and Common Lisp both call their type [inaudible 00:16:56] operator, the, then we’re in good company.
Adam: Okay, nice.
David: 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?
Dan: Yes, absolutely. I figured if we’re going to talk about it we should talk about what we have.
Curry-Howard
Adam: So, the correspondence between types and theorems, I guess, is a…
Dan: Curry–Howard isomorphism, you’re talking about now?
Adam: I am, but I was hoping to get one of you to maybe expand on it because I know nothing, and I have some experts here.
David: I suspect you know some things.
Dan: 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, the 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.
Adam: The interesting thing that I’m learning from this book, I guess, is that some of my skills that I’ve developed for writing software, I guess, can translate via this isomorphism to do math, I guess.
Dan: Yeah. Real math. It’s the first time I’d ever seen real math that didn’t come with an awful lot of 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 parenthesized guys, and you’re very comfortable with recursion. And I’m sure you’ve read that far where you discovered the comfort with recursion it’s necessary, but I won’t go into any more details than that.
David: 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 sort of Curry and Howard both observed this, that not only do statements written in intuitionistic logic map directly to types and proofs written intuitionistic logic map directly to programs in the [inaudible 00:19:47] calculus, but also that normalizing expressions in [inaudible 00:19:52] calculus corresponds to cut elimination, which is to say that… So 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 sort of make local assumptions, can be simplified to approve 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.
Dan: Yeah. I think that you’ve covered it a lot better than I did truthfully, but it’s still the two boxes I put up in my class.
David: Yeah, it’s the two boxes, but it’s more than just the two boxes. It’s also that they [crosstalk 00:20:52] the same way, which I think is what’s really cool about that. And we have similar correspondences, like so you had Phil Wilder 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 that sort of 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 sort of A and B, but also predicates about some object.
Like you could say the two numbers are equal or that if… Yeah, 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 the 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.
Normalization
Adam: You mentioned normalization and something that was interesting to me in the book was, well, this concept of normalization, I wonder if you could describe what it is and with an example and how it relates to evaluation?
David: So when you have types in a language like Pie, the types don’t just sort of classify expressions saying 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 five plus eight is the same natural number as 13. And you know that upending the list containing one, two, three to the list containing four, five, six is the same as the list containing one, two, three, four, five, six. You can look at these sort of groups of things that are the same as each other, as sort of 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 sort of 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 it’s sort of, 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 forums is to do all your computation until it’s all done.
Although some of the types in Pie, they have some additional rules that are more than just running the program. So for example lambda F of X is the same function as just F on its own. So in order to find the normal forms of functions, we have to sort of wrap them in a maximum number of lambdas until they get figured out. And the unit type, which we call a trivial in Pie, because it corresponds to sort of a trivial theory 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, and it’s the same as everything else, whether or not it’s that constructor, because eventually it would be.
And so 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 till it’s done, also includes like going in and underneath lambdas and running those, which makes it extra fun.
Dan: I thought you were going to skip the eight along, but I guess you didn’t.
David: So Dan says eight along, 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 [inaudible 00:25:23] was that at Indiana University, they were kind enough to let us test out a draft of our book on a class of students. But we didn’t even have to go through an IRB for that. I think-
Dan: But there [inaudible 00:25:37] to do additional.
David: … sure. But during that semester, we discovered certain things like 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, like 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 does less work, which is always a good thing.
Adam: I want to get back to the sameness. 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 files with the Pie type as the extension. And then I found somebody, I guess, who probably took this course, you’re talking about and their exercises. And actually it helped me out a lot to to see this so thank you to who wrote this down here, Jacob Adley whose exercises helped me understand the like-
Dan: Jacob who?
Adam: … Adley.
Dan: I don’t know this person. But thank you.
David: Jacob, if you did take our class and we’ve forgotten you, I’m very sorry.
Adam: So on the normalization points to make sure I understand, in a simple example, where you could have plus two, two and four, and you’re saying four is the normal form, but the four is also an evaluation of this statement. So there’s some sort of… Somehow a quality has been linked to evaluation in a way I’m not familiar with, I guess, because…
David: So I think that 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 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 think [inaudible 00:28:38] to live for is coming up with this judgemental 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… 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.
Adam: 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 two plus two, but actually the sameness applies to whole functions.
Dan: Yeah, everything, mm-hmm (affirmative).
David: 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, right? 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 [inaudible 00:30:21] 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.
Adam: Ah, I see now. Yeah. So you have to, that has to be.
David: Say I write a function and it needs to… As its argument, I need to pass it four pieces of cake. Let’s say I’ve got a type that represents pieces of cake. So I pass it like chocolate and I pass it rainbow and I pass it double chocolate and I pass it quadruple chocolate.
Adam: I like your consistency of food, keeping all the examples on food.
David: But then I actually what I ended up passing… So I think that’s what I want to do, but my cakes are coming from two different places. So 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 quadruple chocolate.
And so I’m going to call a function that will append to 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 the type checker 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 two plus two and four are the same thing. And there’s some systems out there where I’d have to sit down and sort of manually prove that two plus two and four 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 two plus two and four are just the same as each other, without any work needing to be done by the user.
Adam: And in Pie you have something called evidence, is this related?
David: So evidence is-
Dan: Evidence is a program.
David: … yeah. Evidence is the reason why a thing is true. 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’re false because then somebody’s made a real big mistake.
Dan: Yes, I’d say.
Adam: So I guess see, this is my fault for skipping ahead because I might’ve misunderstood the evidence.
Dan: Especially in chapter eight, you got to read that one really carefully.
David: So, when we define what it means to be even in type theory, we do that by saying what counts as evidence of evenness.
Adam: Okay.
David: 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 leftover. In other words-
Dan: No crumbs.
David: … yeah. 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 it gets us 108, which is what we wanted. And we don’t have evidence that one is even because there isn’t any number that doubling it gives you one. So the way you define a new concept or a new predicate… Predicate is 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.
On Writing Proofs
Adam: If I were… Maybe I should just finish reading the book.
Dan: You can call us back.
Adam: I’m really enjoying the book, it’s stretching my mind. I’m finding it a challenge. That’s my summary of it.
Dan: It’s definitely a challenge.
David: Music to my ears.
Adam: So, if I were to want to write out something, a proof that the square root of two is rational, is that something that can be done in Pie?
David: It would take a fair bit of effort, but I… So I don’t want to say yes cause I haven’t done it. I think-
Dan: Nor have I.
David: … 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 Pie and I would go write it in CORC or [inaudible 00:35:42] or Idris or one of these systems. We are trying in our book to help people get more sort of the 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.
Dan: Yeah. I’m hoping that people will pick up the implementation and say, “Oh, I’d like to have streams in language or something.” Or other other types that we don’t have. And all of a sudden they will say, “Oh, now I’ve got it. I got to 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 Pie and hopefully they would share that with others.
David: But yes, that is the kind of thing that could be done in languages like Pie.
Adam: And the intent here… I mean, isn’t that right? So if I understand the intent is to present a very small language so the people can understand this core?
David: Yeah.
Dan: Mm-hmm (affirmative). Absolutely.
David: And the core of Pie looks very much like the core of something like CORC, [inaudible 00:37:01] or Idris. The sort of one really important difference, which is that Pie 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.
Adam: I wanted to find out what the definition of one of these like [inaudible 00:37:37], I don’t know how you pronounce these things.
Dan: That’s good enough.
Adam: And I was looking for like a prelude, but there’s no-
David: It’s built into the language. Kind of like in Haskell, if you want to go find if, if isn’t really defined anywhere.
Adam: … yeah.
Dan: 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, give you a sense of what is going on.
David: But it’s not the case the [inaudible 00:38:16] 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 [inaudible 00:38:23], except it’ll be a little bit noisier because it will need more arguments.
Dan: That’s true.
David: And one thing we really tried to work hard to do with Pie 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 Pie 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.
Adam: Is that a good thing or a bad thing, are the constraints-
David: 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 bi-directional type checking, which I think people interested in and 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.
Adam: … so I think now we understand 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.
David: And to teach you about the way to think about these sorts of types systems, which will hopefully make it easier to learn the industrial strength ones when you’re done.
Dan: Yeah. Anything 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.
Adam: After my interview with the Phillip Wilder, I was wondering about with dependent types it seems like have we reintroduced undecidability, if types and values are the same thing?
David: So when you say undecidability, do you mean undecidability of type checking?
Adam: My question may not be coherent, which is perfectly possible.
David: That’s okay. Let’s work it out.
Adam: Phil was telling me this story about there was paradoxes and one way to remove these paradoxes was to remove self reflexitivity.
Dan: We are consistent. So that doesn’t come [crosstalk 00:40:58].
David: Well, Dan, I should say we do not have a proof that our language is completely without paradox-
Dan: That is true. Although-
David: … all the standard things that one does to avoid it, and I’m pretty sure. I bet a decent amount of money that at least the idea is if modular, maybe there’s a bug left.
Dan: … oh, that could be, it definitely be bugs, but a modular that.
David: 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. And-
Dan: Also know as the [inaudible 00:41:35] of paradox.
David: Yes.
Dan: By [Bertrand Russell 00:41:38].
David: 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 sort of things that are smaller than it. So in a set of sort of type zero only gets to refer to ordinary things and not to other sets. A set of type one gets to refer to sets of type zero and ordinary things or refer to [inaudible 00:42:07]. A set of type two, gets to contain sets of type one, sets of type zero 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.
Adam: So then, I guess my question is, if we’re saying like can’t types refer to themselves in this world or?
David: No, actually, and that’s a very good question. So in the very first version of dependent type theory that [inaudible 00:42:36] cooked up, you actually did have a type which classified all the types or described all of the types including itself. And [inaudible 00:42:47] came along and showed that based on an earlier system he made, which had a feature like that, that he showed to be inconsistent.
He showed that [Martin Lives 00:42:58] earlier system was also inconsistent for exactly that very reason. So what we do in Pie 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. Adam, the type of Adams 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 zero, which talks about things like Nat, universe one, which talks about things like universe zero and Nat, and so on and so forth. And we had that an early version of Pie. And then we ran a little test with all of the homework assignments from our students and with all of the code in the book, and we found out that nobody ever actually used anything more than one universe. So we just rip the rest out.
Dan: There’s also a sort of a folklore theorem that you never need more than five levels of universes.
David: Yeah. Oh, someone was saying that they’d gone and checked sort of every proof [inaudible 00:44:30], which is another implementation of type theory, which is sort of very unique and very different than many of the other ones. They [inaudible 00:44:36] ever use like 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.
On Recursion
Adam: One thing that I found challenging, I guess, in this Pie language is just recursion is a bit more involved than I’m used to, is that…
Dan: You’re not allowed to use recursion. [inaudible 00:45:04].
David: Hey Dan, why aren’t you allowed to use recursion?
Dan: Because you’re not allowed to use recursion.
David: Yeah. But why not?
Dan: Because you’re not allowed to.
David: 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.
Dan: And that’s not good enough. Well, that’s the biggest shock for me, incidentally, that there has to be a way around recursion. Absolutely all the time there’s no, if ands or buts about it.
Adam: So it ends up looking like recursion, but you just have to, you’re just working down a natural number.
Dan: Yeah. One of the things about the industrial strength ones is that they allow recursion, but only special kinds of recursion usually using a pattern language. But we opted out of that because we really wanted people to think hard about things that took away… We have taken away recursion so that you really have to get into the nitty gritty details.
David: And I think that in order for this discussion to make perfect sense, there’s something that we should probably clarify. So when we’ve got our programming language [Piedmont 00:46:22] 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 CORC or [inaudible 00:46:43] or Idriss, 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 were 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.
Dan: Back in ‘74, that was the driving force I used for teaching recursion. I actually thought recursion was really cool. Now I can’t use it.
David: 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 because the problem of self reference, like a 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 Pie in order to make this, what can I say? 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 Pie is the style used in [Lean 00:48:31], which I’ve been really remiss in not mentioning because Lean is also a great system, another dependently 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 is acceptable. So in languages that allow recursion, you’re always going to have… Because it’s impossible to tell whether an arbitrary program falls into an infinite loop spinning they’re 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 like, “Oh, we can allow this, we can allow this, 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 Pie and like they use Lean and like epigram used behind the scenes, that’s nice because it’s… The rule saying like, when is something that has a recursive behavior acceptable are very, very simple.
Dan: You haven’t mentioned yet about fatality functions that I think is relevant in this point. Do you want to say a little bit more about that, David?
David: Sure. Yeah. So function it’s, we’ve got the domain and 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 Pie, 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.
Dan: I mean, after all, we do have [Ackerman 00:50:42] in the book.
David: Yeah. You can write very, very slow programs that take a very long time, even in a [inaudible 00:50:49] 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 then other logics also have these correspondences, but the sort of the traditional Curry Howard correspondence is… Intuitionistic proofs are those that don’t make use of non-constructive reasoning proofs.
So we can have… We’re not able to make use of the principle of the excluded middle, which lets us… We’re not allowed to make use of 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 [inaudible 00:51:50] 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 if… Well, 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 for all statement, right? So we might say like for all even numbers, adding one to that number it 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 like didn’t work for 24, for some reason, then we’d have a problem. So it’s got to cover all 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.
Dan: Simply wouldn’t be.
David: It wouldn’t be evidence. Yeah. So in order for all of our programs to correspond to proofs in Pie, we make sure that you can only write total functions. And these elimination forms like the [inaudible 00:53:14] that you were talking about earlier, those allow you to make sure both that you’re covering all the possible Nats and that any recursion you do is controlled in such a way that recursive calls are all happening on one smaller number.
Dan: If we allowed recursions.
David: Yes. Well, I mean the behavior acts recursive, right?
Dan: Yeah.
Adam: To me it feels like recursion because like, I don’t know… I’m programming in Scala day-to-day and I don’t tend to write like direct recursion where I’m calling myself, I tend to use like 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.
David: 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.
Adam: Mm-hmm (affirmative).
David: Although the underlying idea is essentially the same idea. So, when you’re doing a fold on a list-
Dan: Is that a folder R, or a fold L?
David: … let’s go for R here.
Dan: Okay. That’s what I thought.
David: And I will 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 is I’ll always sort of like 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, when we’re doing using this reckless operator, which we have, which is the non independently 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… Finally 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, that’s what it’s called.
Dan: Well, this [crosstalk 00:55:27] you’re talking about induction now, right?
David: Yes.
Dan: Okay.
David: And so dependently typed fold is induction. The motive explains what the type is for in terms of the list that you’re reoccurring over, which means that the type at each step could be a little bit different. So for instance if we wanted to check… If we wanted to write a proof that upending the empty list to any old list gives you back that same list, then the motive is going to be lambda-xs, upend, 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, depend empty list is equal to empty list. And then for the step we’re going to apply it to one sort of 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.
Adam: So I really liked the book.
David: Thanks.
Adam: I’m going to keep working on it. I have found… I’m going to make it through it. I’m going to try.
David: I hope so.
Dan: 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.
Adam: I’m exaggerating here. But I did get the Little Schemer and Little Typer, and I think the Little Typer is twice as long, but I think there’s a lot of appendix.
David: Yeah.
Dan: Yeah, there’s a fair amount.
David: Yeah, we wanted to include the source code, the Pie 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, 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.
Dan: And probably be for the people who want to know just exactly what’s in the language that appendix B is pretty useful.
David: If you have the right background and otherwise we did our best explaining it so that you could figure it out.
Dan: But we try to give you the background as well in that section. So hopefully we came pretty close.
Adam: 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. What did you guys mean by that?
Dan: Well, there are these other systems Idriss, et cetera, the ones we keep mentioning and they are practical.
David: That is also a truth with 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.
Dan: Yes.
David: I’m just saying this because I [inaudible 00:59:00] on the Idriss [inaudible 00:59:01] 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.”
Dan: Well, there is that, of course.
David: We are moving toward practicality in more domains, but they are still research software.
Dan: 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 the dependent types. I like to tell a little story if I may, when I had just finished a book called Little Prover with Carl Eastlund, I sent it to my friend, Adam [Faulser 00:59:51], 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 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 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 would be uncomfortable if we did not mention Adam’s involvement,
David: He deserves the credit that accrues. So not the blame, depending on how you [crosstalk 01:00:49].
Dan: [crosstalk 01:00:48] the blame.
David: Yeah. So I knew Adam because I was an intern at the time at [Galois 01:00:54], which is where I’m working right now. And he worked there at the time, and so we met each other that way.
Adam: Dan are you a convert now, like you mentioned at the beginning types maybe not your favorite?
Dan: Well, I usually think in terms of the structure of the problem, and sometimes the structure of the problem is not as friendly with Henley Milner. And I don’t care as 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 perfectly good choice, but sometimes they aren’t. It’s just that simple. We only have so many pages. We only have so many that the size of programs can only be 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 MLer with Matthias Felleisen, sure that’s a good time to do it.
And even in Little Java, a few patterns we ended up using types. But by and large it’s the ideas behind the problem that mattered 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, 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.
David: Not all types need to be checked by machine.
Dan: That’s a good way to rephrase it. I like that David.
David: I stole that from Matthias.
Dan: Oh, okay.
Adam: All right guys. Well, thank you so much for your time. The book’s great. I recommend people check it out.
David: And thank you very much for having us on here and also for putting in so much effort to read through the book.
Dan: Well, just keep trying. You’ll be fine.
David: If I may-
Dan: Just remember what I said about chapter eight, read it very carefully.
David: … and if I may insert one little plug.
Adam: Oh yeah.
David: I had a talk at Strange Loop recently where we had a demo of Pie 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. Because I know $40 is a lot of money for a lot of people, and if you aren’t sure whether or not you want to invest that in the book, 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.
Adam: All right. That was the interview. I’d like to thank the many people who promoted the last episode with Wade [Waldron 01:03:55] on Twitter, especially [Decode 01:03:57] 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 [inaudible 01:04:12] 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 conference is I think is really a good thing. Then I followed the conference by doing the [inaudible 01:04:29] training, which was great. I interviewed him back in episode nine and taking a four day training session with him was a great experience.
Using the Pie Language
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 scalp. All right, using the Pie Language. So the Little Typer uses this custom built language as was discussed called Pie. So here is my overview for working through the book. First of all, you want to download DrRacket and then install the Pie Language. And then [inaudible 01:05:14] top of your file you just have to put like a pound line Pie, easy enough. As you’re working through the book, my first tip is to read deeply and methodically. So the book is 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 get 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 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 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 in to DrRacket. You can use lowercase words in place of the Greek letters like Lambda and Pie.
And then what I found helpful with just playing with the code. So trying to run things through the [inaudible 01:06:27] to get a feel about what we were defining and try and 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 check same, that is useful for testing if the results of a function call have the… If the result of a function call have a certain value. So I found that quite useful for forgetting my intuition. I would type out a function from the book. I would then try running it in the [inaudible 01:07:04] with some arguments and then to solidify that knowledge, I would put in a check same this [inaudible 01:07:11] 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.
Sticher
Overcast
Dec 02, 2024
42
min