Hindley-Milner Type Inference: Type Systems Explained | CSE 340 Lecture

[00:00:00]cool uh good morning everyone I I guess I missed you yeah I missed being here with you that's always fun um cool so I hope you had a good class on Monday you can tell me about it after um and then I hope you watch the lecture because we're done with kind of basic types and now we're going to go into more complex and interesting type inference so specifically today we're going to talk about hindley Milner type inference which is a essentially a more advanced or there's two ways to think about it either you can think about what you're doing is a smaller scale down version of hindley mner type inference or you can think of Hy Milner type inference is much more um expressive and does more things than what your project 4 is doing but either way they're related so that's cool can we ask questions about the project after make we cover this questions on types type questions okay so we looked at the type systems right so all the type systems that we' seen so far how do we know the type of a variable and everything we've looked at in the type systems that we studied how do we know the type of a variable it's given what was it it's given who gives it me well kind of but yeah the programmer right so exactly so the programmer is explicitly declaring the types of the variables right they say I want a variable Fu and it has this type bar right so we've seen that with all kinds of examples so we've seen examples with arrays where we give the range of the array and the elements of the array what type they are uh what so well Pop Quiz what kind of what's the name of this type of a the name of it with the name of the type of a uh yeah what's the name of the type of a integer so let's think about this separately so what is the type of a int int was an array of in right right declaring an a the type is array of six elements of int of integers but what's the name of that type an array array type is array a name or is array a basic type so if I said it's a Fu a or something right where fu is some programmer defined type then what would be the name of that type f right exactly so does this type have a name yes no right this is an anonymous type this is a type with no name we are not declaring that there is a type called array 0 to 5 of int right in our type declaration this is a variable declaration right that whole statement is a type correct okay right because this is a type Constructor right we're constructing a new type of array based on some of our basic types you could say that the array has a type arrays of type in and then uh the specific array that we're talking about here has range 0 to five and holds ins yes you could say that but specifically about the name right so why is that important why are the names of the types important type equivalency yeah type equivalency that we studied right name equivalence internal name equivalence and structural equivalence right okay so here we just have an in I right and then we know that now once the programmer has defined these types now if we see their usage in the program we can say whether they're correct or not so is this would this type check and why yes yes why because I is an INT because I is an INT so why does I have to be an INT because it's being used in the index of an array which is need to be an which must be an integer yeah and that's the output of any index of array of Z through five of type in defined as or named a is the output of an INT so setting it equal to an end is correct right so you have this array operator essentially if you think about the type system returning something right returns this type int and so you're checking that this int here is the same as this type here which is an INT right and you're saying yes that that type checks cool and so now we know right so if we have a different program where I is declared as a string type right if we were to do this would this type check no why not because the index I is not the string isn't going to return something valid most likely right so the reason is the types right so the type of the bracket operator means that to do an array access we access arrays based on their element right not on strings yeah if you switched I to a CH would it try and convert it to ma value of it or would it just crash out depend on your language I imagine uh it definitely depends on the language right here we're talking a little bit more not like concretely in C but kind of more in this language we've been talking about where the type system we kind of I mean we want to be very strict right so uh you could actually maybe so let's see if you knew the range of the array right and you saw a character in here if the range is bigger than a character then you could say that that doesn't type check right because a character can't describe all possible indices um that would be interesting that's what you can do when you know the size of every array so you could do some cool tricks like that cool okay so can we do something like this can we have our array of in a and in I and do AI equals string testing no why not because you're trying to load a type string into an array that contains its exactly so here we have we have a string so we're trying to set a string equal to the return of the array access operation right so in all these types what's the return of the array array AIS operation of a a memory location for an INT in types so don't think about memory locations so just get rid of that an INT right it's the it's what is inside of this array right memory array access is giving us one of the elements of this array so it's essentially peeling back all that other types so we're checking is int equal to a string well no of course not okay so at this point in your careers I think you're familiar with some more Express type systems and what we've seen here right so what are parameterized types what does that mean right so in some language so like generics in Java or templates in C++ right what does that actually allow you to do yeah you can provide a a type argument to another type so if you wanted to make a like you had a list you could give that was like a generic you say list yeah exactly so you can actually use this allows you so it's parameterized right so it's essentially like the type is a parameter to either a function or or a class so instead of defining a function on two integers right you can define a function on two types that are the same right which is actually more generic and that means that function can be used in more scenarios right and it allows the programmer a lot more abstraction and EMP power in defining these more generic types of functions um and so the idea is the type it's weird uh the typee is given as a parameter to either the function or the class so gener Java and c will have generics templates and C++ both do this and so let's look at an example so you can write a a function in Java so here we're going to create a static random variable we're going to have a static method called choose that is going to take in two parameters first or second and the idea is this function will randomly return one of those values either the first or the second right so you think of this this is I don't know a handy function where if you just want to randomly choose one of these two elements this function will allow you to do that right so without parameterized types you can only do this with you would have to specify the exact types of each of the arguments right you would have to say first has to be an INT and second has to be an INT but really from what this function does we just want it to return return one of the two we don't care what the types of those arguments are right we only want to just return one of them and in fact in this the types are completely irrelevant right as long as they're the same right so why do they have to be the same because because you're only outputting one exactly we're only outputting one so the function that calls us right needs to know the type of whatever we're returning so it can properly manage the types right so if these were two different types then we just return some random type and all type safety would go to heck so we can do this very easily we can have a little function that calls randomx in it gets an integer it mods it with two so mod two is going to return either zero or one depending on if it's odd or even and if it's zero it'll return first if it's one it'll return second right so now we have this generic method that we can apply to any types any parameters so we can in our function we can have variables X and Y right which are integers and then we can print out choos or. choose X or Y but didn't I say that the parameters here to the types have to be passed as parameters so did I specify any of the types here no so how does the how does Java type check this we would look at the angle so from the invocation of this function right did I how if I want to specify exactly the parameter of the type could I do that yeah think you had brackets I can't remember here or here you had brackets here I think yeah um you had brackets here to specify exactly which type you want to do or does or does it know because both of them are of the same type it just exactly it just figures it out can look here right and it can say okay I'm calling a parameterized function both the first parameter and the second parameter are of the same type so are X and Y of the same type yeah yeah and what is that type in so it knows to invoke this with passive using int as the argument yes is that true for all generic Java that they'll figure it'll figure it out if which is part of the problem that's why it's not as smart so we're building up so we're going to see that m is much more powerful than this um but this is kind of what you can use in Java which Java is kind of getting there these other languages are getting there so you strings so I can call the exact same method with strings right and Java has enough information at this function in location to know exactly which type to create okay questions on that yeah so it'll work the ah what am I returning from the choose method what type am I returning you're returning an in t I'm returning a t whatever what is T whatever you pass it whatever is that parameter of this method whatever the type of that parameter of this method is right so in this invocation this type parameter is int so it's going to return an INT T is going to be an INT when we invoke it here it's going to be a string and it's going to return type string yeah will the return type ever be different than the parameter types no that's exactly what this constraint here says this constraint of this method says that the return type is always the same as the arguments so you can think about essentially one way to think about it is every time this function is invoked it it looks and sees well not exactly when it's invoked even beforehand it can see that okay this is on ins so I know T is an INT so I can make a whole new copy of this method replacing t with int everywhere it's just a regular Java function and then with this the same thing I know here T is a string so I can create the exact same thing a brand new copy of this method replacing alt T's with strings yeah so then that means the parameters have to be the same type also yes they can never be different and that's defined here so you can you can use generics to have as many types as you want you can have t u v whatever in this list this defines the the parameters but where those are used that defines the relation between the types cool don't you have to use this when you use like an array list or this is exactly what's happening right so because an array list right or any kind of list you don't really care what types you're putting in it doesn't affect anything right but you want that class to be specialized on that type because you want to be able to put in let's say strings in one array list and ins in another array list not a great example because of the Primitive but the high the same okay so in this case we have what's known as explicit polymorphism so the idea is the programmer is declaring the parameterized types explicitly right the parameter the programmer is explicitly saying here's a function right and here are the types to that function right it's going to take in a type T in this example so one type so it's important that this is a little bit of different polymorphism than what you're used to thinking about in the object orientation right here we're thinking kind of on functions and types so that I can use the same function in different places just like with object polymorphism right I can use I can call a parent class and depending on the specialization of that class right it may call a different method and so this is great because it allows you can call a function or a you know a class with different types while still checking type compatibility so you still get all the guarantees of the type system the type system will ensure that everything is still good um but we go back here we still had to say this type T right just like just like in the previous things we've looked at we have to explicitly declare the types of variables here but let's say if I got rid of this T and didn't put specify any types of this function could you come up with the types that this function should have that the type constraints here that each of the parameters have the same type and the return value has the same type so let's think about that uh and so this leads us into where we want to go which is even more powerful and very cool where we as the programmer don't even want to specify the type parameters right so we want to be able to not even specify any of the type parameters and we want the system to essentially infer the types that we want and create the program accordingly so Dynamic languages right we don't do we have to specify in a lot of dynamic languages do we have to specify the types so in python or JavaScript or Ruby do you have to specify the types of the variables no no I think we talked about this a little bit before right but is that do you think it's better worse worse worse it's more complicated for sure under um yeah it's it it can be worse in the sense that you don't know when you run the program if it's correctly typed or not right you could be add trying to add strings with lists or something right um whereas with a compile time language like Java you don't have that but there are there can be a lot of cases where have you ever tried to make changes to your program right so like oh man I was using this string but now I want to instead of using a string I want to change that with a struct or an object right so you have to go through in every place you use that variable and every single parameter every single function you need to change that to now use this new type right otherwise the compiler won't let you won't let it work um the other nice thing about Java I mean some things about python that are nice is you can they use kind of what's known as they call it like Duck typing so rather than so basically the idea is if it walks like a duck swims like a duck and quacks like a duck duck then it's a duck what this means is I don't care about object hierarchy parent children whatever if I get an object and I call a function on that object if it has that function then I'm happy right I don't break the type system and if it takes the same parameters and everything so and this is nice because you can write very generic functions you can have a function that um let's say sorts elements and as long as it knows how to compare things and pass them to some kind of compare function then it can properly do the Sorting right so in that sense you can have functions that are a little bit more generic but you have to give up the fact that you have this nice safety net of static typ checking so what's super cool about what we're learning is with implicit polymorphism and with hind hindley mner type inference you kind of get the best of both worlds so the type system is going to actually statically check and verify that the types of your program are correct while at the same time the programmer does not have to specify any of the types so the program is going to automatically try to infer the most General type for every single construct function function invocation everything in the program expression in the program so if it can't solve this if there are no types types that solve this then it will say there's a type error otherwise it will figure it out and it's actually very nice because you as the programmer you don't have to specify the types you can trust the compiler to figure it out what you meant that things are ins or strings and then later on if you want to change that it makes it a lot easier we also see it allows you to write functions that are a lot more General than what we're used to so let's look at an example so before I get started on this right this is a principles of programming languages class right programming languages is one of those words or two of those four words I guess um right so we're going to be we've been talking about a lot of different kinds of programming languages so here I'm going to introduce some kind of new it's more of a functional programming language syntax it should be fairly clear I don't think it's it's not meant to be tricky it's just meant to be easy to look at and discuss because this is the way that a lot of um a lot of these languages that do implicit polymorphism how they look so it's just easier to kind of and we can talk about some of the differences there so for instance when we do have function definitions we're going to use fun because functions are fun right so we're defining a function fu fu takes one parameter X and so what does FU return X yeah returns it returns to the first parameter right X so that's the definition here so f xal x so now what is the type of Fu so do we specify any types here no no but what can you tell me about the types here whatever X's type is because it has to return X so whatever the type of X is is right okay so let's talk about think about this first how many different types are there in this little function definition zero how many things do we need to the Spectrum there covering everything it's actually negative Infinity so damn um so how many things do we need to be able to say what the type is like do we okay for instance do we need to know the type of x no no wow the program is going to statically determine that right it needs to determine types for every variables to do type checking right so the programmer doesn't have to specify but the types syst needs to figure out a type of X right what else does it need to figure out types of what was that F fu yeah we also have a function that we're defining Fu right so we also need to know the type of Foo actually one of the coolest things about programming in a language like this is you can actually while you're programming you can ask the type system what exactly is the type of X or Fu and it will tell you what it thinks the type is and if it thinks it's something really weird that means your program is wrong and so actually often times so I've done some programming in okl which is based on this and it's crazy because like like you'll be fighting the type system but then when your types all work your program actually works because it's actually what you meant for it to do so so if we were to do a type of Fu what's the type of function Fu using kind of the type syntax that we've talked about before so what what could we give the type of Fu right so what is the type of X is it uny Anonymous generic unspecified yeah I think these are all the same things we can say basically say it's any type right so we can just make up a new name for it right we can make up some name t right so we say it's some type T so the type of X is some type T so then what does that mean about the type of Fu it's t yeah if x is type of T then but fu is a function is X a function returns exactly right so using so fu is a function and what do we know about types of functions what do we have to say to specify the type of a function return return just return type input types the word for that parameters parameters yeah so the types of the parameters and the return type right exactly so if we're to use this fu is a function that what takes in what type T type T and Returns what type type T we can know this just by looking at that so basically this means right whatever we invoke Foo with as the type whatever the type of the thing that we invoke Foo as the return type is going to be that same thing right so if we call Foo with a string we're going to get back a string if we call Foo with a list we're going to get back a list if we call Fu with a function that takes in another function that takes in another function that returns an in it's going to return that same thing so it doesn't matter what we pass in we know that the type that gets returned is always the same thing so we're also going to change our the way we write functions uh the types of functions so what we're going to do is we're going to put all of the parameters of T in bra the par sorry the types of the parameters of a function in parentheses right separated by commas and then we're going to have an arrow with the return type of T So this means a function that takes in type T and returns type t and this is just to we can keep doing it like this this is a little more succinct plus it uh is exactly the format that most uh languages that use this use so it'll also help you if you use any of these languages okay so let's say we have some function Fu X that returns X right so our same function above and let's say we have another function bar y that returns Fu of Y so now what's the type of bar and Fu can we determine it well of white just Returns the of which would just be why so what's the type of food is the type of food Change no right so fu is a function of T that takes in one parameter type T and returns a parameter type T right which we're going to write as TT and what about bar Type U that returns yeah so we can we we actually reuse the same terminology because we're what this means is that in this function bar these types have to be the same right right the input to T must be the output of t but the relation between these two T's has no relation right they could just as easily be some other random value okay let's look at so let's say we have a function Max so we're going to say if x is less than y then if we're writing a correct Max function what should we return y otherwise X right so more things to notice about this function this uh language we don't have explicit returns right so we're not saying return y or return x what we're actually doing is we're saying an if statement actually returns something implicitly so the result of a value so an if is just an expression that if its condition is true it will return whatever it's true block uh returns otherwise it'll return whatever it's false block returns right so now what's the type of Max or maybe put another way do you have enough information to decide the type of Max why not because X and Y not necess I I would say for this to work X and Y have to be typ why because they have to be comp well they just have to be comparable okay yes so there's a couple things so there's actually two separate issues here right so just like your homework right we have X less than y I guess your project right what does that mean about the types of X and Y they must be they must be comparable they must be the same type comparable yeah that's part of the problem right we actually don't know if they have to be the same type it kind of depends on the language but it really depends on what this so is this less than operator can you think of that as a function mhm so if it's a function what does it take in what would it type be T oh Boolean bits what does it take in how many parameters does it take in Tak takes a two param two parameters let's say of the same type T and T yeah right and Returns what a Boolean exactly so but let's say this is a less than symbol that's only defined on integers right so it's in int Boolean so then what does that say about the types of X and Y they have to be ins they have to be ins okay let's think about this from another perspective let's say this was some random function we don't really care when we're thinking about okay when we first look at this right X and Y could be arbitrarily different types right we don't have enough information to say that they're the same type or different types but looking at this program right depending on which branch we go down if we go down this Branch we return y if we go down this Branch we're going to return X so what does that tell us about the types of Y and X they have to be the same they have to be the same exactly right so these types must be the same because they're used in two different if branches right so another way to think about this if you have an if Branch right each of the types of the branches must be the same because no matter which branch you go down you might have to return the same thing yeah you mean for the less than yeah I mean like you said iser yes so it depends on the it depends on the specification so uh if we're assuming that the less than symbol is only defined on ins then we're going to say that Max is a function that takes in an integer and an integer and returns an integer right there's nothing more General we can say about this we can't say it's an arbitrarily type T because we see from the usage in the function of this less than symbol and they have to be in right this is the most General and so the other way we write that is like in comma in Arrow in okay let's change it a little bit so but is this really general for the programmer no no it's kind of crappy right because it's we've written this what should be this Max function but because we the programmer use this less than symbol right we are inherently forcing this function to only work on integers which is what the less than symbol is so now we have to start thinking a little bit more higher level so think of the different languages so what really what we want so do we want to specify if we're writing a function for Max do we the programmer who writes this function for Max do we want to specify the comparator operator we just want to specify some kind of comparing function right we want some logic to use a comparator function in order to decide which of the two values is larger right but this isn't very general so why don't we let the programmer tell us what comparator function they want to to use so how can we do that by put function Yeah by using it as an argument right so let's extend our function right to have the programmer pass in a function to be called so for those of you that have used uh vectors or sets yeah you can tell them right in your in C++ you can tell it specifically what function to use to compare two elements of your set list are the same way as well right so this is extending that so the idea here is functions are essentially what they call First Class right we can pass functions as arguments we can return functions from functions we can treat functions functions are not different from any other variable type right they're just the same as strings or ins just that we can invoke them right we can call that function so now how would we rewrite that function that we just saw if the comparison of X and Y then y right so so now what's the type of Max T doesn't all it's let see it's a function right so it's not going to just have one type right so it's how many parameters is this type going to take in three three parameters each is type T the the the type of Max is the type of compare type of Max is the type of compare no how many variables so okay let's think about this so there's a couple different layers in here right so so we know just from looking at this the types of Max and the types of compare can't be the same why because compare is compare a returns Boolean but B how many parameters does it take two two compare takes two parameters Max takes three parameters right so max is a function that takes in as its first parameter a function that takes in how many parameters two two parameters and Returns what Boolean a Boolean what do we know about those two parameters they have to be equal why do they have to be equal does anything about this function inv vocation here say that they have to be right don't to be because the US they are they have to be the type of X and the type of Y right right because the because the programmer specifies the comparison function somewhere down the chain exactly but let's look at this remember what I said about if statements so what do we know about the types of Y and the type of X they have to be the same they have to be the same and they have to be the same as the return type of Max okay which means that the types of the compare function must also be the same okay right so this is actually a function of a function of right functions of T comma T which returns Boolean and then takes in a T and A T and returns a t so if we to write this in our simplified format right we have a function that takes in as its first argument a function two types of that function and returns a type T yeah so you know when you say like in a function the parameters you know they need to be the same type and the function should return the same Ty as right mhm so do you know how like that doesn't hold on the comparison function you're you're passing in you know T but you're returning sorry say that again so you know how Max well okay a function the parameters need to be the same T and T for instance and it t yes that should hold right that has to hold for Max okay so for um yes the parameters is TN but you're returning a Bole yes so why where is the CMP function used Max where inside Max specifically in the if statement in the condition of the if statement so what do we know that the condition of if statement has to return bullan Boolean right I mean that's kind of we I guess we didn't explicitly specify that but we'll see that but yeah we need that to be a Boolean so that's what we're saying is if it wasn't used here then there would be no constraint on the return type right the most General type would be some new type w that we haven't seen before but because specifically of its usage right here we know that it has to be a Boolean and if the function usage if we use compare somewhere else that's not the return type of compare is not a Boolean then we know we have a type error right so you can think of we we treat everything as really generic types and then B based on the usage we restrict them to more specific types so now we can do cool things right now we have actually a very general function we can call Max and we can pass in the less than operator and then pass in 10 and 200 right so we can call this function Max with the less than operator and we can also call it with the string compare function to compare strings right so Le the less than function is a function that takes in two integers right and returns a Boolean which now means that this function invocation here these must be integers right these T's must be the same and then we know that this function invocation must return an integer here we know string comp is a function that takes in two strings and returns a Boolean so we know that the types of these two parameters must be a strings and then the return type here must be a string and we got all of this without specifying any types okay look more so we can have a lot of fun with this this is why these are fun functions so now we have a function Fu how many parameters does it take in three three and then it returns result of calling C passing into to C's first argument the result of a bracket B right so based on the usage here what do we know about the types of A and C at a high level you don't have to get yeah C would have to be a function C is a function yes how many parameters one one one good what else what about a is an array a is an array and is an in and B must be an INT right we know from this usage we can see here from this array access B must be an in right we can only access arrays with ins this must B must be an in we know so there's other things implicitly that we know here so we know that the return type of C is also going to be the return type of Fu right we know those have to be the same we also know that whatever a is an array of let's say it's array of W's that must be the same type that c accepts as its first parameter right so we're going to have a function of so a is going to be some array of type t b is going to be an INT and then C is going to be a function that takes in a t and returns a u some new Type U and F returns you so actually even just from this type system we can kind of see a little bit what's going on we can see that like okay we have some array of some type T's we have some index into there and we have a function to translate from that type T to some new type which is the return value here so we have some way to trans it's essentially translating like C is translating from T's to so does this mean that T and U can't be the same not necessarily not necessarily exactly they can be the same it doesn't prevent that cool so this is in our simpler format all right new function so now we say a is 10 so usually we're not going to do it like this with the statements um but it should be very clear to read here so a is a 10 we're calling a passing in B bracket C so what's the type of Fu here so what's the type of let's go in reverse type of C int type of B array an array of something type of a and it you're and it oh I see a is a function that return that takes in an array of something in which kind is so what does this function say that a is what does this sorry function what does this line say what does this line say that a is function a function can something be a function and an INT if you believe if you believe hard enough no type error you cannot do that question yes so hindley mner type checking is a general algorithm to do this for a program to automatically infer what the types are at all points in the program and for all variables um and this is amazing because you as the programmer don't have to specify any of the types the type system will help you and decide the types for you and the key idea is it it leverages it uses kind of like you think of it as like base knowledge right it uses these these things that we were doing right of array access means that the argument to the array access returns some type I and that means the array that you're access must be a type array uh it uses function calls so it knows that at function calls the types have to be based on the invocation it knows how many parameters need to be in that function um and then it builds up on that and it builds these together to try to infer the types and if it can't if it ever gets to a point where it tries to say oh an inch is the same as a function or an inch is the same as a string then it throws a type error and so this full the full hindle m type checking is used in oel F Pascal a lot of actually really cool languages that are fun to play with okay so the key idea here is you first need the type constraints of your language right if you have no constraints then you're everything always typed Tex right um so we first have constant integers right so we know what what the types of constant integers in we're going to call them ins they're going to be type in constant real numbers so when we have floating Point numbers what's the type of those real reals we have constant Boolean so we have true or false looks oddly almost like you're doing a homework assignment on thisf right types Boolean and we have strings right where the types are strings so constants all the constants have specified types we have our operators so we have relational operators so we have some operator which has some type T1 and I'm going to draw in tree syntax which is going to be clear when we go through the algorithm so we have our operator and we have the first the left side which is a the right side which is B right so the way we like to think about these is these are elements of the tree of the parse tree right we have our operator it has a left child which is another node it has a right child and it has all these types T1 T2 T3 so our type and operat in this case is all these different types of operators so what we have here is we have constraints our type system is going to enforce constraints so it knows when it sees a relational operator what does it know about the types here from your project that type uh T2 and T3 have to be equal and T2 and T3 have to be equal yes what else and type T1 is a Boolean yeah type T1 must be a Boolean type t t three must be equal and you can also say maybe they have to be numeric types or like in our language you can just say they have to be the same type all right arithmetic operators right work very similarly so we have plus minus multiply divide so the constraints could be that now here they all have to be the same type right because when you add two numbers to ins together what do you get an in yes um so we're saying that they're all the same and this constraint says that they have to be a numeric type right so this would restrict us even further by saying maybe it can't be a string we have our array access operator right on the left side we have the array that's being accessed and on the right side we have the parameter that's inside that array access so this would be a bracket B we can see there right so what does this tell us about the types T1 T2 and T3 T1 and T2 equal T must T1 and T2 must be equal shouldn't it because if because you have an array of whatever type so you have an array of in what happens when you access an element to that array what type get returns returns an INT what's the type of a in that situation array of same thing as an it it is very close though so what is the relationship between T1 and T2 T2 is a ray of type T1 yes exactly so T2 right must be an array of type T1 right so we know that a must be an array and we know that whatever that array is composed of must be the same as whatever it returns so then what do we know about T3 here got to be an in okay function application so we're going to uh use this to represent apply so function applications and on the left most we're going to have the definition of the function so it's going to be F then we're going to have all of the parameters of that function oh so application so this is not function definition this is one we're calling a function so what does this tell us about the types here when we call this function so what do we know about the constraints here what does this tell us about f f is the return type f is uh we're going to do the f is the type of variable FU oh the return type is going to be R okay yeah so what does it tell us about f it a function with types T through t0 is that t yeah t0 T1 through TK yeah what does it return and it returns R yeah so F right F this tells us that F must be some function and it's a function that takes in these arguments and it returns whatever type that that returns all right we will stop here we will finish this on Friday