The Simply Typed Lambda Calculus Explained | Introduction & Basics

[00:00:00]hello and welcome back to the lambda cube unboxed in this video we're going to introduce types into the lambda calculus the result of this is what's known as the simply type number calculus which is denoted by a lambda with a simple arrow before we start with the definition of that let's quickly recall the conclusion at the end of the first chapter types are desirable when it comes to functions functions that don't expect a specific type of object and don't tell us what objects they will return often too general although addition might make sense for numbers and strings alike it's not clear what the factorial or square root of a string is supposed to be this is the case for almost all mathematical functions which are mappings from a specific domain to a codomain usually this codomain the set of elements a function maps to is very dependent on the domain and the behavior of the function even more so if we talk about programming where it's important that we get an element with specific properties as an input so we want to be able to restrict the input of a function and also be able to specify what kind of objects the function is going to return in order to do so we introduce simple types each term of the lambda calculus will get a type which contains the information on its required input type and what type the output will have we begin once again with a rather informal motivation before we look at the formal definition consider the function f of x equals x squared plus one we can translate this function into the lambda calculus and write lambda x dot add applied to multiply x x which is the x squared applied to one now this function should take natural numbers and map them to natural numbers we denote this by putting a colon behind the term and we write down natural numbers to natural numbers and to say that the input should actually be of type n we write lambda x of type n instead of just lambda x so variables can have types and terms can have types too for the lambda calculus the set of simple types is constructed as follows as with lambda terms we have a finite set of variables v and each type variable is a type by itself a variable type we can also combine two types with an arrow to get an arrow type these types are called simple since we can only do one thing attach another type we can have a single type variable as a type or create a long chain of arrow types nothing else we're going to use small greek letters like alpha beta gamma and variance of these for type variables and sigma tau and rho for any types so sigma tau and rho can stand for a variable type but also any kind of arrow type again we're going to denote syntactical identity by the equivalence sign and we can leave out the outermost parentheses arrow types just like abstractions and lambda terms are right associative so we can also leave out the corresponding parentheses with these types at hand we can now define the set of simply typed lambda terms the definition should look quite familiar to you as it only really differs in one detail from the definition of untyped nounder terms whenever we construct an abstraction we need not only the variable which we want to abstract but also a type for this variable an abstraction now has the form lambda x of type sigma dot m translating the identity function from the untyped into the simply type lambda calculus is quite simple we need to choose a type for the input variable let's say alpha and then we would write the terms as follows lambda x of type alpha.x this term has something of type alpha as an input and it outputs it again so it returns something of type alpha the type of the term is therefore alpha to alpha if we now apply something of type alpha maybe a variable y we get the term lambda x of type alpha dot x apply to y this term would then have the type of the outcome so it's of type alpha but what if we don't apply a term of type alpha but any other type to this identity function this would actually be valid by the current definition of terms there's no restrictions of any sort in the application or abstraction rule additionally by our definition we could also construct a term where we take a variable x of type alpha and a variable y of type beta and we apply them to one another so lambda x of type alpha lambda y of type beta dot x applied to y what type would this lambda term have there's actually quite a lot of constructions that are allowed by definition but contradict intuition and the rules that we define later this is why the definition that we stated actually doesn't define the set of simply type lambda terms but rather only the set of pre-typed lambda terms so a set that has the simply type lambda terms as a proper subset but also contains some terms that look like simply type lambda terms but aren't actually typable like that properly typeable lambda terms will be called legal terms we're going to come to that definition very soon and we're going to introduce rules to check whether a pre-type term is legal before we do that let's take a look at our last example lambda x of type alpha dot y applied to x here we have a free variable whose type is unknown this term takes an element of type alpha and then we don't really know what the type of y applied to x is as we don't know the type of y we can guess and just give the result of y applied to x any type sigma so the whole term would have the type alpha to sigma so we've decided y applied to x as type sigma and we know x has type alpha since y applied to x is an abstraction and xs of type alpha y would need to be an abstraction with an input of time alpha returning something of type sigma so y would need to be an abstraction of type alpha to sigma these conclusions that we just came to can be done for any pre-type term to validate or check that the types fit and what type the free variables need to have this process is called derivation and might be familiar to you from courses like logic or any kind of mathematical theory derivation also called deduction is the process of forming new information from already gained knowledge for this transformation rules are applied to premises to get to further conclusions so we start with one or more propositions that are assumed to be true or are true by definition called axioms and by continuously applying inference rules we can prove other propositions a transformation or inference rule is written like so we have a finite number of premises p1 p2 up to pn that we write next to each other we draw a long line and underneath that the conclusion such a rule is to be read top down and it says if the propositions on top are true we can conclude the proposition at the bottom an example of quite a common inference rule that we use in our daily life is called the modus ponens of propositional logic it has two premises one is the implication if a then b and the other is just a the conclusion is b modus opponent says if a holds and from a follows b then the conclusion is b holds as mentioned a derivation is a sequence of applying inference rules starting from some axioms but normally we don't start with ground truths but with a conclusion and we want to find the derivation that proves this proposition so we don't want to start from the top but rather from the bottom so we write whatever we want to prove at the bottom and then we go backwards hopefully reaching axioms at the top to be able to formulate premises propositions and conclusions we need to introduce a few definitions whenever we want to state that the term m has type sigma we can do so in a statement where we put the term which is called a subject before a colon and the type behind it if the term is if the term is only a variable such a statement is called a declaration a context gamma is a set of declarations for pairwise different variables so we take a set of variables give each of them a type and then we put them together with such a context we're going to set the types of free variables this context will represent what we assume to be true in our system so we could for example say that natural numbers will all have the same type with these constructs we can form a judgment which will be the way to formulate propositions premises and conclusions a judgment reads as gamma yields m of type sigma and it tells us if we have the context gamma and three variables typed accordingly then m has the type sigma now if a term m can be found in a judgment so if there's a context gamma and a type sigma so that m has type sigma under context gamma we call such a term legal remember that up until now we only define pre-type terms the set of simply type lambda terms are exactly the legal pre-type terms the set of the simply type number terms are exactly the legal pre-type terms we'll also call these typeable in our examples from before we already constructed a few judgments we stated that the identity function over an input of type alpha has type alpha to alpha and since we don't have any free variables the context is empty this is a legal term the other two examples were not quite so simple first we applied the term y to the identity function and we required it to be of type alpha so y of type alpha has to be in the context for this to work in the last example we concluded that if we have the term lambda x of type alpha dot y applied to x it could have the type alpha to sigma and this only holds if y is of type alpha to sigma again we have to assume a type for y and we need to put it into the context if we chose the context to be empty this judgment wouldn't be derivable so in conclusion whenever we want to state that a term has a certain type in a certain setting we will form a judgment the inference rules that are allowed are given by the deduction system in the simply type lambda calculus we have only three derivation rules one for each step of the inductive term definition the variable rule says if we have a declaration in the context gamma like term variable x has type sigma then gamma yields x has type sigma to put it simply if x has type sigma then x has type sigma these are going to be our axioms the second rule called application rule has two premises if gamma yields that m is of type sigma to tau so m is an abstraction of some sort and gamma also yields that n is of type sigma then gamma yields that m applied to n is of type tau be aware that we always use the same context and that n has the type sigma which is the input type of m this is quite intuitive and it resembles the modus ponens if you want to know more about the correspondence of the lambda calculus and logic please refer to chapter 7.

[00:11:17]lastly the abstraction rule says that if we have a context containing some declarations in gamma and the declaration x is of type sigma and this context yields that m is of type tau then we can derive that gamma also yields that the abstraction lambda x of type sigma dot m is of type sigma to tau so to unpack that a little whenever we have a term m of an arbitrary type and in our context we have that x is also of an arbitrary type and we can abstract x from m and we're going to get an abstraction of the corresponding type you may have noticed that these derivation rules look a lot like the formation rules that we have for lambda terms if we have a variable it's a legal lambda term for two lambda terms m and n we can form a new legal lambda term by applying m to n if their types match accordingly and lastly if we have a variable x and a legal term m we can form an abstraction with its type depending on the type of x and m if you think about it this makes quite a bit of sense as those rules should enable us to derive all simply type lambda terms so although these rules might look a bit complicated at first the idea behind them is quite simple applying them does need some practice especially since we have to go bottom up so the last task will be to look at four examples together with increasing complexity to get used to the notion example number one is the identity function we guessed that without any further assumption in an empty context lambda x of type alpha.x has the type alpha to alpha so we want to prove this given judgment the term obviously consists of an abstraction so we need to apply the abstraction rule the types sigma and tau from the rule are in our case both alpha so we need to take gamma which was empty and add the declaration of x of type alpha this yields the term m which in our case was just x of type alpha so next we try to derive the judgment that x of type alpha yields x of type alpha since all that's left is a declaration on the right side of the judgment we have to apply the variable rule which is indeed possible so we've reached our axiom and finished the derivation so lambda x of type alpha.x is indeed a legal term from now on we're going to omit the variable rule if it's clear that we've reached an axiom this is always the case when we have only a declaration on the right side which is contained in the context on the left the second term that we want to prove legal is lambda x of type alpha dot y applied to x we assumed this would have the type alpha to some sigma for now let's say the context is empty once again we have an abstraction so we have to take x of type alpha into our context and y apply to x then needs to have the type sigma this time we need to apply the application rule y is the term m x is the term n and sigma is the type tau the context is x of type alpha in the application rule bottom to top it looks as if we gain a new type sigma and now the question is what is this type in the rule there's no restrictions on sigma apart from it being the type of n obtainable from the context gamma so we're going to use the placeholder type for now whenever we reach a point where we need a specific type or we see any other restrictions we're just going to adjust this placeholder the two premises we get are therefore context x of type alpha yields x of type tau and context x of type alpha yields y of type tau to sigma don't get confused that the roles of sigma and tau in our examples are switched this is going to happen quite often as we use sigma and tau frequently for arbitrary types the placeholder type in our example is tau here we can see that the second premise can only be true if tau is alpha otherwise we can't apply any more rules and we're stuck on a judgment which is not an axiom so we replace tau by alpha now we can see that in the first premise we're stuck two this is the case because we haven't specified the type of the free variable y we already saw this problem earlier when making informal derivations after introducing all definitions this derivation doesn't work but if we change the context we started with from empty to y of type alpha to sigma and also change the derivation accordingly we can derive the judgment both premises at the top are axioms and so they're also true the third example looks a bit more complex it's meant to show you that the derivation process is basically always the same just following the derivation rules and it also shows that the type of a specific lambda term can almost always be read from the term itself from an empty context we want to derive that lambda y of type alpha to better lambda z of type alpha dot y applied to z is of type alpha to beta to alpha to beta this type should be read as the term first has a term of type alpha to better as an input and it returns of type alpha to beta so the output still has an input of alpha on its own and the type of the final output is better obviously we have an abstraction and we have to apply the abstraction rule y of type alpha to beta is added to the context and cut from the declaration again an abstraction which leaves the judgment y of type alpha to better and z of type alpha yields y applied to z of type beta lastly an application so we get two premises the first says that the term y should map the type of zed to the type better and the second says that z should be of some type matching y we see again the placeholder type sigma which in the case of the second premise needs to be alpha otherwise we'd get stuck but as we can see this all works out we get two axioms since the declaration on the right side also appears in the context as the last example we want to look at a derivation that doesn't work it's one that we mentioned briefly already and it's quite similar to the third derivation from the empty context we want to derive lambda x of type alpha lambda y of type beta dot x y is of some type now we know already that we need an arrow type for an abstraction so let's put sigma to tau since x is of type alpha we know sigma has to be alpha so we change that now we can apply the abstraction rule here lambda y of type beta dot x y is again an abstraction with input beta so tau has to be some type beta to row and we can apply the abstraction rule again we've reached an application once again so we have to apply the application rule and we get these two premises we can see that sigma has to be better for the second premise to be true but the first premise can't really be saved x needs to be of type better to row for some type row but it's of type alpha this doesn't work so this term is therefore not legal that's going to do it for this video we covered the definition of types and pre-typed terms and we also got to know derivations which are crucial in deciding which terms are actually simply typed and which are not in the second video of the simply type lambda calculus we're going to look at some interesting properties of this system thank you very much for watching and see you then