Hindley-Milner Algorithm W: Type Inference Explained

[00:00:00]hello and welcome to this video on Henley Milner algorithm w if you haven't seen the intro to this mini-series I recommend you go and watch that but otherwise we're going to jump in and look at the algorithm so what is this definition of telling us there's a few things that we see initially at the top we see this W uh colon Type n to expert Subs times type and what this is saying is that we have an algorithm algorithm W which is our type inference algorithm the inputs uh like each time we call this we pass in a tuple of a typing environment which is like a context and an expression so this might be our Lambda expression so part of these two things is arguments and then it returns uh a tuple of a substitution so this is like our substitution uh from type variable uh to type um and then also a type so specifically it's basically our method signature or function signature for this algorithm W um and it kind of makes sense what we'd expect we pass in a context and an expression um and then we get back some type for that expression um the substitution back might not be obvious at first months but this is actually needed so we can combine substitutions across different types uh when we need to do that so you're kind of gathering those constraints within a substitution where we make recursive calls down below so we have a few different kind of versions of this you can see we've got four different things and actually these four different versions are for our four different Expressions so this is effectively doing pattern matching so we say well if we're calling algorithm W and we've got a contact so the context is always the same we've got some some context Capital gamma if we're calling it with a variable expression then we do this thing if we call it with a function abstraction expression then we do this thing uh a function application expression we do this thing and a let statement then we do this thing so let's have a look at these cases we'll start with the variable expression first given that's the simplest one it's the only one to fit in one line and what it's saying is Well if you want to call algorithmw and you have a context and some variable expression X well then you need to return this thing so it's saying you're calling this thing then is equal to like kind of you get the result back um this thing and this is our our substitution and type it's a tuple so the first thing is our substitution and our substitution we're just saying is ID and that's like the identity substitutions or like the empty substitution and then next we're also getting a type back so this type it's a little complicated we haven't seen something quite like it before we've got a Tau here right so Tau some type Tau and we're also replacing all our Alphas so we have some vectors of Alphas so these are our type variables that it's Quantified by and we're replacing them with a vector of betas and so there we have a where clause which basically explains what these things that we're returning are so our context when we take X out of our context so we look up X in our context provided X is there we should get some monotype that might be prefixed by a number of type variables so there's some poly type with monotype and variables and these variables for each kind of variable we've got there we'll create a new uh type variable so really it's saying take it take a new Vector of uh betas so for example let's say this type that we got out our context was for all a for all B A to B right then this new beta means we have to replace all those things uh with new type variables that we haven't seen before so let's say we have some type variables like t0 and T1 and nowhere else have we use t0 and T1 then that that's basically what our new thing means then we can say well this type where we replaced all these Alphas that were in front of the type with betas might look like um t0 to T1 I should have specified earlier but this syntax here with the kind of curly brackets and this slash is uh this is some substitution we're saying we're substituting all the Alphas with uh betas and then we're going to apply that to to Tau and so that's what we return we return the empty substitution and uh Tau effectively instantiated right where we're replacing all the for all Alphas in front of it with these new type variables that we're going to call beta which will make a t0 T1 Etc okay let's go on to our function abstraction so this is where we're creating a new function we're defining a new function where we're saying a new function uh takes in One X and then returns this expression e so let's look at that well this is actually uh two lines we're actually basically going to use our let binding syntax uh within our rule um so this isn't the let binding syntax that we've been using in our Lambda calculus there's some extensions for example in this one you can actually see this multiple definitions and we've also got like things like defining tuples like this but you can think of it similarly in that we're going to Define this thing and then we're going to use the results of this in here so you can see we're defining S1 and Tau 1 in here and then we actually use Tau 1 and then S1 in our second line so what are we setting with this let in binding well we're saying that S1 which is probably a substitution one and Tau one which is probably a monotype one is going to be equal to the result of calling uh so it's like a a sub call or a cursive call to argument W where we have the same context as we had before plus an additional assignment where we say we're going to assign X this type beta and we're going to say again as we had this kind of new type variable here we have a new type variable beta here so this might be you know T2 for example as long as we haven't used T2 anywhere else so we say access type T2 plus the existing context and then we're going to figure out the value of the expression e which remember was our body of the function so again this actually looks pretty similar to our typing rule for function abstraction where we're taking the context we're adding sexual assignment and then we're inferring this uh expression e right and we get back our substitution S1 and Tau 1. and so the return of this is S1 so the same substitution and then S1 applied to Beta goes to Tau 1. and why might we get this type well it's a function right because we've defined a function so we should expect function type and the return type should be it's returning this expression e so the return type should be this Tau one which is the type of the expression e that we found out and the argument it takes should be this beta because remember we created this new beta and we said that X our kind of input parameter is going to have this type beta so we have the beta and using the uh S1 the substitution one here and applying it to the beta is going to be any kind of constraints that we've picked up by applying algorithm W to this I'm going to then be applied on that beta so for example if our function when we infer it it tells us well then the input type beta should have to you know unify with an integer well then that means it should be an integer and so we're going to apply that and get an integer back next rule we have function application so this is where we have two expressions we've got E1 and E2 and first we look at E1 uh so we call algorithm W uh and we're going to say with that same context how's E1 doing we get the results there we do the same thing for E2 and get the results there you'll notice we're actually pass in substitution one and apply that to the context first this is so if there are any constraints in E1 that we just learned about by running algorithmw on it we are kind of aware of them when we're running E2 so if there's something that conflicts within E2 we'll actually throw an error here by knowing that hey something's not quite right because we you know we updated our contacts when we applied this S1 and we learned something from inferring E1 and now we can infer E2 and if there's a problem we draw an error otherwise we get back this new substitution and so I'll do here so now that we have the types of these two expressions so we've got this Tau one and this Tau two right we know the types of them but we need to check do these actually go together and so that's why we need to unify with kind of our expected type and the actual type so what we're going to do is that this weird swirly U here is our symbol for the unify function so we looked at unifying in a previous video and go back and check that if you are not familiar with it what we're going to unify is this T1 type which is going to be our E1 which is going to be our function so you should expect the function type should be something that takes a T2 right because our T2 is an argument so he said it should say that this T1 should take a T2 and then return some beta we don't know what that beta is we're going to say it needs to you know take a T2 and return some Beta And as we have done before we're going to create this new beta so this is going to be a new type variable so this might be you know type variable T3 T4 anything that we haven't seen before right um so we have our function type should unify with the input type to something um and we're going to unify those together and then we get a new substitution out of that so provided these unify um we get another substitution which tells us what we need to apply to make sure they actually unify and then our return type is we combine all these substitutions so we have S3 S2 and S1 all three substitutions together we want to combine all those constraints that we've just discovered and then we're also going to return the return type of this thing right we said beta was the return type of a function and this whole thing once you apply a argument uh in a function you get back the return type so we're expecting this beta as a return type and we also need to apply the unification constraint to that again because we want to combine those constraints and get back the actual return type so lastly we have the let in binding again we're calling rmw and we have context and the let statement so we have let x equals E1 in E2 so we have some expression that we're setting X to and then we're saying well we can use x within here and it should have the value E1 sort of have you done well we've said uh we need to figure out the type of E1 first so we're going to call algorithm W on that E1 and we get some type Tau 1 for that E1 and next we're going to use that type so we know that X has this kind of type Tau 1.

[00:09:39]and we want to figure out the value of the body E2 so we're going to ask algorithmw to look at E2 again and in this case we're going to say well we want the same context but we also know now that X has this uh type Tau one so you know I'm jumping over a few things here but we're going to imagine that we just say algorithm W we're going to ask it for the context and we also know that now X has Type Tau 1 is also in our context because we've just defined it here and we're going to ask that and then say what is the type of E2 and so what are these extra bits well first off we have to apply the substitution S1 to our context in case we learn anything you know extra from from inferring this type X so maybe extra constraints with how we're using other things so if we're using a thing in a certain way like for example we're calling odd on a variable within that we might end up with a constraint that well this variable has to be an integer because that's what I'm expecting so that's kind of included on our substitution so we apply that substitution to our context that's that one and we also ask uh for this like clause function over the substitution S1 and our context so apply the substitution S1 to our context and we have the updated context I'm going to ask Claus on that context plus our tau1 which is Computing our kind of uh generalized version of Tau one so what in Taiwan is not restricted anywhere else in our context and therefore what can we kind of put for all uh type quantifiers in front of and that way we can have a very generalized type so again this used to be called a generalize or gem in uh the damerson uh amount of paper I believe and that's what this function does it's kind of our generalized rule implemented there so saying well we have our updated context and we have X having the kind of most generalized version of our type Tau one that we found and then we're going to use that to infer E2 so that's why let binding is related to generalization and then finally we're going to do the same thing where we're combining these other constraints that we've learned about uh through combining our substitutions and then returning tau2 which is our return type of this E2 which is the main thing and now that binding so that's been quite a hand wavy Rush run through of algorithm W hopefully it's been helpful in understanding what all these parts mean what the syntax is meaning and will allow you to go and read it yourself and maybe spend some time understanding it in future videos we're also going to look at algorithm M as well as actually implementing this in typescript so if you're more familiar with maybe you know imperative languages or you just like typescript then uh look forward to that and hopefully you can uh maybe better understand where it's you know fully defined and you can actually run it and write tests for it exactly on your own machine thanks for watching and see you in the next one