CoRecursive: Coding Stories - Tech Talk: God's Programming Language - Philip Wadler on Haskell

Episode Date: October 22, 2018

Tech Talks are in-depth technical discussions. Today I talk to Professor Philip Wadler, a very accomplished programming language researcher.  Phil walks us through a principle that has guided his career.  That principle is that typed lambda calculus is not invented but a discovery of a deep truth. It is something connected to the mathematical underpinning of the universe itself. It follows from this that functional programming languages are therefore more correct or more deeply justified and fundamental than other languages.  I am probably stating things in a stronger fashion than Phil is comfortable with, but I like fp, so I can be a little hyperbolic. While explaining this principle, that has guided his career, Phil takes us through the history of computer science.  We start with Turing and Alonzo Church.  Eventually we get to what the movie Independence Day got wrong and what language a theoretical creator deity would program in. Show notes: talk paper   Web page for this episode CoRecursive On Twitter CoRecursive On Itunes

Welcome to Code Recursive, where we bring you discussions with thought leaders in the world of software development. I am Adam, your host. I'm going to stick with Russell here and say our dedication should be to truth rather than to efforts to be widely known. Hey, Philip Wadler is a very accomplished computer scientist, a great communicator, and also occasionally dresses up as his alter ego, Lambda Man. He has a paper and a talk where he gets close to saying something like functional programming languages are superior to other languages. Today's interview, along the way to arguing this point, we explore computer science history, lambda calculus, alternate universes, space aliens, and what programming language a theoretical creator of the universe would use.

Phil is a super interesting guest, and the bits of computer science history we touch on, I find really fascinating. Before we start the interview, if you are enjoying the podcast, please rate or review us on iTunes. It really helps. So I have this paper of yours here. I'm going to shake it so maybe they can hear propositions as types. And there's also this great presentation you've done a couple times about it. So I wanted to talk to you a bit about it. I found it to be very interesting. I highlighted one section here in the introduction that says, those of us that design and use programming languages may feel that they're arbitrary, but propositions as types assures us that some aspects of programming are absolute. It's kind of a big statement i would say yeah yeah it is sort of a big thing and i know many people disagree with me but for me this is highly motivating when i first understood about propositions as types it well actually the first time i saw it i just thought oh that's just a funny coincidence. That's cute, but of no significance.

But after a while, it became clear that it wasn't just between a particular system of computation and a particular system of logic, but rather pretty much any system of logic you could name had a corresponding system of computation and vice versa. And even that sometimes looking at interesting logics could give you interesting systems of computation. So it ended up becoming a theme of my research career, probably the most important theme in my research career. And yes, I feel very strongly about it, that this is telling us something quite useful and quite important. And it's very often, you know,

computer science is a horrible name, right? It's horrible for two reasons. It's horrible because it has the word computer in it. It's a bit, Dijkstra's pointed out that calling it computer science is a bit like calling astronomy telescope science, right? It's not the telescopes that are interesting, it's what you can see through them. And then the other thing that's wrong with the name is that we have science in it. If you're a real science, like physics or astronomy, you don't feel a need to put science in your name. It's only if you have an inferiority complex and feel that people won't take you seriously as a science that you need to

put science in your name. So I much prefer names like computing or informatics, which is the fancy name we use for it at Edinburgh. And it's relatively rare that you see things that make you think, oh, this is getting at deep insights of the kind that you get in physics or mathematics. But this, even though it's really very shallow, it's almost just a pun, it feels to me like it's getting at something deep and important. So let's back up and let's try to get to that place. So what is computability theory. What is computability theory? So that's the one other claim, I think, or it was certainly the first claim that computing made to say, there's really something interesting here with content. And the beginning of that was the observation that you could build a universal computer, that there was a way of – well, actually, no, it goes back independent definitions that came along. One from Church, one from Gödel, and other. Turing was completely separate. It was something he did basically as an undergraduate student. One of the most cited papers ever was done by Turing as an

undergraduate student. The fact that three different people found the same thing independently really gives you a lot of evidence that you're onto something. And so the thing they found is, I guess, the Turing machine is probably the term I'm most familiar with. Right. So there's three different terms. Church's term is lambda calculus, which you might have heard of. Gödel's term is recursive functions. And what Turing came up with is what we now call Turing machines.

And the point was that all three of those had exactly the same computational power. And then Church's thesis says, this is what you can do with a computer. And Church sort of just baldly asserted it. And many people looked at lambda calculus and they went, wait, no, why should this correspond to what a computer can do? And, you know, of course, this was back in the 1930s. This was before they had digital computers. They did have computers. There were things around called computers. If you've seen the movie Hidden Figures about early work at NASA, they had a room full of computers. These computers were women that sat around doing computations. And one of the

interesting things is that a lot of this work, which was actually fairly sophisticated work, for some reason they decided that, oh, we'll just let the women do it. And so when the first computers came along, they said, oh, well, the women have been acting as computers, we'll let them program it. And there was an interesting stage where people suddenly went, oh, actually, programming computers is really interesting. This isn't women's work, this is men's work. And there was this whole big shift to push women out. And now, of course, we're very keen to bring women back in to say, no, we need a diverse range of views here. We don't want just a bunch of geeky men doing this. We want a diverse range of people doing it and trying to restore the balance again that we – it had been balanced the other way at first, and then very much unbalanced.

So it only took us 70 years. It was quite a way back. The way I first heard about it is when I was in high school, one of my friend's mothers had been one of the early computer programmers. And so it was first from her that I heard about this history. And it was her who said, oh, well, when the men figured out it was interesting, they kicked us out. And eventually I found other historical documents describing that. And this is really something that we need to fix now. Definitely. I definitely agree with that. So, but anyhow, computer didn't used to mean a machine. It meant a person, as it turned out, Definitely. I definitely agree with that. them. And there were three different definitions that came up, as I said, churches, which was

lambda calculus. And people just looked at that and said, why should that correspond to what people could do? And then Girdle's, where, in fact, what happened was Girdle went to church and he said, I don't believe your definition. And Girdle said, fine, if you think my definition is wrong, you come up with your own definition. Probably not quite as testily as I put it. Maybe it was even more testy, I don't know. by Church's student, Kleene, who also became famous in logic and computing. So Kleene took notes as Gödel presented this at Princeton, where Church was, at the Institute for Advanced Study. Oh, sorry, no, this was before there was the Institute for Advanced Study. This was before the war. The Institute for Advanced Study was founded during the war at Princeton because there were all these German Jews that wanted to get out of Germany,

like Albert Einstein, and Princeton wanted to attract them, but they were anti-Semitic enough that they didn't want to actually have them at Princeton, so they created the Institute for Advanced Studies. So it's a very prestigious institute now, but I've been told that the reason it exists is due to anti-Semitism. So going back to the story, pre-Institute of Advanced Studies, Gödel came to visit at Princeton. And he said this to Church, and Church said, fine, you come up with your own definition. Gödel gave a series of lectures. It was actually printed as a paper written by Church's student, Kleene, who took notes of the lectures and attributed it to Girdle.

And they then sat down, and they proved the two were equivalent. And when Church went back to Girdle and said, look, your definition is actually the same as my definition, Girdle said, oh, is it? Hmm. I must be wrong then. And the impasse was resolved by this young undergraduate student, Turing, who came up with his own definition, Turing machines.

And unlike Church and unlike Gödel, Turing wrote a whole section of the paper explaining why what a Turing machine can do should be done by lambda calculus or by recursive functions or by a Turing machine is often referred to as Church's thesis, because it was just plunked out there. Here, this is what they can do. But Turing actually gave evidence, and there are people who claim, well, it shouldn't be called Trich's thesis, it should be called Turing's theorem. Because some people have classified the sort of argument that Turing gave as saying, well, let's assume that what people can do are this, this, and this. And under those assumptions, he then actually, as it were, proved a mathematical

theorem showing, so what they can do is exactly what a Turing machine can do. And at some point, this all bumps up against, like, isn't Girdle the undecidability and halting problem? That's right. It was Girdle's proof of undecidability that got this all going. Because before Girdle proved undecidability, everybody thought that what you'd be able to do is build a computer that could resolve any question in logic and hilbert gave a famous speech where he ended by saying we will know we must know talking about this idea that logic could do anything. And implicit in this, the notion that you could have a computer program, as it were,

although again, this is just before there were computers, that would solve any logically well-expressed problem for you. And ironically, the day before Hilbert gave that speech was when Gödel, at the exact same conference, presented his proof of undecidability. And so some people think it's ironically very appropriate that what appears on Hilbert's tombstone is that phrase, we will know, we must know. Oh, really? We must know, we will know. Yes. And somehow, as I understand it,

like undecidability has something to do with kind of this riddle of like the barber who shaves. There's a barber who shaves everybody who doesn't shave themselves, who shaves the barber. And so that statement, if you think it through, it kind of bounces back and forth between he shaves himself, but he can't shave himself.

Right, because if he shaves himself, well, he only shaves people who don't shave themselves. So if he shaves himself, that can't be right. Okay, so then he doesn't shave himself. Ah, but he shaves everybody who doesn't shave themselves. So he must shave himself. Right, it's very similar to that. The fancy name for the barber's riddle is Russell's paradox.

So there'd been a lot of work on set theory. People basically said any well-defined property defines a set. And Russell said, wait a minute. So in particular, this was in the work of Gottlob Frege, who was one of the earlier formulators of logic. He did very important work, and also, sad to say, a noted anti-Semite. Frege was writing this huge work on logic, and Russell was, again, a young student. I'm not sure if he was an undergraduate, but certainly a young student. And he discovered that what Frege was doing had a paradox in it, and the paradox was this. If any well-defined property defines a set, let's consider the set X consisting of all elements such all elements little y, such that little y is not in big X. Okay. So is big X in

big X or not? Because the set might contain itself. And the answer is, well, it's in itself if and only if it's not in itself, just like the Barber's Problem. And this completely undid all of Frege's work. And there's a sourcebook called From Frege to Gödel, a sourcebook in mathematics by a man named van Heijenhort. And in that, he reprints Russell's letter to Frege, along with a commentary by Russell about this. And I'll actually look it up and read it to you, because it's beautiful to read to you what Russell actually said about this.

So Russell's letter to Frege is just a page long explaining all this. Russell wrote a very nice paper. So this was actually the beginning of what we call type theory, the way that Russell solved the paradox was by introducing what we now call types, in fact, what Russell called types, so that it didn't make sense to talk about a set belonging to itself and ruled out some other things as well. So this was actually very important. But Russell's paper on type theory is beautiful because it begins with 10 pages of different stories, all corresponding to what we were just talking about. So one is the Barber's Paradox. One is, there's a special name for a kind of word that whether the word

refers to itself or not. And then he came up with a special name for a word that doesn't refer to itself. That has the same paradox, and so on. So it goes on for like 10 pages with variants of this paradox, and it's very readable. We never have technical papers these days that are as readable and entertaining as Russell's introduction to type theory, and we really need more of that. So anyhow, here's what Russell said to van Heijenhort. Dear Professor van Heijenhort, I should be most pleased if you would publish the correspondence between Frege and myself, and I am grateful to you for suggesting this. As I think about acts of integrity and grace, I realize that there is nothing in my knowledge

to compare with Frege's dedication to truth. His entire life's work was on the verge of completion. Much of his work had been ignored to the benefit of men infinitely less capable. His second volume was about to be published, and upon finding that his fundamental assumption was in error, he responded with intellectual pleasure, clearly submerging any feelings of personal disappointment. It was almost superhuman and a telling indication of that of which men are capable if their dedication is to creative work and knowledge instead of cruder efforts to dominate and be known. Yours sincerely, Bertrand Russell. Wow, so he took it well. That's a beautiful story. So an interesting or confusing thing, I guess, to me, I guess would be, so we're in the 1920s, 1930s.

Besides, you know, misogyny and anti-Semitism, these men of the time come up with like type theory. But types, when I first learned C,, types were like a representation of the width of bits that I'm storing somewhere. But we don't even have computers at this point, but yet types exist. Yes, and interesting. So, I will address that in a moment, but let me go back for a moment, because I've gone off on all these tangents. Let me tell you the rest of the story about Gödel. So, as you said, Gödel came up with something very much like those paradoxes, but it was slightly different. So, what he did was he said, consider this statement is not provable. Ooh, okay. So, if it's true, then it's not provable, and you have something true that's not provable. That's unfortunate. Okay, let's say it's false.

So, if it's false, then it is provable, and you've proved something that's false. It really undermines the definition of proof. And even the Nazis, people like Jensen, who was a Nazi but developed really interesting bits of logic. The idea that you could prove something that was false, they really were against that. I'm not sure people in the Trump administration would be against that, but certainly in the early days of Germany, they were very much against that. So you couldn't have that, right? That would just undermine the definition of proof. So it had to be the other possibility, but that meant that there was a true statement that was not provable. And of course, the trick was, how do you show that you can write a statement that says this statement is not provable? And what Gödel had done was he showed how to encode logic as numbers. So he came up with this thing called girdle numbering, where basically you use the prime factorization of a number as a way of representing a string

of symbols. So he could take any string of symbols and encode it as a number. And so statements like, this is a well-formed statement of logic, became a statement about a number. Or this number actually represents the proof of a statement of logic represented by this other number became a statement of logic. Sorry, it became a statement about numbers. And then he showed that indeed, there was a number that corresponded to the statement, this statement is not provable. It's kind of a trick. Yeah, but it was because, so that was a statement about numbers, right? The statement, this statement is not provable, had a particular number.

I don't know that anybody's actually computed the number. That would be a fun thing to do. Well, I should set that as an assignment for a student to compute the actual number that means that is the number of the statement. This statement is not provable, but there is such a number, a finite number, and that's what gets you into trouble. So that's how they showed that things were undecidable. So there were some things that you can prove. At that point, people went from thinking, oh, hmm, maybe there's not a computer program that can solve every possible question of logic. And in fact, again, the example they came up with is what we now call the halting theorem.

And we normally think of it as Turing's halting theorem, but it was actually earlier proved the exact same result by Church. And again, you can show there's a question that no computer program can answer. And the question is, given an arbitrary computer program, does it halt or not? And the reason why, again, is if you had such a thing, you could very trivially computer program that takes itself as input, that takes its own text as input, and therefore corresponds to this program halts if and only if it doesn't halt, the same paradox again. So to prevent you formulating that paradox it has to be the case that there is no solution no general solution to the halting problem and these all involve sort of self-reference or at least the halting problem involves like a program looking at a program the the girdle system involves encoding rules within like there's a self-reference theme.

Yes. Yeah, self-reference is definitely part of it. And self-reference is very important in computing. Anytime you're using recursion, you're defining a function in terms of itself. That's an example of self-reference. And in fact, if you look at the particular lambda term that encodes this idea of recursion, it's something called the fixed point combinator or the Y combinator, which happens to be the name the early logicians gave to it. It's the same thing written twice next to itself, which is what allows it to do this kind of self-reference. And actually looking at that structure, I thought that looks a lot like the structure of DNA and the way in which DNA allows it can be replicated.

Indeed, if you look at the letter Y, it looks like a strand of DNA unzipping. That's true. I think there's some interesting work to be done showing that anytime you have self-reference, it actually involves two copies of the same thing. But I don't know a fruitful way into proving that. I don't know anybody that's done that. I think there might be something interesting to be done there.

So, to bring it back, if we go from lambda calculus, and now we have types introduced, what does that give us? Right. So, we've got all these paradoxes. Oh, by the way, it's because there's this sudden rush after Gödel proved this that you get three people giving definitions of computability at that time because as soon as Girdle proved his result, people thought, oh, you probably can't decide everything with a program. But to give a proof of that, you need a definition of what a computer can do. So before that, people didn't care about the definition of what a computer could do. When they said there is a computer that can decide, they conjectured there'd be a computer program that could decide whether any statement of logic had a proof or you could prove its

negation. So they referred to that as it would be effectively decidable. And if you had such a program, you could just look at it and go, yep, that's a program. It would be sort of like Justice Stewart's definition of pornography. I know it when I see it. But if you wanted to show, no, there's no way of doing this with a computer program, then you have to know what computer programs can do. And then you need a formal definition of computer program. And that's why you had three different definitions of computability coming out at the same time. Because there's this rush to say, wait, to prove it's undecidable, we need a definition of computer. How do we define that? So it's not an accident that you had three at the same time

have you heard this term the the adjacent possible before no i have not okay so it's an interesting term uh from people who looked into like uh things that are co-invented like the telephone for instance invented in two places at once right but um it required the you know a proper understanding of of like uh electricity and a couple other concepts. And once those concepts were laid down, then the telephone was adjacently possible. Everything to come up with that concept was already available. It was just one step. So then I think that's a similar concept here. Yes, that's exactly right. So very often when you have the same thing invented several times in a row, sorry, several times in near succession, it's exactly for that reason.

And in fact, I remember reading a paper about that, which had a list of about 10 different different things that were all independent inventions very close to each other in time of these different things. The phone being one of them, and if I remember the story right, it turned out that as Alexander Graham Bell was walking down the steps of the patent office, having just patented the phone, somebody else was walking up the steps about to try to patent the phone. Yeah, I think I've heard a similar story. So yes, that happens a lot. And in fact, the thing we're about to talk about, propositions as types, seems similar in that, again, you end up with two people independently inventing the same thing,

one doing it as part of computing and one doing it as part of logic and doing it at about the same time. But in that case, I don't think it's about the adjacent possible because there's not a single development that was enabling both of those things to happen at that time. And sometimes it was quite a while before people realized they had done the same thing. Are these, using a term from your paper, are these concepts invented or discovered? Right. So in the paper, I say, well, the fact that two different people working independently come up with the same thing suggests that the right thing to call this is discovered, that there's something fundamental there that people are finding. And other people prefer to say, no, it's just this reflects the human mind, and they both had human minds. They both invented the same thing. I'm not even sure if that's a arbitrary and that arises somehow? Is it part of the structure of

the universe? I don't know. But there's something quite important here. Then I'm happy. I don't really care whether you use the word discovered or not. I find that the word discovered is a good way of conveying this. Yeah, and you touch on a number of examples, not just this one, I think, in your paper, like type inference and... Sorry, I don't have this in front of me. Like the ML type system, I guess,

has some roots in an earlier logician or? Yes. So, well, let's go back for a moment before talking about that one and talk about the first one. Okay. So the very first thing, which was, is to note that

if you look at the way that Jensen formulated logic in a paper he wrote in 1935, and you look at Church's lambda calculus, and in particular, the first type system that was attached to Church's lambda calculus, which was done in the 1940s by Church, because he'd used lambda calculus sort of as a macro language for writing down statements in logic. And then he found out because it supported recursion, you could write down the statement A, which is equivalent to A implies A, which it was already known due to Haskell Curry, had worked out something called Curry's paradox that says, if you can ever write down such a statement, then you can prove A. And if you could write down such a statement for any statement of logic, you could prove any statement of logic. So you'd better not be able to write down these statements. That was sort of okay because they were, in effect, infinitely long. Maybe you want

to rule out things that were infinitely long. But by just allowing arbitrary lambda expressions, you could actually write down a statement with this property. So his logic became inconsistent. So that's why he introduced type theory, for much the same reason that Russell had introduced type theory to types to sets before. Church introduced types to lambda calculus for this purpose. And you were saying before, oh yeah, but people ended up using types for very different things, meaning like how many bits were in a word. And one thing I've not been able to track down is the direct line between using type the way Russell and Church used it and using type the way Bacchus used it in Fortran, which I think was the first use of the kind you're describing. But I suspect

that Bacchus in fact knew about the work of Russell and Church, at least indirectly. Turing certainly knew about those, and Turing started using the word type for these things. So Turing is probably the connection. But I was never able to, John Bacchus unfortunately died before I got around to thinking, oh, I should ask him if he got this from Turing. So I don't know if he did, but I suspect he did. And that's why we use the same word for both these things. But also there, like as you're saying, there's some sort of conceptual isomorphism or something. So the way we use types now, certainly in functional languages, corresponds directly to the way that Russell and Church was using it. But the types that

appeared in very early computer languages like Fortran were much more restricted. As you said, it was things like, is this an integer or a floating point? How wide is this numerical representation? How many bits are in it? But I believe that that usage was inspired by looking at the usage of Russell and Church and Turing. So Turing probably made the leap, was the first person to make the leap from one of those to the other. The thing that I like about your paper here, I guess, is you're saying, the fact that typed lambda calculus came about several different ways and has strong roots in logic. I mean, it implies that the languages that follow this structure maybe are following a correct structure, or I don't even know if you'd use the word correct.

Well, they have more justification than the design of,32, and then simply typed lambda calculus in 1940. And it turns out that simply typed lambda calculus and a subset of Jensen's natural deduction, the subset corresponding to implication, are identical. They are formally identical. But as far as I know, that formal identity wasn't written down until Howard wrote it down in the late 1960s in a paper that was circulated in Xerox form and wasn't published until 1980 in a festschrift devoted to Haskell Curry. So it was between 1940 and 1969, that's close to 30 years, before people noticed, wait a minute, these are exactly the same thing. So there are concepts, maybe you won't say this, but I'll say it. There are concepts that are innate to the mathematical underpinning of the universe, and they seem to be invented or discovered because they're part of this underpinning by multiple people. And it seems to be always logicians. And then eventually computer scientists.

Is that right? Yes, I wouldn't put it quite as bluntly as you put it. I'm not sure that putting it that bluntly is justified. And if you tend to overstate things, even going so far as just saying that things are discovered rather than invented, you'll find lots of people willing to argue with you. And as I said, I'm not sure that those arguments are fruitful. But I think if we just want to say there seems to be something fundamental and important going on here and something interesting and worthy of study, I will settle for that. And yes, this fundamental process is at the core of type lambda calculus, which is at the core of every functional language. I don't know anything that has that interesting property of being discovered

independently twice that's at the core of imperative languages or object-oriented languages. So, you said I shouldn't state things so bluntly, but... You can do whatever you want, explaining why I don't find it productive to state things that bluntly. Yeah, you know, I really had as a goal in this interview to get you to say, type lambda calculus as God's programming language, and I can put that as a quote. I have said that in the past. I've said exactly that. And when I said that, somebody got up and walked out of the room because they didn't believe God had any role in talking about science. And indeed, I said it even though I don't believe in God.

I'm Jewish. I regularly attend shul. Tomorrow is Yom Kippur, and I will go to that. But I do not believe in God at all. I'm not a Jewish agnostic. I'm a Jewish atheist. As my colleague Gordon Plotkin puts it, well, you know, he goes to the orthodox shul. I go to the liberal shul, the reform shul. But, no, sorry, I go to the liberal shul. But Gordon says, well, yes, I don't believe in God, but I know exactly which God it is I don't believe in.

But yes, saying this is God's programming language, I think, is one way of conveying what I feel like is going on there. For a while, it was sort of the only way I could think of to phrase it that conveyed it very well, but not unreasonably. Some people got upset with that and said, no, God shouldn't be coming in here, and I can understand why you would say that sort of thing. But then the question is, well, how I've never had, uh, and I'm still looking, I think for the best way of phrasing it. Yeah. I mean, I think that it makes sense to say that like, like, you know, in our number system, like prime numbers are, are what they are. Like you don't invent a prime number. You, you just verify that it's prime and maybe there's some extension of this concept that that um that applies yes and that same debate right our prime numbers invented or discovered

uh you'll find people um debating that as well so maybe i should just explain it by saying these languages are prime. There you go. Maybe that's a good phrase to use. So in your paper, you actually use aliens to explain this concept. And the movie, I think, Independence Day. Oh, yeah, I've sometimes used, right, if you look at the movie Independence Day, at one point, it's actually a remake of Wells' War of the Worlds. At the end of War of the Worlds, the invading Martians are destroyed because they catch a human virus. And back then, right, when War of the Worlds was written, people didn't know very much about biology and how you prevented these things. The notion that Martians would fall prey to them seemed completely reasonable. Now we would say, well, why weren't they wearing

biological shielding when they went to invade the earth? We would understand this sort of thing. In Independence Day, the invaders are destroyed by a computer virus that they're infected with by, I think it was Jeff Goldblum. And again, that movie was a while back. We now know a little bit more about computers, and people would say, well, why didn't they have antivirus software on their computers? But also, if you freeze-frame the movie and look at the bit where he's downloading the virus, you can see that it's written in C. It has lots of angle brackets. In fact, the screenshot that I have is a dialect of C that only has open angle brackets.

They never got closed. But the time I saw that movie, I had just moved to Bell Labs, and Brian Kernighan and Dennis Ritchie were my bosses and were in offices just down the hall from me. So I thought, this is cool. Something they've done has made it into a very popular movie. So I thought that would be neat. I still don't know any popular movies that have Haskell in them. But the concept... But the notion, right, that the alien computer was running C, that really doesn't seem very likely. So it should be running something derived from typed lambda calculus. Not really. So I don't think you could give an alien computer a virus by giving it lambda calculus any more than you could give it one by giving it C. But what I do think is, let's say that we tried to communicate with aliens. We've done that, right? The Voyager, I think it was,

had a plaque on it trying to communicate with aliens. And you might try to communicate by sending a computer program. And maybe we could send a program in C, and aliens would be able to decipher it. That might work. Or it might not. Maybe they would just find that too hard. I think if we sent them a program written in lambda calculus, they would be able to decipher it, that they would probably have gotten to the point where they had discovered lambda calculus as well, because it is so fundamental, and that they'd have a much easier time deciphering that than deciphering something written in C. And in fact, I go on, I'm explaining this to say, even if you were in a different universe, let's say, had a different gravitational constant or something like that, right?

And scientists actually talk about, they point out that the different constants of our universe are finely tuned. If they were a little bit different, matter wouldn't have accumulated. You wouldn't have life. There'd be nobody here to observe the universe. Oh, maybe that's why they're so finely tuned, because we're here to look at the universe and wonder about it. So they think about, well, maybe there are other universes where they're different.

I can't conceive. Maybe it's just a limitation of my own abilities. That's quite possible. But I can't conceive of any kind of universe where you don't have the fundamental laws of logic, and therefore where you don't have lambda calculus, which is isomorphic to the fundamental laws of logic. And so, yeah, so the way I put this is by saying you can't call lambda calculus universal a universal programming language because calling it a universal programming language is too limiting right it works in all universes not just in one universe and I tried to come up with a word for it, and I couldn't. Eventually, somebody suggested the word to me, omniversal. Omniversal. So in the great multiverse, if I were to slip through to some other permutation,

then perhaps PHP would not exist, but some functional programming would? That's kind of the concept? Yeah, I suppose the idea would be no matter where you went, you wouldn't necessarily find PHP, but you would find some descendant of Lambda calculus as a programming language. Oh, that actually sounds like an interesting science fiction story. Of course, what actually happens in any of these stories about parallel worlds is you find somebody identical to you. They look exactly like you, and they've had exactly the same life as you, except for one small difference. Like, you know, there'd be somebody exactly like me, but who wasn't born Jewish or something like that. Yeah, I have, like, I've had a very small version of this, not to do with the multiverse at all just in that when i was

learning haskell there was a lot of concepts for me to learn and at some points i got frustrated with them and then when i was learning uh scala um all of a sudden all these concepts were here that i thought were just like weird haskellisms they were actually actually maybe more innate to the way the programs were structured ah yeah that's a nice version of it, isn't it? So it means when you go from one programming language to another, you find friends. Yeah, the things that a programming language exposes that are kind of part of this innate area,

you should find them in other languages that have a similar backdrop or, I don't know, similar theoretical basis. Yes. Right, so that's a nice phenomenon. I expect that probably happens with languages that aren't functional languages as well. But you raise an interesting question. Does it maybe happen more often with functional languages? It might or might not. I don't know. But if it did, that would give some more evidence that we were on to something fundamental. I have no idea whether that's

true. I don't even have an intuition that that's necessarily true. It's an interesting question. It's super hard to say anything in depth because people who created these languages are often up on all kinds of programming languages and concepts tend to move around and right what's certainly true is if you look at object-oriented languages there's a huge variety of different object-oriented languages they They all have different formal bases, whereas pretty much every functional language will have lambda calculus as its formal basis, and they'll all be organized around very similar principles. Whereas for object-oriented,

there's quite a few different principles, really. Yeah, and I feel like there's some principles that are maybe... Some principles have trade-offs, but some principles, once you see them in a language, then you don't want to use a language that doesn't have them. So like generics, for instance, I think come from some of the FP world of like, you know, parametricity, but now is a pretty mainstream concept and if you're familiar with generics and you switch to a language that doesn't support them you're like this this horrible

yeah that's a nice example and that definitely came out of the functional programming community and indeed the basis for it something called polymorphic lambda calculus, or called system F. It's one of these things that was discovered twice independently. So the computer scientist John Reynolds came up with polymorphic lambda calculus as a way of getting at exactly what we now call generics. And at exactly the same time, the logician Jean-Yves Girard came up with System F because he was trying to capture some properties of second-order logic. And they turned out to be exactly the same thing. And it was quite a few years before Gerard and Reynolds became aware of each other's work. And Reynolds even told me that he went to talk at gerard's university and nobody told him about

gerard's work when he was talking about polymorphic lambda calculus i think like it seems like sometimes you have to squint to see the like they're not direct it's not immediately clear that these things correspond uh i'm guessing um no actually actually, system F, so you do, I think you do need to squint, right? You need 30 years worth of squinting to see that Jensen's natural deduction and Church's simply typed lambda calculus are the same thing. But no, as it happens, the correspondence between what Gerard did and what Reynolds did was very

close. They were both formulated as variants of lambda calculus with abstraction over types, which is what generics are about. Being able to write a bit of code that works at any type. So

I learned a lot from this paper and the talk is great. In the talk you have some costume changing that's quite exciting. Yeah, I'm not going to do that over the radio. I assume you're wearing some sort of Lambda t-shirt right now.

We can't see you, but let's pretend. You can imagine that. So I guess for closing thoughts as we wind down, why is it that these ideas don't seem to come from computer science first they seem to be coming from different areas um yeah the logicians usually get there before the computer scientist so if you look at these pairings like the um the type system that was independently discovered by hindley and milner hindley was several years before Milner. System F came a couple of years before Reynolds system. Many computer languages now are based on the next

thing Gerard did, which was called linear logic. And that was sort of interesting. By then, they'd sort of caught up with each other. And in fact, linear logic was published in a computing journal, not in a maths journal. And it was quite interesting when it was published. It was a whole issue of the journal, more than 100 pages. And the editor of the journal had to preface it by saying, we've not been able to get anybody to referee this, but it's so important that we're going to publish it unrefereed. And that was a good decision. That was an extremely influential and still is an extremely influential piece of work. I have an almost $4 million project funded by the UK government, then jointly with Imperial and Glasgow. And that's essentially developing ideas

that come from linear logic to try to apply them to communication protocols. So linear logic has proved to be extremely influential, and I think will continue to be for a long time. In the Rust programming language, many of the ideas in that are best understood in terms of linear logic. They don't use linear logic exactly, but it's coming from the same roots. Affine logic or something, as I... They'd be closer to affine than to linear logic, but again, they're not affine logic exactly either. The difference between linear and affine is just, in linear logic, you must use each fact exactly either. The difference between linear and affine is just in linear

logic, you must use each fact exactly once. You can't use it twice. You can't forget about it. You can't not use it at all. There's some older things like relevant logic where you can use things twice, but you can't forget about them. In other words, everything is relevant, so you can't forget about facts. Affine logic is the other way around. You can forget things, but you're not allowed to use them twice. Which is important, because that's a constraint you don't really want to have to deal with as a developer. You don't want to have to make sure you always use things, I guess. That's why you might want to be linear rather than

affine, that's right. And the reason that you might want to be linear rather than affine. That's right. And the reason that you might want to be, say, affine rather than relevant, so only use things once, is this corresponds to a limited resource. And in particular, it would correspond to not being able to alias something. If you can only use it once, you can't take an alias of it. And that means that when you're, say, sending a message along a channel, you've got the only copy of the channel. So you can update it to indicate, okay, I sent this message now. Now I'm expecting the next thing in the communication protocol, which is why linear logic is important for doing communication protocols. And the main

method of doing this is something called session types due to Kohei Honda. When Kohei Honda invented session types for doing protocols, he was inspired by linear logic. And in fact, there are sort of four main things in session types. There's send a message, receive a message. And the idea is that these are dual. If you're sending a message at one end of channel,

you must be receiving at the other end of the channel. And then there's make a choice or accept a choice. So at one end of the channel, you say, right, I've got two alternatives here. I pick alternative A. At the other end of the channel, you're saying I'm offering two alternatives here called A and B. And again, you want those to match up. So that make a choice and offer a choice are actually two connectives of linear logic. And Cohay did this in the late 90s. Linear logic had come along, or the mid 90s, linear logic had come along in the late 80s, 1987. and it wasn't until 2010 that Frank Fenning and Lewis Karish worked out that actually send and receive could be viewed as the other two connectives of linear logic.

And that then formed the basis for a lot of my research work. That's why I got involved with Nobuko Yoshida at Imperial and Simon Gay at Glasgow, who are carrying on Kohei's work. That's why I got involved with Nobuko Yoshida at Imperial and Simon Gay at Glasgow, who are carrying on Kohei's work. And that's where our big government-funded project comes on, what are called session types, comes from. So that's good. I've gotten a reference to my day job. Well, I have another reference to your day job, maybe, which is, so Modologic and of Edinburgh working with Gordon Plotkin. And he'd worked out that monads were very useful for structuring the denotational semantics of programming languages. And I looked at that and went, oh, they're just as useful for actually structuring functional programs. So I was one of the first people to suggest using monads as a way of structuring functional programs. So I was one of the first people to suggest

using monads as a way of structuring functional programming. Andy Pitts and Andy Corden at Cambridge were suggesting very similar things at the same time. And it seems like if it's based on modal logic, the guy who invented modal logic was long dead at this juncture. Well, it wasn't based on modal logic. It was just done independently. It came out of ideas from category theory.

So monads are a structure that appears in category theory for dealing with things in algebraic topology, which I don't know, so I don't really understand the connection. But Monad's a very simple structure. It's actually very easy to apply in structuring functional programs. And then it turned out that – remember when I said that any interesting idea in computing, there'll be a corresponding interesting idea in logic and vice versa. And it turned out that there was a variant of modal logic that exactly corresponded to monads. And this was discovered by Valerie DePiva and Gavin Bierman. And I can't remember the other authors of that paper, but I think there were about four authors that had worked out this exact correspondence. And then later than that, Bob Harper told me, well, actually, there are lots of different modal logics. There were, I think, some given standard names. There was S1 through S8. And Bob said, each one of these corresponds to an interesting thing to do in computing. So there's a rich mine of data,

of ideas for programming language concepts if you just look in logic and squint, given 30 years? Yes. Waiting 30 years can be important. All right, Phil, or Phil, I guess. We've gone over. Is there any closing thoughts? Would you like to pitch your work or anything you'd like to finish with? Well, since we've mentioned 30 years, what I will mention is that when we first did Haskell, we never thought that it would become widely used.

And now it has. And I think this is the secret to having an impact in research. Do something good, stick with it, and just stick with it for 30 years. And if you keep teaching it to your students, some of them will go out and do amazing things with it, and just stick with it for 30 years. And if you keep teaching it to your students, some of them will go out and do amazing things with it. So I think it's really important. There's a lot of work where the government wants people to focus on whatever they think is important right now, like AI and machine learning or something like that. But I do think there's a lot to be said for finding something fundamental, sticking with it. And it turns out if you wait 30 years, or maybe sometimes 100 years,

you'll find out that that was well worth doing. And it gives you a great legacy as well. I'm going to stick with Russell here and say our dedication should be to truth, rather than to efforts to be widely known. Nice. Well, thank you so much for joining me, Phil. It's been very fun and interesting. Okay. Well, thanks very much. I enjoyed that. All right, there we go. That was the interview. Thanks to so many people who retweeted the previous episode on Twitter, or who mentioned it on Reddit or elsewhere. If you liked the show, tell your co-workers when you

are hanging around the proverbial water cooler. Or if you work remotely, like myself, leave a review somewhere. If you have any guest suggestions or feedback, shoot me an email.