Lambda Calculus - Fundamentals of Lambda Calculus & Functional Programming in JavaScript

okay welcome everybody very glad you could make it for this talk I've been working on this for a while I'm really excited about it if you don't know me I am Gabriel and I'm an instructor here at full-stack Academy of code my social media presence is G Lebec everywhere except unfortunately and someone ironically given the subject of this talk at Twitter where I was forced to use an underscore there's going to be resources available on my github at slash geela backslash lam to talk so you can go find additional stuff after this all right so let's just dive in and get started I want to start by pointing out a minute node repple here I can do kind of typical JavaScript e stuff but we're going to avoid JavaScript in the sort of classical sense as much as possible and start off with this function called eye or identity now just looking at the function if I invoke it with some value what am I going to get back here yeah identity of one is one identity of two is two what about the identity of identity yeah it's the identity function so very simply the identity Combinator is a function that takes in an input a and it returns an output a basically just reflects back a value so the identity of any X is X and we saw that in this particular paradigm we're allowed to use functions as arguments verbs are nouns and nouns are verbs so the identity of identity is itself in Haskell this is actually built into the prelude module which is there the base standard module for the language as the ID function as you can see it takes an argument v and gives you back v so looking at this I just flashed a bunch of stuff on the screen you might be thinking what's this lambda stuff that's sitting up here so lambda is a signifier it's a notation that we're going to use to indicate that we're starting the definition of a function so we can read this as we're starting to define a function which takes a single input or parameter and it returns some expression some body this whole thing is called a lambda abstraction in the lambda calculus but it basically just means it's a unary anonymous function unary meaning it takes a single input the lambda calculus is a really tiny symbol manipulation framework a calculus is just a way of moving around symbols on a page the subject that you may have learned in school called calculus is a specific calculus for things like differentials and integrals and stuff like that derivatives and so this calculus is about something else this calculus is about evaluating and defining functions so in the lambda calculus we have variables which are pretty boring please come in we've got expressions which are the application of some function to its argument we've got an expression that is itself a function definition an abstraction instead of a concrete thing like 1 plus 5 1 plus 6 1 plus 7 we have something like a plus you know 1 plus a and a can be anything that's become abstracted and we have groupings to disambiguate the order in which we should be doing certain operations this is the entire lambda calculus all right so it talks over I can go home now now we're going to see some examples of this so let's start with just a couple cross comparisons here variables in the lambda calculus as I mentioned are extremely boring one thing to note here is that these variables are immutable they cannot be changed after the fact there's no concept of assignment per se in the lambda calculus there is binding which we'll see shortly but if this variable is bound to a value that's its value for now and forevermore so now let all constant applications are slightly more interesting this is applying a function to its arguments and in the lambda calculus that's just juxtaposition it's just a space there's no parens for invocation which at first if you're used to something like JavaScript is a little disconcerting but in reality and ends up removing a lot of noise from our expressions and as this talk goes on you're probably going to see it's becoming easy easier to read the lambda calculus rather than trying to parse the JavaScript so here we apply a function f to its argument a we can apply multiple arguments but in the lambda calculus all functions are unary so this is really a curried function this is an f that takes an A and that returns a new function there which is not written down which takes a B let's try this out let's do kind of a classic example of a curried addition function will say that add takes an A and it takes a b and it returns a plus B so if we call add with just some single argument we get back some function if we call that function with an additional argument now we get the final result pretty familiar stuff I think for this crowd so f a B you can read this first it takes an A and then a B and if there were more arguments they get fed in one by one going from the leftmost argument onwards marching kind of tore the right we can make this clear with parentheses we can say first apply F to a and then apply the result of that to B but this isn't necessary because we say that function application is left associative so these are really useless parenthesis and we'll omit them and most of our examples finally we can use parentheses to force evaluations to occur in a different order so here this is actually a different expression this this means something else in the lambda calculus it means we're going to first apply a to B and the result of that will be the argument to F hi hello welcome so just to summarize for everybody who's just arrived we're starting to define the syntax of a very small language called the lambda calculus and this is just something that takes functions applications of functions two arguments and parentheses for grouping that's really it so really high-level review of just this last slide FA means invoke F with a and you'll get more as we go so let's talk about function definition in the lambda calculus as I said before we use a lambda to indicate that we're defining a new function so we got lambda cos on the Left JavaScript on the right this is a function that takes an A and it returns whatever B is sort of throws away a a B becomes irrelevant in this expression the function abstraction like this is greedy the body swallows up as much stuff to the right as it can and that's all included in the body of this lambda abstraction so up into the point where it would stop making sense like if you're using parens to force things to be evaluated differently so this indicates a function that takes an A and then invokes B with X as its argument we can disambiguate this with parentheses but as I said since lambda abstractions greedily swallow up everything to the right these are actually useless parentheses and will not really show them in most of the upcoming examples on the other hand if we use parentheses to force the thing on the left to be a function with a body that's just the B variable now this is a different expression now we're saying take a function that goes from A to B and apply it to the argument X as we saw a second ago in a demonstration in the lambda calculus were allowed to nest functions so this is a function that takes an A and returns a new function that new function takes a B and that function returns an A so just to reprise our curried addition function from a second ago we have this function that takes an a returns a function that takes an B and that returns a plus B so we have to feed out the arguments not like this all at once but rather each argument one at a time in a six successive invocations and we get the result we want known as currying we again we can clarify this using parentheses the lambda on the Left returns the inner lambda and then we can use that but since these are useless parentheses will limit them in most of the examples how are we doing so far questions about the bear syntax of the lambda calculus as you can see it's very similar to JavaScript except you don't have parentheses around function invocation you just put things next to each other and that indicates apply a function on the left to the argument on the right cool all right so I swear this is going to be the most complicated bit of lambda calculus syntax we have to deal with it's called beta reduction it's got a scary name but it really just means tracing the logic evaluating the function invocations seeing what we end up like so beta reduction is just the act of taking a function and applying it to its argument so here we've got this function in red applied to the argument underlined what we do is we take the argument and it comes in as the parameter of the function this is a function that takes an A and returns an A so this argument the BCD function is going to replace in the body of the function every a we go look in the body find all the a's and we substitute in this other expression and that gives us this first simplification well we continue doing this we've got a new function the BC B function being applied to another argument the X argument so we're going to take the X argument and substitute it in as the parameter to the function so we go look inside the function body find all the B's and replace them all with X's and we get this new function as a result once again we've got a function that we're going to apply to an argument we take the argument we pass it into the functions parameter we go look in the body for all the C's there are no C's in this body we replace all the C's with that argument and that gives us this simplification at this point we've got nothing left to do there are no more reducible expressions so we say this is in beta normal form which is just a hilarious way of saying we've fully evaluated the function in a terminal way so it looks a little dense compared to what you're used to with JavaScript but it's really nothing that we haven't done many times in JavaScript taking a function passing in arguments as the parameters and then in the body everywhere that parameter exists it's been replaced by a value there's some caveats here I'm not going to cover in this presentation if you could do multiple reductions in different places in the expression simultaneously there are caveats and strategies to which ones you should do first and there's also possible ways that two separate functions that coincidentally share the same variable names you want to avoid conflating those two variables which mean different things so there are some gotchas but they're kind of outside of the scope of this talk let's see another Combinator here the mockingbirds this is a fun function it takes a function as input and it invokes that function passing in itself this is the self application Combinator whoa what's happening here this is craziness let's try it out the mockingbirds is a function that takes a function calls the function on itself what might the mockingbirds of identity be somebody walked me through the logic here what's F in this function it's the identity what are we doing with it identity of identity we already solved that before right what is the answer it's the identity the self application of identity is identity we saw that earlier this one's going to be a little bit more disconcerting what is the self application of self application feel free to yell it out if you think you got it maybe a hinted at by the fact that I'm putting this in a try-catch block any takers call stack.size exceeded what just happened well Mockingbird idea of identity is identity of identity self application we already know that that is identity so that made sense that does reduce to a better normal form but the mockingbird of the Mockingbird is the self application of self application so we take self application and we apply it to itself but if we're gonna evaluate that that's the self application of self application so we take the self application and it just goes on forever this is a problem the problem is we don't always know if some lambda term is going to have a beta normal form we don't know if this process ends or not sometimes it doesn't end sometimes it diverges which means it goes on forever and in fact there's no way to know in a general way if a given expression there's no single algorithm that can tell you whether or not one of these expressions will stop that's known as the halting problem and Alan Turing figured it out now for is an individual one you can prove through ad hoc means that yeah for instance this one is going to go on forever so it's not that it's always unanswerable just that there's no one set of steps that you can take that will cause that that you will know whether or not a halts this particular divergent term by the way is called the Omega Combinator Omega because it's like the end Alpha and the Omega and sometimes the mockingbirds as a result is called little Omega they one of the problems you'll find if you start going out and reading about all this stuff is that a lot of different mathematicians and programmers and people have worked on it over time and they've all given their own pet names to these things so there's a lot of synonyms and sometimes even intersection okay we're almost done with lambda calculus syntax but I lied before and I said it was the end there's one more thing I want to show you about syntax here we can do as I said before these nested lambdas we could say there's a function that takes an A and that returns a function that takes a B which returns a function that takes a C which finally returns a B but the way we're using these functions we just kind of think of well we're going to call it with both arguments at once in quotes really meaning we feed it the first argument then the second argument but we think of it as taking two arguments just in a curried way so in order to kind of make it easier to write this stuff down and parse it there's a little bit of a shorthand where we just condense all the nested lambdas and say here's a ternary function here's a function that takes three inputs and returns something but don't get fooled these don't come in all simultaneously we feed them into the function one after the other so this still means nested lambda expressions it's just a convenient shorthand for indicating that they're curried I'm not going to go through all of the logic of this again if the exact same examples we saw before of feeding an argument into its parameter and replacing the parameter in the body feeding an argument into its parameter and replacing the parameter in the body but this time I've used the syntax shorthand to show those nested lambdas so the body of this one is another lambda and then we proceed as normal in the rest of this is exactly identical to what we saw before so just a shorthand don't get too tripped up over it but it's going to be convenient for us to be able to think conceptually of functions that take multiple arguments even though we know we'll just keep that as a footnote that they're all curried functions are you ready for the next Combinator let's talk about the Kestrel the Kestrel takes an A and a B and it returns a let's try that out takes an A takes a b returns a what is the Kestrel of the identity in the mockingbird yeah what about the Kestrel of the Kestrel in Mockingbird right it doesn't matter what the second thing is it's it's irrelevant the Kestrel just takes two things and returns the first one so we just saw that here in Haskell this is built into the base language as the Const function why is it called Const in Haskell let's try something interesting here I'm gonna say k5 is the function you get when you call K with only one of its arguments so normally the Kestrel takes two arguments and gives you back the first one but I'm only gonna give it one of its arguments well that's interesting but these are curried functions so I can give it another argument it gives me back the first thing I can also give it back some other argument it gives me back the first thing this is a function that's fixated on a particular value it's the constant five function no matter how I invoke this function it always gives me back five that's why it's called constant Haskell but it's the K Combinator here's a fun one I really like this one the Kestrel of identity and some X is a dial a makes sense this is an algebraic equality the thing on the left is the thing on the right and vice versa well the thing on the right is a function and I know in the lambda calculus I'm allowed to apply functions to values so I apply this to Y what do I get why that makes sense on the left side equals the middle side equals the right side that means I can ignore the thing in the middle and the thing on the Left equals the thing on the right does anybody see where I'm going with this I've got K I of x and y returns y kay I have a first argument and a second argument returns the second argument I just derived the kite the kite Combinator takes two arguments one and two and it gives you back the second one now I could have done this manually I could have said the kite is a function that takes an A and it takes a B and it returns B and then I would call the kite on something like four and A nine and it gives me back nine but it's cool to see that from these atomic Combinator's combined together I get these new molecules which are other Combinator's so some of my combinators can mix and match and start producing other functions that are useful and interesting in different ways so ki of em and ki is yes so kite of the Mockingbird in the Kestrel is the Kessel flip them around you get the other one so far so good at this point probably some of you are wondering what's with all the bird names got Mockingbird Kestrel kite etc alright so we're gonna take a little mental break for a moment and talk about history Moses Ilyushin Finkel and I can't pronounce German so please forgive me name these things long German names like Zeus omit set some function Haskell be curry who came a little bit later used some of the same letters but also some of his own letters just to add to the confusion and in the 1980's logician and puzzle author named Raymond Smolyan wrote this absolutely wonderful book to mock a mockingbird the whole back third two-thirds of which is about combinatory logic and Smolyan took Curry's combinator names and turn them into birds and the reason is because the book doesn't lay a lot of emphasis on the math from a formal perspective instead it uses this metaphor of birds in a forest who hear the songs of other birds and sing back the names of other birds so birds creating birds and singing birds and all this kind of stuff now unfortunately somalian called the identity Combinator of the idiot bird I wish that he had used the Ibis I used the Ibis in my first slide but will will forgive him because the rest of the book is just so wonderful now he didn't do this totally for no reason he actually did it to honor curry because curry was himself an avid bird watcher and at this point some of you are thinking Haskell curry who's this guy why do we care about him not shun Finkle or vice versa so the next slide is the the anti diversity slide this is just the historical nature of mathematics in the 20s and 30s it was filled with a lot of white men so we'll acknowledge that and move on but I'm going to give you a really fast crash course in the formalization of mathematical logic around the late 19th century early 20th century people were realizing that math which had seemed on the face of it so cut and dried and straightforward was hiding some really nasty paradoxes and so people were trying to unify mathematics and figure out the sufficient axioms that would define all of mathematics in one big tome so what was like the real true system of math lesson so I'm gonna race through this I could do an entire presentation that would be two hours on just this I'm gonna try and keep it to less than five minutes in 89 Giuseppe Piano invents his own formal notation for function abstraction he also defines arithmetic as the sequence of natural numbers starting from zero and then the successor of zero and then the successor of successor of zero and the successor of successor of successor of zero and so on and so forth these are piano numbers the logician Gottlob Frege develops his own function notation which uses this really unique graph format it's actually really cool to see impossible to read but a good idea a good idea which has better versions that come later and most famously he basically invents quantified axiomatic logic so this is the kind of sentence like for all X in the reals there exists a Y in the reals such that Y is greater than X for all and there exists that's the quantification and quantified axiomatic logic by the way Frigga even in 1891 was using curried functions in the 1910s Bertrand Russell along with whitehead very famously published principia mathematica an attempt at formalizing all math but he also discovered earlier than that actually Russell's paradox the thing of the set of all sets that do not contain themselves well as that set in itself or not it's a paradox it's impossible to figure out so that we made a lot of people really disconcerted and they realized that math wasn't quite so perfect in its foundations as first thought tion Finkle we talked about he was an early pioneer in combinatorial logic he also used currying and published one paper and then it was really sad actually the rest of his life really spiraled downhill he ended up in a mental asylum which don't worry it's not because of combinatorial logic I don't think von Neumann famous mathematician also later in life helped build the first real electric computers he also kind of did something that if you reinterpret it it's combinatory logic but that was almost by accident like that wasn't his goal in life and then in 26 Haskell curry starts reinventing combinatory logic he wasn't aware of tion Finkle or Fraga well he was aware of Franco but not any kind of link to combinatorics and so he does a whole bunch of contributions he's a really smart guy at Princeton and in 1927 he discovers that Shawn Finkel beat him to the punch so he forges on nonetheless which is good for us because he delit velop smen ii many new theorems in 1931 court gudo very famous mathematician who kind of plunged a dagger into the very heart of math discovers that this race and search for the perfect set of foundations for math is fundamentally flawed it's a fool there and it's impossible it's literally impossible because every complicated enough system to be interesting by a certain definition of interesting such as piano numbers is either inconsistent or incomplete that means there's either logical inconsistencies which make it make no sense or there are systems and things inside that language which you can talk about but you can't prove or disprove there's no way to get to the proof or disproof that totally up ends math as we know it in the 30s Alonzo Church is trying to figure out a system that's at least good enough to compute things that are computable in some definition of computable and he develops this thing that we've been talking about the whole time lambda calculus this notation system for writing down functions now it's this tiny tiny language and at first his grad students such as Stephen Kleene II and Rosser they think that it's not gonna really lead to much like it's just a notation system but then they start to realize like it's ballooning outwards and it's from this very tiny bit of logic is coming all sorts of interesting results they also prove four different versions of it are consistent or inconsistent Stephen claiming by the way goes on later in life to invent this thing that we use all the time called regular expressions so that's fun in 1936 Alonzo Church solves a famous unsolved problem David Hilbert's decision problem this is an algorithm problem that says like well actually I can't remember the specifics but it's let me see oh is there a way to figure out if any given problem does have a solution very closely related to but distinct from the halting problem and church is like no there isn't but he uses the lambda calculus to solve it which was hilarious because it started out as three or four lines of notation and it turned into a system complicated enough to solve this famous unselfie it's what also happens in 1936 two months later Alan Turing solves the problem using something called a Turing machine and he publishes his own paper and then he finds out that Church beat him to the punch by two months and it gets really annoyed by that he was actually quite disappointed to find out that someone else had raced him and beat him to solving the decision problem but he looks at paper he looks at church's lambda calculus as you know what these are actually identical my Turing machines and church's lambda calculus are the exact same thing just expressed different ways so then he decides you know what I'll bury the hatchet come to Princeton get a PhD under church with churches as advisor and in 1937 he publishes the first fixed point Combinator okay that's the history in the tiniest nutshell I could manage or at least bear to part with so Combinator Combinator you keep using that word I don't think it means what you think it means what is a Combinator we've said this many times combinatory logic and combinators lambda calculus where's the dividing line in reality they're almost entirely the same thing a Combinator is a function with no free variables a free variable is a variable in a function body that's not bound to some parameter so this is a Combinator because the B in the body is bound to the B parameter whereas that's not a Combinator because a comes from nowhere what is a who knows we could make it up it doesn't matter that's a Combinator it doesn't matter that we're not using the B the B's are relevant it's a parameter not a Combinator because where does the B come from don't know and even more complicated stuff like this don't get distracted by the e that's a parameter it's not a variable so everything that appears in the body C and B those are bound to parameters that's a Combinator you now know what a Combinator is we've seen a bunch of Combinator's identity self-application first or const second and the cool thing is as I mentioned before using some of the primitive Combinator's mixed together we start generating some of the more complicated combinators or at least other combinators which is surprising but cool are you ready for the next one let's look at the cardinal let's just look at it for a second not the beautiful photo which I stole from somewhere I can't remember where but the culminated self anybody looking at this can you think conceptually what this actually does in a sort of a use-case way I'm really pushing you here because we're talking about abstract math and I'm dumping you in a land with no JavaScript exactly it just flips around arguments it takes a function f that takes two parameters and then it calls the function f with both of those parameters but in the opposite order so here's the C Combinator and what if we apply this to a function in two arguments such as the kestrel and these other two things that we don't care what they are but there I am in this case the cardinal of the Kestrel and the idiot and the Mockingbird well walking through it it takes three things the function and two arguments and it calls the function which is the function here okay and it calls them with two arguments which are the arguments and it calls them in the opposite order so it's K of M and I which is yeah so we start with the Kestrel and then we put two things into it but backwards that's interesting because look at what we have here the cardinal of the Kestrel takes two things and returns the second does that sound familiar what is the kite the Cardinal of the Kestrel is the Kestrel of identity is the kite is this other thing they're all the same and we can just do this to prove it let's do the cardinal takes function this monitor why don't we never go okay takes a function takes an argument another argument calls the argument with the arguments backwards whoops let's get the Cardinal of the Kestrel apply it to two variables the Kestrel normally gives you back the first thing but the Cardinal of the Kestrel gives you the second thing it works this isn't pure math it's also applicable so that's kind of fun Cardinal if you've got a cardinal you can't apply it in different ways you can flip the kite around to pick out the Kestrel if the Kestrel to get the kite and in fact in Haskell this is built into the base language and it's called flip and it actually ends up being useful from time to time so why why are we learning this what's what's actually going on here is why how is this useful do we care remember lambda caucus and Turing machines are equivalent they both anything one can calculate the other can calculate but Turing machines are exciting because they're these hypothetical devices that use state you know information that exists over here here here and things that change over time to do computations and from these hypothetical devices people said wait a second we can build real machines that do this and they use memory and state and they do a little bit more complicated stuff just to make it more performant and easier to work with but at their heart they're really Turing machines so they work with Machine Co which means let's flip a whole bunch of physical switches and then see what electricity and bits come out the other end and we abstract that away in a language a text format called assembly language that says things like move the data in register B to the accumulator register add 1 to whatever value is in the accumulator register of my memory very stateful very machine based very hard for humans to reason about it's not conceptual it's all about machines well we build higher-level languages like C compiled into assembly but those higher-level languages are still machine centric they still say things like hey C go allocate seven bits of memory over here and give me back a reference to the pointer of that memory address and so on and so forth so then somebody says this is stupid will make the program in languages do that for us I will just focus some more on concepts like hey give me a VAR X and I don't care how you figure out the memory for that just go do it yourself and then somebody says why are we even bothering with memory why don't we just have these pure functions that operate on each other and wait a second this whole time this machine marched through abstraction has been leading us to something that existed before Turing machines existed which is the lambda calculus functional programming languages are based on slash their backbone is the lambda calculus so if we decide wait we're not going to organically evolve towards this kind of conceptual abstraction but let's just start straight from the lambda calculus and go the other direction we can start designing purely functional languages and using all the decades of mathematical research that have gone into Elsi to design our language and see what comes out of that and see if there's anything useful that we could do there and then we'll take that pure functional language just compile it down to machine code so it runs on our physical turning machines lambda calculus and Turing machines are equivalent therefore here's the big theme of the entire talk coming on the next slide everything can be functions when I say everything I mean everything like boo Liam's whoa here's a JavaScript boolean expression not X is equal to that's the double equals not the assignment equals Y or the result of the expression a and Z how are we going to do this in lambda calculus well it's a problem because we don't have negation and we don't have ORS and and operators I mean we don't even have a quality checks in the lambda calculus right that wasn't in the language we don't have billions we do with parentheses let's instead let's that's what we got we got parens alright so how on earth are we gonna do this let's tell with the primitive building blocks the boolean s-- a bool what is that used for in JavaScript hmm well what about selection some result is check a boolean condition if it's true we'll get the first expression if it's false we'll get the second expression let's start translating this over to lambda calculus well we got this turnery except oops this question mark in colon that's not on the lambda calculus syntax it's got to go bye-bye what are we left with this is a function application right so bool must be what's the theme of the talk function and oh well what do we need here we need a function that if it's the quote unquote true function it selects the first expression and if it's the false function it selects the second expression wait a second this sounds really familiar to me where have we seen a pair of functions that select either the first or second things yeah we already have Williams we need to have to reinvent them they're already in the language that we've developed so far in this talk we'll just encode in other words represent Williams as functions will say that the kestrel function the constant function the first function is true quote unquote and the kite is false that's kind of neat let's do that while we're looking at this slide and admiring it true is equal to the kestrel and false is equal to the kite now there's a little node trick that I'll use here because if I go console.log out true it tells me it's the kestrel which is true but in both senses but it's also slightly annoying like if I'm going to start doing billions so I'm going to do a little trick here I'm gonna say T dot inspect is a function that returns the string true slash Kestrel and false dot inspect is a function that returns false or the kite now if I like out T I get T / K and if I log out false I get false / kite so that will be useful going forward in some of these demos that wasn't lambda calculus the other stuff was but not the dot inspector okay so we have true and false but true and false on their own are kind of boring right yeah so we can select between two things what about boolean logic what about negation let's translate it well what doesn't belong one of these things is not like the others the negation that's that the error the exclamation mark isn't in the lambda calculus syntax what does it got to be instead what's the theme of the talk a function the not function the not function will take in a boolean and it will select between two other boolean x' if we give it not true it selects false if we give it false it selects true how can we implement the not function well wait a second we just talked about selecting between two things what kind of things selects between two possibilities where you have various a function that's true but specifically these boolean x' that were using the kite and the kestrel are themselves functions that choose between two possibilities look over they have here this expression an unknown boolean P it might be the kite it might be the Kestrel I don't know which one if it's the Kestrel or true which one of those does it select the first one false and if I my unknown boolean is the kite which does it select the second one true my unknown boolean selects its own opposite in this expression so we'll turn this into a function and we'll call it not that's it not just takes a boolean and then tells the boolean select your opposite I promise it works so not takes let's see it takes a boolean and then it calls the boolean passing in false and true so if we say not true that's false and not false is true I have not put a single JavaScript boolean into any of this I'm doing negation this is like this should be exciting all right so our church encodings which is what these things are called from boolean z' now includes the negation we saw how we got true and false but there's a more exciting way of doing this there's an even better way in my opinion a cooler way not true is false and not false is true but we said true and false were encoding those as the Kestrel and the kite but if the Kestrel and the kite there's no named functions in lambda calculus this is just us writing down a shorthand so that we don't have to remember and read out all the lambdas but if we did replace them with their equivalent lambda expressions that's what we're really looking at now we're saying the not function will take at the top there a lambda that takes two arguments and gives you back the first and it gives you back a lambda that takes two arguments and gives you back the second okay and on the bottom we're saying it takes you know two arguments and gives you back the second and the not function will give you back a lindo that takes two arguments it gives you back the first interesting so does anyone see instead of not is there a function that we've already seen that will result in this a function that it accepts a binary function a function that takes two arguments and it moves the arguments around it's the Cardinal yeah the only other one we see the Cardinal already does this behavior the Cardinal is bully and not the flip of true is false and the flip of false is true this minor is really gonna bug me there we go stay there don't move let's try it Cardinal of true now unfortunately look old weak I'm about to get here this isn't quite what I want just as function well that's weird what if I use this function I'll apply it to two things one and two I get back the second thing which is what I want the flip of true is false so I should get the second thing and the flip of false is true so I should get back the first thing which I do the problem is the problem is and it's not really a problem the problem is that the Cardinal generates a new function unlike my previous implementation of naught which selects between existing false and true functions the Cardinal generates a new function that behaves identically to the kestrel or kite this kind of identity crisis is known as intentional equality versus extensional equality extensional equality which is the kind of equality I'll use throughout this talk means the functions are the same if for every input they generate the same output so the Cardinal of the kestrel is extensional e equal to the cut they both behave identically there's no way to tell them apart from the outside corner quote intentional equality is more like well where did it come from and what's inside it what are its guts I'm not gonna focus on that during this talk but it works that's the important thing let's design and together boolean and boolean conjunction we know it's a function right that's the theme of the talk how many arguments does it tick what are these arguments what kind of thing are they they're boolean so that our role of a kite or kite and Kestrel or Kestrel Orchestra or tied in kite just to finish it out well if you're gonna use to take in a parameter you're probably gonna use that parameter somewhere in the body of your function right so even if we're not quite sure where to go with this let's try just using one of these boolean z-- P is a boolean so what does it do what are these boolean functions do when I use them yeah they select between two possibilities such as the Spanish question mark what if our first argument to end is false which of the two possibilities will P select the second one but wait a second if one of the arguments thar and is false what should that result of this entire function bei yeah so I'll just put false there if P is false short-circuit don't bother looking at Q there's no point we can know we just select the second thing and it's already going to be false so we don't even bother checking Q well what if P is true it's going to select the first thing right but what is that first thing what should it be yeah it's gotta be Q because if P is true the end is true only when Q is true and the end is false if Q is false so once P is true we have to go look at Q and use Q as our result there's one more small simplification we can actually make to this that's kind of nice I like it at any rate which is we said that by the way P is a boolean size selects between two possibilities if P is false it should select false but I have hard-coded in a false there was a way I could do this even more directly or indirectly it depends on your perspective if P is false and it should select false P can just select itself right if P is false then return P which is false so I end up with this thing which is very much a Combinator P Q P Q P that is my hand function I forget where we're at in our dumb demonstrations of JavaScript do we have not we do have not okay what about and no we don't okay let's do that and takes a boolean and another boolean and it applies P to Q to P P Q P Q P that makes sense okay so and of false and true is false and of true and true is true true and false is false and false and false is false all the things we love and expect from the and function that's neat let's do or what is or hey someone's got the theme down I cheated ahead I jumped ahead and gave you two of the arguments oh no what are we gonna do P is a boolean it's Lex between two things all right here's where it differs from and what if P is true oops I jumped ahead too much P is true it selects the first thing which is gotta be true right if P is true we don't have to bother looking at Q because in or if one of them is true then we just result in true if P is false what's the second argument gotta be careful it's just the opposite of the thing before so that's we can also simplify I kind of glossed over that but it doesn't have to be a hard-coded true it can just be P because we reuse it if P is true just return P that fact is actually really fun because there's another little thing we can do here that's a trick somebody tell me if I apply this P Q double P Q function to x and y as arguments what is the resulting better reduction in other words what is the evaluation of this function what do I get as a result remember X replaces every P in the body and Y replaces every Q in the body yep X X Y but there's another function we've already seen that does this I'll give you a hint what if we ignore the Y's for a second yeah it's the mockingbird it's the self-application bird the self-application of X is double X it's the self-application of X but if the thing on the left is equal to the thing on the right and they're both functions I could apply them to some Y and now we see wait a second the thing on the top and the thing on the bottom are actually the same the Mockingbird works just like this other function it looks almost exactly like that except the other function is this additional hue on the end which is useless it takes a cue and implies a cure this is known as the Mockingbird once removed so it that's what the star means it's been like it's been given an extra argument the Mockingbird once removed is extensional equal to the Mockingbird it behaves identically to it so have we defined or know we have them let's do that really quickly or takes a P and a Q and it does P of P whoops and Q we can demonstrate that or TF is true or FF is false or F T is true and of course or TT is true but we can also use the Mockingbird for that because we just proved that the Mockingbird oppler it's the same way here so Mockingbird of true and false is true false and false is false false and true is an or statement as well and that's also an or statement Wow Mockingbird you're multi-talented anybody have an idea what this might be well it's definitely a function that takes two arguments and I'm gonna tell you P and Q are boolean's just to make it slightly easier but if P and Q of Millions what does P do what it selects between two possibilities and if Q is a boolean what does it do selects between two possibilities does this make it easier to see what this function does sorry you were sure okay well if P and Q are the same boolean they select true if they're the same that way they also select true but if they're different they select false which function is this sorry oh is or something like that not quite it may be I'd have to think about it it might be Zoe yeah I'd have to think about it yeah let's cheer it that's it's cool yeah nice nice work I didn't think about that there's a simpler thing that we use this with if P and Q are the same we get true if they're different we get false that's called equality this tests if P and Q are the same boolean well there's a nice little simplification we can make here Q is a boolean true or false if it's true it selects true if it's false that selects false that's redundant we could just use Q as it is it's already true or false and at the bottom if Q is true it selects false and if it's false it selects true we already have a function that does that it's called the not function so we can simplify this to P Q not Q and that is our boolean equality function I'll do that as long as that's P to Q to P Q not Q okay so boolean equality takes a P and a Q and it does P of Q and not Q try it out boolean equality of true and true is of course true true and false nope false and false yes false and true nope nice it's always fun to see it actually work like you you kind of believe it and then you see it you know like oh I guess it really is true all right we got Church encodings from boolean's um I'm not going to do this one out but if you are familiar with billion logic you have heard of de Morgan's laws de Morgan's laws are a pair of laws this is only one of them but it says that not P and Q is equal to not P or not Q and we've just expressed that using nothing but functions no boolean x' no ands no ORS I could prove that we'll just take our our shorthand and replace it with the actual lambda calculus so there's our boolean equality of not and P Q or not P or not Q all right it's pretty cool now I rehearse this talk last night my fiancee made me she said this talk is way longer than an hour I was like oh we'll see how long it is no no you're gonna rehearse and I rehearsed and it's way longer than an hour but this is a really good stopping point so what I'm going to do is I'm going to give you the conclusion of this talk which works perfectly after this slide it fits it makes sense and anyone who would like to is welcome to stay another 30 ish minutes I'm gonna go into another room because mark has to come in here and get this room ready for demo day and I'll show them numbers in the lambda calculus but before we do that I'm going to conclude this talk so let me skip way down to the bottom of my deck here if I can find my mouse there it is no further no more than that keep going try remember where this slide starts almost there okay so a small preview this isn't even the only table in this talk these are just the combinators let alone the boolean equality the arithmetic the numerals and the arithmetic operations that yield volumes so lots of stuff that I'm cutting out in the interest of time but yeah I know here's where I want to conclude and I want to give you a couple little small addendums the first is I emphasized early on that from primitive Combinator's come other Combinator's and this is a really cool sort of atom to molecule sort of situation and it begs the question how many Combinator's do we need and which ones to generate all the other ones is it even possible to do that doing an infinite number of them twenty ten five just to not even identity identity isn't on the board these are the only two you need you can make identity out of this the Starling in the Kestrel the Starling is a weird one I actually don't really like the SK Combinator calculus which is what it is called I really like the B ckim Combinator calculus if I just added m to this this would actually suffice five of them and that was the one that Curie used I find this far easier to use than the SK Combinator calculus for instance the identity in the SK Combinator calculus is s of K K it's also s KS those are extensional equal you didn't get a chance to see the Vario but the Vario is the world's smallest data structure that's right I'm putting data structures in lambda calculus here it is in the SK Combinator calculus and this is like not even close to how complicated it can get so really why right what it was what what all right to begin with in my opinion I I was searching for this they answer to this why question I was trying to think like am i trying to evangelize like they're learning abstract math of this and that then I realize no it the honest answer for myself is it's just fun like I enjoy this I hope that you might enjoy it too that's the entire basis of the book to mock a mockingbird it's a book of logic puzzles and games it was written to act as a series of fun challenges it's a great mental workout thinking along these patterns like let's you think about like oh my gosh I have to think of where nouns are verbs and verbs or nouns and I've got to be able to think about partially applied functions curried functions higher-order functions there's a lot of spaghetti so it's it's really laying down the neurological groundwork for understanding functional programming in general the lambda calculus as I said before being the basis of languages like Miranda and Lisp and Haskell means that those languages if you know this kind of combinatorial logic it sets you up for success in those kinds of languages because even though you're not required to think entirely that way there's a large portion of those languages that assumes you are comfortable with that and from that we get all sorts of real-world practical benefits so I started writing them down a lot of them are intersections with just functional programming in general but many of these comes directly from the lambda calculus closures higher-order functions laziness infinite data structures garbage collection function graph reduction type theory provable programming code parallel processing for free parametric polymorphism I mean it just keeps going on and on and on and this all derives straight out of purely mathematical fields that existed even before computers did but at the end of the day I really just think that there's a lot of elegant mathematical beauty to it and it's kind of art for art's sake I hope that this has inspired you to become interested in this topic and maybe to go read some more about it find a little bit of slides here all the Combinator's here all the boolean z' the numerals church arithmetic boolean ops on the church earth to tick data structures all of this is in the deck it's not an hour-long taco is it and you've probably all been wondering wait a second where's the most famous Combinator of all the Y Combinator well there's the Y Combinator what does it do I'll just leave you with this as a brain teaser the lambda calculus has neither loops nor recursion so how does it do either of those things because it can calculate anything calculable this is the answer the Y Combinator allows for recursion in a language that doesn't have recursion built into it unfortunately I cannot demonstrate this in JavaScript because it goes on forever this is a fixed point commenter infinitely just keeps evaluating itself which works in a lazy language like Haskell or the lambda calculus itself so unfortunately because javascript is like the thing on the right and not like the thing on the left we need a slight variation on the Y Combinator called the z Combinator which is the exact same as the Y Combinator except the middle of it has a funk which defers calculation until required so the Z Combinator I could demo if I wanted to but I haven't set that up with my card so I warned today all right that is the talk thank you very much any questions

Channel: Fullstack Academy

Views: 119,296

Rating: 4.9581952 out of 5

Keywords: lambda, combinator, mathematics, functional, programming, languages, computer science, higher order, currying, partial application, haskell, javascript, fullstack, alonzo church, haskell curry, alan turing, Lambda Calculus

Id: 3VQ382QG-y4

Length: 62min 15sec (3735 seconds)

Published: Fri Aug 25 2017

Reddit Comments

[u/Dabbijo]

That was quite wonderful. Thanks for bringing this to my attention.

Part 2 for those interested: https://www.youtube.com/watch?v=pAnLQ9jwN-E&

[u/game-of-throwaways]

Thanks for posting this. The speaker is really exceptional, very well-prepared and clearly passionate about the subject. It's a shame that there were only like 5 people in the audience.

[u/Varelze]

This may be a stupid question, but the slide that he uses to talk about compiling a pure functional language directly into assembly rather than on top of imperative abstractions - has this been done? I tried googling and read a few things about languages bootstrapping themselves but it was vague. I imagine this would allow functional languages to be faster. Also, could a cpu manufacturer implement a functional assembly? Would this be even more beneficial?

Also, would a pure functional compiler vs a C compiler produce faster code? All I've found on the subject suggests that C compilers are fast because we have invested the past 50+ years into optimization techniques.

[u/fagnerbrack]

Yes, it’s aimed for JS programmers, but the speaker managed to build a good structure there which you might find useful.

[u/saint_glo]

Another talk that helped me connect programming to logic is "Propositions as types" by Philip Wadler.

[u/marcusklaas]

Top notch introduction to LC. Great fun too.

[u/Tarmen]

Lambda calculus is kind of weird among esoteric programming languages. It is quite good at abstracting because, well, it mostly is lambda abstraction. But that also makes it possible to write somewhat complex programs in a reasonable time.
My favorite example of this is this talk because it masters show don't tell.

Pretty unimportant but kinda weird: Technically you could use a single combinator, the iota combinator. It is defined as ℩ = f => f S K and you can recover S and K as

K = ℩(℩(℩℩))
S = ℩(℩(℩(℩℩)))

Finally, lambda calculus does have real world uses! System F is basically simply typed lambda calculus + polymorphism and is used (with minor variations) as internal language of GHC, the de facto standard haskell compiler.

[u/robotnewyork]

What's with the weird throat-clearing in the first second? Who edited this video and decided to start there?