On the Expressive Power of Programming Languages by Shriram Krishnamurthi [PWLConf 2019]

[Music] hello I am Shriram this work that I'm presenting is most assuredly not mine I will do my best to not lapse and talk as if it's mine and if I do it is not mine I'm not wearing a lanyard because apparently it's interfering with the audio and that's more important I am a green lanyard in case that matters to anyone and so what is this paper about it's got this slightly obscure looking title it says what is you know it's on the expressive power of programming languages the actual author's photograph is up there that's Matias for licence so in spirit he's hovering over us right now so what is this paper about well you know there's a lot of things that we know about what can and can't be done in different computational models right so we have very sharp mathematical distinctions if you've ever had the fortune or misfortune depending on who taught it a course on theory of computation or you've cracked open a book on the topic you know that there's these very fine-grained distinctions we know how to draw and yet somehow and so these are actually useful to us as a language designer this is invaluable to me when I design languages I think if I add this what does my theory textbook tell me might happen is that a consequence I'm ok with when I build verification tools i exploit the fact that I can live inside small languages that have limited computational power so I can do very rich things with those languages ok I've made a living off of this it's been good unfortunately we hit this point this this sort of a Turing threshold ok and beyond which like everything is equal and when everything's equal we can't make any meaningful distinctions and really can't make meaning meaningful distinctions I can't rely on this toolkit that's really useful as a language designer verification engineer and so on ok and that's what this paper is about and if none of that meant much to you that's perfectly okay because we're gonna spend the next 49 minutes unpeeling all of that alright good now I want to just if you'll indulge me for a moment I want to take a moment tell you a little of my personal history with this paper on I started graduate school I was a computational biologist and and I had the the misfortune of having early success early success is really bad because you know my imposter syndrome kicked in in a big way and I'm like he's people are gonna find out I don't know any biology I really need to get out of this area as quickly as I can right late success okay you could sort of learn stuff as you go along early success is really bad so I looked around and I said what is a computer science thing I could do and I I don't even know how I found this paper it sort of fell into my lap I didn't ask Mateus for it I just somehow showed up and I remember the afternoon I read it and it was like one of the most amazing days of my entire life okay it's I still have the soft glow about that afternoon sitting in a Houston apartment reading this paper and so so that's why when Xion contacted me I said I know which paper I'm going to present now to be completely honest I have not read this paper literally in 25 years so I started to read it a few weeks ago saying you know I need to prepare a talk it couldn't hurt to read the paper and I got stuck on one of the proofs and at some point my wife came over to me and she said you know it's called papers we love not papers we used to love but it's all good it's all good I love it again I love it all over again and this opportunity helped me fall in love with it all over again okay so just one last personal thing I asked Mateus for a photograph of himself from the time when this paper was written and he sent me this so this is from about nineteen ninety one that's Mateus on the left the person on the right is named Bruce dooba Bruce and Mateus with my original Co advisers in programming languages so it's personally meaningful to me but Bruce was also very influential in Mateus constructing this theory he's acknowledged very prominently in the paper so really there's a little bit of Bruce's spirit in here as well okay good that's the end of the personal stuff we're ready to get going okay what is expressive well I could tell you but you know what's even better you could tell me all right so here's what I'm gonna do I'm gonna run this like kind of like I run my classes might work might not work let's give it a try so what I'd like you to do is I would like you to turn to your neighbor if you don't mind if you don't have an anxiety about this turn to your neighbor and introduce yourself make a friend come on go but okay we're back we're back we're back good so here's what's gonna happen here's what's gonna happen we're back we're gonna vote the way we're gonna vote is so there's lots of ways of voting we can raise hands the problem is I don't like with raising hands is you feel bad right if you get the wrong answer it's like everyone's seen that you raise your hand so instead what we're gonna do is we are going to hum can you all hum very good now don't worry we've worked it out with closed captioning we're totally on top of this it's not gonna be a problem if your audio lis impaired it'll be handled right there okay so we're gonna hum so here's what we're gonna do we're gonna play this game I'm gonna show you a series of things that are gonna look like this there's gonna be some language L and then I'm gonna add some feature F to it okay language L feature F you're gonna talk to your neighbors and decide whether you think this is an expressive addition to L is F an expressive addition to L and also y-you know yes or no everything's yes or no is that good we're clear on the rules of the game any questions if you understand the rules of game hum if you don't understand the rules of game hum good okay very good so let's start here's our first okay I have a language it has no loops and no functions and I'm going to add loops to it okay talk to neighbors ten seconds eight seven six five four three two one we're back okay how many of you think this adds expressive power how many of you think it does not Oh interesting why do you think it does you can what you could add confusion okay that doesn't it sound like expressive power to me I think I've caused confusion okay so um classic results from computational theory that once we start adding loops we start adding expressive power we can add whole new kinds of computations okay theory of computation course good okay next question I have a wire language that only has while loops and now I had four loops to it how many go talk to your neighbors quickly okay I already got the answer how many of you think yes how many of you think no why do you think no what do you think not oh you can rewrite I heard the word rewrite you can rewrite one of those things into the other we do we like that answer we can rewrite one into the other very good okay next one for loops I had while how many of you yes how many of you know Oh No why wait that's why why not why not oh you might have some intuition in your head or well you know why loops are unbounded for loops are bounded so if I already have while loops I can add four but if F four I can't add while you see you're starting to form a little intuition here for what's going on okay very good next one I have a regular language and I had context-free grammars I know I know this is exactly the kind of offensive thing programming languages do okay okay very good very good I I will refrain from stating an opinion on this next I have a two-armed Emma if and I had a multi-armed if multi-hundred if I can have lots of if else else else else if else if yeah yes no no okay why why is it a No you can rewrite it again I heard the word rewrite you can just translate one of these into the other right it's not a big deal okay good um I have a pure language and I had state oh I've how many for a yes how many for a no Oh interesting okay why no carry the world state monad okay alright whatever does mean I'm not sure quite what does mean think they have something to do with the food trucks at lunchtime burritos just up okay um here we can do a few more good like that's due tomorrow okay so I have a language it has only binary Megan - and I'm going to add a unary - to it no why rewrite everyone's now using the r-word okay very good rewrite okay last one okay I have a language that has no exceptions or other mechanisms like it I'm going to add a halt operation how do you feel about that no I stated the problem I stated you can you give your problem later on okay okay how do we feel about this yes yes Oh interesting no okay dead heat good that means you need to stick around for the rest of this talk very good okay so here is our general issue okay we have some language l and we have some feature F and what we want to know is does the addition of F add expressive power to L right that's our problem and all of you has seem to have some sort of intuition thankfully your intuition corresponds to what I expected it to be otherwise this prior talk would be quickly about to go off the rails kind of like the same to us rail system I guess okay which is something about compilation right the sense that if he can translate a compile this bigger language L plus F down to L then we haven't added expressive power right that's the general intuition is that roughly correspond to what all of you been saying that's what you've been feeling deep down yes okay very good if this is your feeling then they're two dudes who'd like to have a word with you okay these two dudes right now if you don't recognize who they are that's okay their names are JavaScript and x86 I'm kidding kidding I'm kidding I'm kidding I'm kidding the guy on the right does Benedict Cumberbatch the guy on the Left is uh yeah let's go little arrow DiCaprio right looks close enough and let's say we want count dicaprio playing you know okay no no that's Church and Turing but I think I think you know Caprio in the church has Church on big screen would be a pretty good idea okay so what's the thing so Church and Turing have this church hearing hypothesis it's really I was taking about at simulation but you can think of it as a statement about compilation basically says look you can compile things you can compile all kinds of things into all kinds of things and you know this because you run programs on x86 is you run programs on JavaScript right you can even compile JavaScript x86 and my god it's 2008 a near compiled x86 to JavaScript right everything's intercom pilobolus and this is actually the problem so until we get up to the point of being able to express what are called Universal languages church-turing hypothesis well you have regular languages context-free languages there's a lot of really crisp mathematics that says one of these things is more powerful than another adding it adds expressive power okay whole theory textbooks devoted to this idea that there didn't look boring as hell but they're actually beautiful there's things called a pumping lemma like absolutely gorgeous stuff always mistaught okay but really gorgeous stuff worth reading worth understanding right but when we get tutoring it's like you know it's all good it's all the same but it's programmers that's not what we think you don't as a programmer think well every language is the same so mighta so read that why do we have an elm conference down there and why do we have strange loop well obviously we have strong opinions about these things but we don't have any mathematical way of telling them apart it's all a matter of opinion right and and like you know as you said am i trying to start a religious war that's what it turns into it turns into a religious war so the question is are we without any mathematics at all and that is the genius of this paper the genius of this paper is it lets us escape this phrase that Alan Perlis used the Turing tarpit right you get stuck in there and your feet are stuck and you just sort of like dissolve into the carpet and like as you're screaming and yelling at each other right it turns out we can we use mathematics to draw mathematical distinctions between things that we might have intuitive opinions about okay that's what this paper is about and that's what this talk is going to try to convey to you good okay and if that's not interesting too diverse there okay so now we talked about this intuition about compilation so I sort of suckered you into saying the intuition is like something about translation compilation and then I you know got you stuck in a carpet right I put you in the touring carpet but if you think about your intuition for a moment it's not exactly what I said I think your intuition was a little different your intuition was more like I can locally rewrite it right I can just do a local transformation if I have this multi-armed if I can turn it into a sequence of single armed ifs if I have a you know like if I have a a for loop I can turn the for loop into I'm going to introduce the variable and then I'm gonna do a while loop over that variable till I come to the terminating point right it's a local rewrite that's your real intuition right that's why you're like yeah this is not an interesting feature I can I can just write it a da right away right I could even imagine like a keystroke in my in my editor that just I press the keystroke and boom off it goes and expands everything away right that's your real intuition so so essentially your intuition is roughly speaking whether you realize it or not it's like simple lispy macros right okay good all right now that I have you where I want you okay so I like to think of it slightly differently I like to think of this as the Las Vegas principle okay so a Last Vegas principle is what happens inside parentheses stays inside parentheses and so it's a completely local rewrite it doesn't go wandering off outside the parentheses okay now just to be clear this is not a talk about Lisp in any way lots of languages have rewrites these days if you look at Python for example in Python there is actually D Shivering going on like X plus 2 is actually that thing it's a local rewrite okay Haskell even Haskell has local rewriting right all the comprehensions actually rewrite translate macro expand D sugar whichever term you prefer to use right into something that's just a sequence of local function calls we've been building a language called pirate and in pirate we have a bunch of these transformations too so this not a prefix parenthesis caught talk at all it's just the idea of doing program rewriting locally that's all okay we're good all on the same page all right good so let's now go back to talking about expressiveness when I want to say something as expressive not expressive there's two sides to this right so I've got L and I've got L plus F and what I want to know is is f not expressive how would I say that F is not expressive relative to L what would it take to say F is not expressive what would you have to do yell it out somebody yell out it show me a macro all right show me the macro just give me the macro and we're done right it's really simple it's actually a little more subtle than that right because you might write the macro but you may be wrong okay so really what you're saying is I'm gonna get let's assume I have a semantics for both of the languages okay let's then take every possible program P in the bigger language let's expand out that program okay and now I want to say that these two programs have the same meaning they're somehow the same that's implicitly what we mean right we're good little notation on the screen but hopefully the words are enough to help you get through the notation right okay hold that thought for a moment now let's ask the question what does it mean for F to be expressive relative to L what does it mean for this new feature to be rel expressive relative to this existing language oh you can't just give me a macro for that in fact what do you need to do you need to show that they cannot exist a macro right there cannot possibly exist a macro in like beyond the scope of your limited imagination but none of our imaginations in fact mathematically there can't be such a macro that's a pretty big ask that's the interesting part of this paper okay showing that that cannot be such a macro okay but both parts of this paper rely on some notion of equality some definition of equality okay now I have a question so let's take a vote again right we have a choice we can hand wave the question of equality or I can tell you why equality is an interesting question I mean it's just a quality or at equal sign but you know okay so how many of you want a hand wave like why is equality interesting how many of you want to know why quality is interesting good because I did not prepare the other talk okay so equality is hard okay but before I go into this there's always going to be some person in the audience right wandered over from my CFP ended up in the wrong room or something like that right and and I need to say this for you right everything I'm gonna say in the rest of this talk has a giant asterisk on it okay so there are all kinds of words that you will see in the formal definitions about capture free substitution etc etc they're all I'm gonna leave all of them out now are they important yes usually they are important for making the mathematics work out sometimes they're extremely important because they really changed the meaning of things sometimes they also provide insight but doing all of that is outside the scope of this talk when you read these papers play it some attention to these phrases basically if you think haha I found a counterexample your claim it's probably because one of these phrases I left out and that phrase covers that case so I make sense okay so I CFP people behave yourself now good okay so I said equality is hard hopefully you're not a bunch of academics but like programmers which means you're skeptical of this claim right so if you should be appropriately skeptical any term in academics as something is hard like oh come on really okay so you know here's a counterpoint it quality's really easy right so I'm gonna take two expressions e1 and e2 and how do I check whether they are equal or you could do something really simple I run a one run e2 and I compare the answers okay done ha is there anything on the board that should trouble you what's the word that should trouble you compare because I turn to equal into compare I haven't solved the problem really why is comparison hard you compare all the time right you're right test Suites they compare now of course anyone who's actually really written a test suite knows why equality is hard right but let's think about comparison for a moment what do we mean by comparison like do we mean string equality because then are these two things equal are they not equal are we now getting into philosophical discussions about you know like numbers okay what if my output is actually a function I get these two lambda terms right are they're not syntactically equal are they semantically equal I mean what are we going to do we're gonna send it out on Mechanical Turk and ask somebody do these functions through the same thing even worse what if my expression has free variables in it which is gonna be relevant later on in the talk you can't even run it are you gonna run an expression of free variables you can't do that what about closures they've got environments and stuff like that and if all of that sounds like very academic geekery stuff to you let me ask you to think about what about like things like timing right anybody who's ever dealt in the crypto world knows that these are extremely relevant questions because this is how you break crypto right it's really about equality you think you have these two implementations one of them leaks through power channels or timing channels or thermal channels or something like that and information is revealed okay now not only are these crypto problems not only these kind of like you know theory world problems every compiler writer has to deal with this because when a compiler writer optimizes something they're replacing one expression with another expression they better have those two expressions be the same okay so it's a very pressing problem that every compiler writer recognizes every testing person recognizes okay so equality is actually hard okay now there's this absolutely brilliant definition that is used in the literature and I want you to want to step through this definition with you okay it's a term called observational or operational equivalence and you may have run into it before if you've run into it and it made perfect sense great if you've run into it it didn't make any sense at all that may be an appropriate response because it's quite subtle and there's all this unwritten text and like theory that they never tell you so I'm glad the door is closed because I'm gonna tell you now okay so this comes from Jim Morris's dissertation and essentially this is not how it's phrased but this is the question that it's asking is there a way in the language of telling two things apart okay if there is a way in the language of telling them apart they're not equal if there is no way of telling them apart they are equal okay because if there's any way at all of telling them apart someday some program I'd use that way of telling them apart and now those things are no longer equal right this is what a compiler writer has to worry about what program might somebody someday write that would tell these two things apart okay so that makes sense as an informal understanding I'm gonna drill down from here okay so let's say we have a language like this you don't have to follow the grammar it's just some lambda calculus like language okay so I've got some language and the question is what are all the ways of using a piece of code well it's essentially all of the ways I can surround a program with more code those are the ways of using the code right so we're going to call this a context so context is I've got some chunk of code with a hole in the middle of it and that hole is where other expressions can go so here's an example of a context plus one hole so that's the context that adds one to something okay so it takes some piece of code and uses it in a context where it's adding one to it I might have a context that puts it in the middle of a function application I might have a context that puts it inside a lambda term and so on okay that's what a context is basically it's a chunk of code with a whole city if we could fill in the whole good clear okay and just for convenience in this talk I'm going to give myself a much bigger programming language now here is the definition first definition of observational equivalence okay for every possible context in the language see if I plug in a 1 in the context and I plug in e 2 in the context and I get the same result whatever that means the moment I get the same result then we'll decide that these two terms are equivalent ok if I plug in e 1 and plug in e 2 in every possible context then the two terms are equivalent right so essentially it's asking is there any way in the code of telling things apart so we ask these questions earlier about you know 0.999 versus 1 or you know program source code and all these other things well question is is there a way of telling that a slot part in your language if your language gives you a mechanisms for telling those things apart we shouldn't consider them equal if your language does not give you any way of telling them apart we consider them equal that you see it it's like a very practical programmer oriented definition of equality extremely pragmatic does the language give you a mechanism for telling it apart good yeah ah what does equality mean yeah yeah so as you can see so what just one quick comment the more observations you can perform the fewer things are equal but as you can see I've got a nice big red around that's what you were asking right ah ok so because we've still ducked the question in fact it's even worse um in a language like the lambda calculus there's everything's just a lambda term like how you could they're opaque you can't look into them like what are you gonna do with that right so Morris came up with an even more brilliant version of the definition okay and this will strike you as a little weird but but work with me on this okay Morris said let's not talk about like equality of things because that's what we're trying to define the more general definition is if c 1 c of e 1 halts if and only if c of e 2 holds oh I know I know okay now for the rest of this talk I need to say two things one is I need like a canonical way of talking about an infinite loop will you the term Omega to refer to an infinite loop it's a convention okay so Omega means like think of it as like going round and round okay so make us an infinite loop the other thing that's sort of relevant for what I'm going to do later is there's this little trick that people use in semantics which is if you have a program with an error you think of it as not terminating okay that's a technical thing I don't want to go into it in detail just you'll that's just relevant for one that's the one slide later in the talk okay so we're going to reduce everything down to whether things terminate or not all right and sometimes I'll also need to talk about which language we're either in language L or in the extended language so in that case I'll put a little annotation saying subscript of a means in the language a okay that's the definition we're gonna work with for this talk okay good no not good what are you people nodding your heads about like does this actually sound like this this seems to imply five is equal to six right they both terminate so talk to your neighbors for a woman and see whether you should buy any of my definitions I've thrown like PhD is that you doesn't mean you should buy it talk to your neighbor go in five in four in three in two in one and we're back who are back you people are worse than a high school okay so you buy this is five equal to six why not what context ah how about this context okay so the context says if whole equals five okay then I'm going to terminate otherwise I'm going to go into an infinite loop we said it's for all context remember this is one of the contexts uh-huh yeah yeah see that's how clever a definition it is okay now aah-ha-aah not so simple what if your language doesn't have the ability to check for like equality to five right maybe it's God like you know no equals particular numbers maybe it's just got zero question mark clearly then you can tell zero apart from everything else but you can't tell five apart from six unless maybe you have a context that looks like that you subtract five and then check of it zero see that's the thing that's the beauty of this definition it's overall context in your language okay now and this is the part they never tell you in the papers but this is what's so brilliant about this definition now what if there is no way of telling these things apart like there's no arithmetic there's no zero question mark there's no like you know subtraction then what five equals six there is no way in your language of telling them apart like what distinction is there now you might later go ha I can probe into the hardware well if you can probe in the hardware with your language then there's a way of telling them apart right otherwise it's outside the scope of your language your compiler writer can merrily optimize away okay are we good that blast which made this satisfy you a little bit we can get back to that later if we have time okay we're good so now we understand why is equality hard it's very subtle but we're going to work around it by using this brilliant definition from Morris and other people about what is called observational equivalence please it's called observational equivalence is it's equal under all the observations you can perform in your language right checking for zero is an observation subtracting something and checking something that's an observation all of the observations we're good okay now let's go back to talking about expressiveness okay so now I want to motivate the definition I'm gonna give you a definition of expressiveness but I want to motivate it so let's imagine we have a language where three we're and this is true just about any language I hope three is the observational equivalent to one plus two okay all right that's my language now could you imagine adding some feature F zero to this language such that three is still equal to one plus two what could you add to this language that would make it still be true there's so many things you can't even name one right all right you could add subtraction to the language and hopefully that leaves addition unchanged right okay so this is not hard to conceive of okay could you imagine adding some other feature f1 that leaves all of the things that were previously equal to still be equal you can like what could you imagine adding loops for instance may leave all of the things that were equals still be equal quite possibly okay all right could you imagine something like an f2 that would make three no longer be equal to one plus two once you've added it to the language you can what could you imagine adding yeah macros what else floating-point or any Python programs you're overloading right I can just overwrite plus to be something else right I could do it with a macro I could do it with overloading I can do to lots of things right I can just change the meaning of plus right okay so you see now we have different features and the addition of features may or may not have impact on what is previously equal so that makes sense that's where we're going okay very good so here is the key theorem in this paper hey suppose F can be written as a local macro I'm not exactly defining local macro it's done in terms of freely generated term algebras your intuition should be a local macro that has well relatively limited power okay so like a syntax rules macro if that means something to you okay so I'd have a simple local macro that just takes pieces and rearranges them like that do loop that I showed you earlier right the for loop right just rearranges pieces then suppose supposing I have two terms you want and then for every term that is equal under L okay for every term that's equal under L I'm guaranteed that it will still be equal when I add f2l okay for every term that's equal under L it's guaranteed to still be equal and I add after L this is not completely obvious this is like the core of the paper in some sense it takes several pages to like work through to get to this point but this is the key theorem basically it says that F has not added expressive power to the language right whatever L had as equivalences they're still there they haven't been changed F has not affected L in some material way that makes sense intuitively that that's what it's saying okay good all right now the formal statement looks quite different I'm just going to put it up very quickly I'm going to read it out just to show you that the papers written slightly different terminology it says that it's a conservative extension you will understand all of this based on this talk okay you can go back and read this and you can translate these terms it'll make sense I think okay so that's the that's the way the paper is written some I'm sure you talked slightly different but how do we show this is the thing right so we know that not expressive means you just write a macro down and you do some proof stuff but you know whatever just show that the macro actually doesn't do anything weird okay but how do we show something is expressive because remember this was our original quest we started out by saying we have a way of showing expressiveness using you know turing completeness versus non completeness the Chomsky hierarchy right regular context-free context-sensitive we had all of these ways and then when we got into the Turing complete world we could no longer express our views on expressiveness because everything was equal so now we want a way we've created all this machinery to give ourselves away to still show that things are expressive means not everything is completely equal right that's what we're trying to do so the interesting part is how do we show that something is expressive right if we read off the theorem essentially backwards here's the plan we start with two terms he wanted me to that are in the language L my base language such that they're equal okay they're equal in the base language now I have an extension F 9 new feature if we can find a context in this extended language such that e 1 and E 2 are no longer equal right that tells us that F is added power it's somehow F is messed around with L right it's changed FL in some material way things that used to be equal compiler rewrites that a compiler writer could perform they can no longer perform and if you think this is a theoretical question go talk to a real compiler writer okay every time rust adds a new feature racket adds a new feature Python adds a new feature whatever adds a new feature this is what the compiler writers have to do they have to ask what are the optimizations I used to perform before that have been invalided where is this new addition or is it the case that this is a truly orthogonal addition that doesn't invalidate anything that I used to optimize okay very practical question so good good so far so here's our game plan okay we have to find terms that were equal we then have to find a context that is going to invalidate their equality right okay and if we can show that then it turns out by that theorem that cannot be a local macro for it yeah but more at the point we've said something really powerful about expressions okay that's what we're gonna do so I'm gonna do this on three language features okay first let's take a language without exceptions and let's add a halt feature to it okay so halt is basically exit okay you give it a thing and it just stops the program it doesn't continue execution okay so reminder we need two terms okay you wanna need two and then we need a context in the extended language right two terms you want need two contexts the extended language so if we had you know if this were like a multi-day course we could build up all of these expressions from the bottom up I don't have the time to do that I'm going to show them to you but we'll talk through where they come from okay where the intuition comes from all right so here is my first term II one let me help you with the notation that is a function it takes an argument F and it ignores it it said what does it do can everyone do this yes okay so it takes an argument ignores it and infinite loops okay all right now here is my term e - I'm gonna take an F I'm gonna apply F to zero and when I get something back then I'm gonna apply that to an infinite loop since I have an eager evaluation language I'm gonna go into an infinite loop okay so it's pretty easy to see that these two terms are recover 'land when I say equivalent what do I mean equivalent by James Morris's definition right because no matter what F I give okay let's work through the first expression no matter what I if I give it does this second expression let's say I give it an F that is not even a function that's an error we remember by our technical definition that means it doesn't terminate or it is a function that well that function goes off into an infinite loop well great it's still an infinite loop or that function terminates on zero and what happens to the result we still go into an infinite loop okay so e1 and e2 are equivalent because they go into an infinite loop no matter what you apply them to good so in all contexts okay all right now here is so now I need to give you a context in my extended language right here's the context I'm going to give you and it's like it's brutally short the context is I'm gonna give halt as f what happens in the first expression what is e one inside that context halt goes in as F F is ignored and the result infinite loops second expression halt goes in as F and we say halt of zero and the result of that is zero okay therefore I have found two expressions that used to be equal that the act of adding halt makes not be equal okay now your first instinct might be to think oh okay so he played some technical trick on us that's very clever but matthias did really not me but you know like is there an insight here yes there is an insight the insight is the following let's not lose track of the fact that there's an insight the insight is when I add halt to my language I've added some real power to the programming language the power I have added is the ability to ignore all the pending computations right all sorts of computations were waiting to happen I ignored all of them and bailed out okay so all that I'm doing with e1 and e2 is taking the intuition and translating it into code right because e 1 is good and I have to do it in a technical way because of my definition Yi one is not gonna bail out e two is gonna have the potential to bail out in a language without halt I can't exercise that potential once I add halt I can exercise that potential do you see that so really it starts with the intuition of what's the difference what did I add because of this operator and then you have to construct the idea and then you have to do the mechanics to make sure I put like Omega is in the right place okay so really those two terms are telling us something quite profound about the difference between a language that doesn't does not have halt okay for those of you who know what call/cc is call with current continuation it turns out that works just the same way I could instead put in contacts were called CC because again a call CC of fi will still get omega and the e1 in the second case called CC of FF Fultz escaped my zero back out and so the same thing works there too okay good you see the game plan we see what we've done here right okay let me do a second language now haha this one's gonna be fun now then okay so um the terms are gonna be simple but the context is gonna be a little complicated I'll walk through the context alright so here is my first term it's a lambda that ignores its argument and applies F to zero whatever F is okay e to is gonna look almost the same I'll just apply F to zero twice in a pure language and if you're really picky we can try out convert the we can expand he two into a pure lambda term so you know there's like an implicit begin or something but we can just convert that into an abstraction so don't worry that's not that's not interesting here okay all right so basically whether we apply F once or whether we apply F twice what difference does it make it doesn't make any difference right it's a pure language F is always gonna have the same result so F applied to zero is going to be F applied to zero no matter how many times I apply it you see where I'm going yeah you see exactly where I'm going because I'm gonna construct my context now and I there's a lot of code so let me just walk through the code for those of you aren't familiar with how to read this what I'm gonna do is I'm going to define this function f it's gonna take a parameter it's gonna return the result of that parameter but along the way it's going to change the thing that f is bound to which is a procedure that is a diverging function an infinite loop okay so when I apply this context to e1 what happens is I I basically I'm gonna send 0 in write F is going to get 0 so 0 is going to go into the underscore position and be ignored F is going to get 0 it's gonna change F and return 0 and the computation terminates right in the second case it's changed F but when I come back in I changed F so when I apply F the second time I'm going to diverge right again there's some details to the mechanics of the construction how to put like and when it goes in the right place and whatnot but the insight is what does state do state gives us the power to count state gives us the power to count right sometimes as a functional programmer sometimes I really really want my programs to not to be like independent of time and sometimes I very much want my programs to be dependent on time or dependent on the virtualization of time in terms of events that have happened I want both things and state gives us that but what this is saying is if you had programs that you had considered equivalent previously now they might no longer be equivalent because you added this feature so you had to make sure that you added in a way that you know is reasonable for what you want to achieve okay oh and I forgot to show you this but you know that already okay good let me show you just one more example there's a few more in the paper the paper actually does some very interesting distinctions were in call by need and call by value that's quite technical I'm not going to go into that but I'll give you one more example it's very relevant to programmers let's say we have a language it has just a boolean value if it takes only true and false and anything else is an error we're gonna add a little truth e faulty if to it okay so we'll do like a lisp e true the list B if but you can imagine something else so let's be F is false is false everything else is true okay but if you're like a true scripting language programmer you know that the correct way to define F is through a very complicated table with about 17 rules that are completely obvious to every programmer except they are different between Ruby and JavaScript and Python everything else but they're all completely obvious anyway okay I don't have any opinions on this matter okay so here is my term my term is gonna be really complicated I will explain this term to you okay I actually have two terms remember e 1 and E 2 there's e 1 can you tell that there's a 1 that's in a color up there okay II - is gonna be the same term but it's gonna have an Omega in that place and you can tell haha something tricky is going on there right okay let me walk through this term for you okay so what are the possibilities B could be not a procedure okay if P is not a procedure then error right we can't apply an on procedure so is there any difference between e1 and e2 no because both of them the first thing they do is they try to apply EP not a procedure they terminate are they they go into an infinite loop or whether they don't terminate sorry error okay good but they have the same behavior okay another possibilities P actually applies its argument if it applies its argument that's going to diverge right which means again they have the same behavior a 1 and E 2 remember first I need to convince you that you want to need to are the same okay so that's what I'm doing so let's see it applies its argument diverges third possibility B takes its argument and feeds it to you know addition or something like that that's an error but that's true for both u 1 and D 2 okay fourth possibility B puts its argument in a boolean if position is that a boolean no it's a function okay so again you want to need to or the same the fifth possibility is actually the very interesting one which is that P ignores its argument if P ignores its argument it must be a constant function if it's a constant function let's say it always fix false then we're going to go to the Omega case in both cases if it's always picks true we're gonna go into the nested biff and that's gonna go into the zero position so we're going to go into the zero position in both cases so the key thing is this very cleverly constructed term we never get to the orange term it's dead code okay it's dead code in a language of boolean ifs but now when I add my Lisp EF here is the context I'm going to define okay I'm going to say that p is a function that takes its parameter does a list B if and gives you the true or false back okay so now what has happened is if I apply this to e1 what happens well e one is the lambda is a true Val so it's gonna basically it's gonna in both cases the lambda is a true value so it goes into the bit nested BIF at that point the false is a false value so it goes into the else so in p1 it's gonna go to one in p2 it's gonna go to Omega and that is exactly the distinction that I needed to show termination versus non termination okay what's the insight here the insight here is a truth e faulty if allows us to perform more observations than a boolean value if does okay okay so that's my short tour so these are local versus global transformation the topic we started off early on now in a pure language you can add state by doing store passing style but that's a global transformation you can add control operators to continuation passing style that's a global transformation what this paper tells us is maybe you have a different global transformation but you cannot do it as a purely local transformation right that is one of the consequences of this paper right and furthermore more profoundly they really do add expressive part of the language so let me wrap up now first what have we learned we learned a really awesome definition of equality right really cool definition of equality it's used all over the literature second really neat definition of expressiveness right we've gotten ourselves out of the Turing tarpit we can now make distinctions between language features inside the space of turing completeness with mathematical truth not just a matter of opinion okay and finally I've shown you in this talk some proof sketches that match the intuition that we had in Arma in our minds what else is in the paper there's a lot more in this paper it's written as a sort of theoretical paper pretty theoretical paper so you will it'll it's it's admittedly a little bit of hard going there's actually multiple notion of expression that says expressiveness and local expressiveness there's the proof of that theorem which is kind of non-trivial there's an interesting relationship to mathematical logic and it talks about some other frameworks for talking with other formalizations for expressiveness now as language designers there's a lot for us in here right disagreeing slash macro systems are in all of our languages these days right everybody seems to be adding them now they're really neat they can come with a variety of powers they can help us only add non expressive features they can also help us add expressive features and if they allow us to increase expressiveness that's the thing we might want to think about doing with care okay last thing I want to say is there is a real benefit to having expressive features right expressiveness in some sense what this talk is done I hope it's convinced you is to say expressive features a little little bad right because they break existing equivalences and that's something you should do very cautiously right but on the other hand they also have benefits they avoid these global transformations if you don't add the feature to the language the programmer has to do it by hand and that's called callback hell right in fact callback called ojs is a website okay having the expressive features gives us greater modularity you can have code that doesn't have to be transformed hasn't it doesn't have to have these patterns and if you don't have it people have to follow patterns they can misuse them they can get them wrong it's also harder to tell what they mean okay that's the end of the sermon part of the talk I'm going to leave you with two homeworks all right homework number one so anyone here know JavaScript okay let's see how well you know JavaScript so you know JavaScript has a feature called width okay is width expressive okay if you need a way to start if you want to work on this homework if you need a semantics for JavaScript we wrote down a very clean simple semantics that's tested against reality and this paper it gives us semantics for width by compilation but it doesn't do it through a purely local transformation question is is that possible or can you prove that it's impossible okay second homework problem anyone here program in Python okay good you're willing to admit it even though you know there's a homework coming you know generators in Python okay our generator is expressive now you would think in fact it's a very careful design in Python to do generators basically through local CPS okay it turns out that kind of breaks and if you want to know more about it we have a paper on semantics of Python and section 4.1 explains what's problematic about generators in Python they could have done it cleanly but because Python screws up scope everything in the language suffers from it flow suffers from it screwed up scope and we ran into this the hard way but the paper documents what we ran into so those are your two homework problems I will leave you with one last thing I asked Matias so Matias was might end up being my PhD advisor because of this paper and I asked him for slaw for a photograph from back in the era I showed you one here's the other one we can't date the conference exactly but it was around 1990 it may even have been Matias delivering this very talk i've although the paper for this talk at a conference i mean it's either that or it's a scene from like you know Fritz Lang's Metropolis one with the two but anyway that seems like an appropriate note on which to end and I would be happy to take your questions so the question is so question is this seems to be founded on theoretical concerns and based on infinite loops what if we wanted something that was maybe less than an infinite loop first of all I think I failed as a speaker because I think I tried numerous times to explain why as a compiler writer as a worker this is of concern to you so it's not purely theoretical concerns every compiler use has to worry about this okay but they'll set up about infinite loops is merely a theoretical artifact to make it very clean to separate these two okay there's nothing that prevents you from taking that intermediate definition of observational equivalence where I said all these two values equal using the equal sign right you might be perfectly happy to say well I have base values in my language numbers and strings and bullying's and stuff I know how to tell them apart right well five is not equal to six that's not surprising to me then you can just take that definition and you don't have to worry about the infinite loop part of the talk at all you can reconstruct all of this without any of the infinite loops does that answer your question very good thank you other questions yes ah I didn't add the question is warehouse hoping for this so you defined equivalents in terms of not I somebody defined equivalents in terms of halting but like doesn't that this halting we've heard this halting thing before right there's some problem associated with it I'm trying to run what it's called okay so yes I did not give you a algorithm for figuring out equivalences ah the proofs we're doing by hand now you could do them with my hand you can do them through so I can automated proof system or whatever but I'm not giving you an algorithm for determining these you're still going to have to do these proofs through some mechanism that requires human insight okay ah that means there might be things that are provable that we can't demonstrate in fact if you if you carefully read that theorem statement there were actually two parts to the theorem statement and the second part is not about that but a related thing there might be distinctions there are distinctions we can't tell there are non distinctions we can tell etc so so it it is it does mean that we don't get like sound and complete systems out of this that's absolutely true but that's not about the halting part it's really about equality we can't get sound in complete equality it's the halting is just an artifact with this mechanical setup yes then there great question so the question is basically we spend most of our time having debates about the human facing sides of it right syntactic aspects of it and this is a very austere if you wish but it's a it's mathematical so questions can one inform the other and I claim as somebody who also cares very much and does some research on human factors in programming languages I think we make we are we're remiss if we do one and the other right we end up splitting into two camps that the theory people who do theory and then the human factors people who do human factors and oftentimes these people have no idea what the other stuff is okay I think what we need is a balance between the two and it's easy to say but we need a balance where we can talk about what it means to make something more expressive for the human but do we realize that in the process of adding that we might have actually also made things unexpressive or unintuitive for them by destroying things that they might have expected that's the part of the debate we never have when we talk about human factors I can add this feature but in the process if I broke an existing equivalence that means somebody might look at and say no I always expected I could I mean who doesn't expect that you can replace one plus two with three right so you could say oh it's a convenience to give somebody overloading but did you also ask them are you perfectly okay and one plus two not being equal to three did you ask them have you ever accidentally taken an expression that looked like an arithmetic expression and rewritten it down down to its answer because you can't anymore you have to unexpanded so that's the way you link the formal with the human right because the formulas giving you a guide as to things that might have changed that you may not have wanted and you need to make sure that those are okay changes for your community of users hand back over their other hands any other hands you'd go ahead Oh last one sorry okay great question great question so questions about this undefined 'no so i basically said errors all go error programs and errors don't terminate right and in fact um matthias is a particularly good person to ask about that because if i can channel matthias for a moment he'll tell you that's a terrible idea okay because people make distinctions all the time based on erroneous behavior right in in fact any practical language will tell you there are multiple kinds of exception handlers not just you know stuff happened right and we make distinctions based on that we can make observations based on that right i can send in one kind of thing and get one sort of exception send another kind of thing get another kind of exception so really a more honest accurate account of gurmann language expressiveness would take that into account okay this is mostly this paper was written at a time when Mateus was starting to make that very explicit and his later research explicitly exploits that difference his work on s PCF but this work was in an older tradition where theoreticians found it convenient to simply say and this when when I can't evaluate I get to a non applet function in an application position we'll just hear the machine got stuck okay and there are stuck states but stop states are not terminating states they're not quite same as infinite loop states but they're not terminating states and now everything is non terminating it's not a satisfying definition from a programmers point of view okay and this paper sort of explicitly acknowledges that but then the later work that he did not on expressiveness peels it apart so you should be you are right to be unhappy about that I share your unhappiness and I can tell you so does the author okay on that ground thank all that well thank you [Applause]

Channel: PapersWeLove

Views: 15,238

Rating: 4.9521914 out of 5

Keywords: paperswelove, pwlconf

Id: 43XaZEn2aLc

Length: 59min 3sec (3543 seconds)

Published: Thu Sep 19 2019

Reddit Comments

[u/_tskj_]

Probably the most incredible talk at Strange Loop this year! As a pure functional programming ideologist I was absolutely blown away by his reasoning that functions having local state between invocations gives you power which is impossible to simulate without entire program rewrites. This is an incredibly interesting space to explore further. What other features are we missing out on?

[u/shevy-ruby]

why always videos ... :(

[u/[deleted]]

Offtopic, but I got to meet Shriram Krishnamurthi this past Saturday. He generously took the time to hear about a programming language that I'm working on, then responded to my thoughts with some wise advice about where I was making mistakes and how to design a successful language. In our conversation, Dr. Krishnamurthi really gave me a lot to think about. He is a very smart man, and I highly respect him for his work on Racket and Pyret.