Implementing Algorithm W for Hindley-Milner Type Inference in TypeScript

[00:00:00]hello and welcome back to implementing Kenley Milner in typescript so in the previous video we set up some things uh we set up a typescript project where I've got some helper functions so for example dealing with substitutions uh applying them combining them dealing with instantiation and generalization of types uh as well as figuring out how to unify types um we then also you know had some models so of the actual Expressions that we're going to be inferring from and the types and then we've also got a parser so that we can kind of give it a string that represents uh whatever we're using um and then imitat for that as the expressions in this video we're going to look at implementing algorithm W so this is the slide I had uh from previous videos uh which you know was taken uh from a paper um link down uh in the description for reference uh but this is uh algorithm W um and so we have definition here we've built all the helpers and so now we should be able to implement it uh so let's uh Jump Right In we've also looked at a previous video uh at kind of how to read this I guess so if you haven't seen that that might be useful and understanding how I'm going from this algorithm to the typescript but hopefully uh should be fairly straightforward so um we'll create a new function I call it w for algorithm W uh and so we can see it takes a typing environment and an expression and then returns a substitution and a type so let's give it that type signature um so it has a typing and which we call context I guess we could call this context as well within here but I'll just call that for now an expression uh which can be of type expression and that's going to return a substitution and a type and when it says type uh really what that means is monotype cool and so you can do that so we've got W has a context and expression and returns a substitution to monotype and then we've got these four different cases so as I said when we were building the helper functions uh what algorithm W is basically going to look like is doing pattern matching on the kind of types of these expressions and then executing whatever the thing on on the writers um and so we can do that pretty easily so the first one is I guess just X so if it's a variable expression so you can do if our expression type is well uh then we need to do this thing well what we're doing is basically this is our kind of conditions and then this is what we're returning so we're going to return uh ID which is like the identity substitution or the empty substitution uh and then we're also going to uh return whatever the thing is in the context uh with that is now instantiated with these new type variables uh in a vector beta and so the first thing is we can deal with this wear condition so where X from the context is equal to this thing uh so we're going to say you know let's let's pull it from the context and we can say like uh value is iPad which is our from our context um and then the variable name which is going to be I think Express X right uh so putting X and pulling out the context which is this type end thing um cool and so we've got this value uh there is a edge case here which is if you use a variable that isn't defined you're going to get like a undefined value uh so we'll need to check for that so if this value like is uh undefined uh then we'll we'll throw an error saying that aha like hey uh undefined variable and we can give the name here as well I would say I think it's B expert or X and make this a template string uh so that get substituted um and then otherwise you can just return uh the thing right so which is the pair of the identity solution which is uh if we make a substitution just empty um and this type but instantiated so if we instantiate um value there we go that one's done because that's our VAR uh expression done uh for our functional abstraction let's do this one so the type is abs um well we've got two things so first we need to because we call algorithm W uh with the contacts plus this extra assignment X colon b um on the kind of body expression e um creating new to variable B um and then store that as a substitution uh S1 and T1 so let's let's do that so let's say we have I think we're gonna have to remember this new beta so we'll first have beta is just going to be a new type variable right that's what this new new beta means and then we can have S1 and tau1 is going to be equal to calling W on our context right so the same context but in this case we want to add this Expos Vector so we'll make a new context based off that context uh where we're going to let's run out our type our existing type environment so that's the same as this context here plus this extra assignment x uh to Beta so that would be expert.x uh maps to Beta cool that looks good um so that's our contacts done and then the other thing we need to pass in is the expression e so that would be the expert right and the next step is we just return this one so we return substitution S1 and then we return the type S1 applied to and then here we've got a function from beta to Tau one uh so this is going to be a type function application of uh the function type function um and the arguments are going to be beta and Tau 1.

[00:05:42]um and hopefully the syntax is making sense if not maybe go back look go back and watch the previous video on our helper functions and hopefully like the make contact stuff and applying these substitutions and defining our our types like this uh will make more sense cool so that's our abstraction rule done uh next we've got our rule for uh application an application uh we've got last one is just uh S1 Taiwan uh are going to be equal to calling uh W on our type environment and then E1 so let's watch a new one then we have S2 and tau2 and we want to combine the typing constraints that we learned when we called this the first time so we're going to apply the first substitution this S1 to our typing environment so we make sure we combine these constraints uh including them in type environment and we have E2 um uh there you go and then S3 is going to be our substitution that happens when we try and unify uh these these two types well not quite these two types but types that we can construct using uh this kind of rule where we have a tau2 to Beta and just Tau one uh what those should be together so uh we then apply S2 to Tau 1 so that we make sure that any constraints picked up here right in the second line get also applied back to this right whereas this one already contains the constraints from from both of them because we had the S1 constraints included there and also we've just generated S2 so we're going to unify that um and then also similarly here we're going to have this kind of thing right where we had a Time function application and in this case it's from T2 to Beta where beta is new so um say beta is a new type variable again um there we go that's good and then we're going to return this combined substitution so we're combining all those constraints uh into one substitution and then also getting this beta out using the substitution so S3 S2 S1 and then S3 on beta that looks good and then finally the last thing is our let in statement so if the expression type is let um then what we should do is have an S1 and Taiwan is equal to calling W on the same typing environment and U1 so expert E1 and then next step is S2 and tau2 is going to be calling W I'm going to use the same trick here where we add something to the context so let's copy that bit um so we're gonna have the existing type environment Plus in this case I actually want to apply substitution one first let's do S1 on type environment and then we have X and it's going to be generalize of um because that's the the Clause uh I think it's called short for closure but I'm not sure uh we're gonna we call it generalizing in kind of our stuff um so X has Type closure over this context uh gamma so that's our Type n type and um and Taiwan right um and then all that is you know sent into W with E2 that's just E2 at the end here good um and then finally we're gonna return uh S2 combined by S1 and tau2 um and that's basically our algorithm I think we might need just a throw exception at the bottom so um unknown expression type or something here uh this should never really be called and that's algorithmw mentioned typescript so that's the kind of uh Theory version that's the typescript version um all this code will be or if not this specific exact code uh code very similar to it will be available on GitHub also Link in description and this should do our algorithm so if for example we did um let's just check this still works so we could do um log pass um what do we have X to X something like this I'm using these two backslashes just because it's otherwise going to escape it um nothing so let's have a look at that so it can tell it's a abstraction from XX which is correct and then if we do uh W on that and we can just have a uh empty context to begin with uh because you don't need anything uh what we should get here is it should be a function from anything to anything uh so if we check uh that's what we get so we get the um if we look at the return type we get substitutional monotype we can kind of ignore the substitution at the end um but the type is uh frustratingly not uh shown so I'll do the uh what's up there to a depth fold procedure this just like make sure it's printed all out and we look at this there we go so it's a type application and it's going from t0 to t0 right with a type function uh a function type function there so it has the text edits you know from something to the same thing uh whereas if we did X to Y uh what's going to happen here is that Y is going to be undefined so it'll give a uh should throw an error saying that Y is undefined right based on uh this thing so if we hit save now uh there we go we get an error saying undefined variable y okay that looks like it's working and we want to try something else uh like imagine we had a context I'm just going to improve the formatting on this a little bit uh so let's try that um so imagine we had a context with some interesting things in it so if we had say uh uh not as type it's going to be a type application of the type function application um and it's going to go from type type application uh of ball which is uh nothing ball which looks correct um so this basically us defining like what's in the standard Library what are the types in the standard Library let's say odd is takes a um integer and tells you whether it's odd or not until it returns a pool and we can say there's so maybe some constants so uh true and pulse I just realized we have to use lowercase because uh our parser only supports lowercase identifies I also realize we never implemented a parentheses but we were gonna we can come back to that um so our true is just going to be a ball so it was false actually um so if also distributable um yeah I mean we could do numbers as well but yeah oh I'll do numbers why not uh we can say one is going to be uh or something spelled out because again we just did a text we could like add some number uh literals pretty easily so in this case uh this one is invalid so it's giving us a failed to pass error which is correct because we haven't written a valid Lambda expression um so let's say we did not true which should uh so this is well we could just do true which should tell us it's a Boolean uh great so it tells us it's a Boolean that looks right um if we did um not true this should also be a Boolean because it just flips it from Boolean uh to Boolean uh that's cool uh and similarly if we did say um one that should tell us it's an integer that is right uh and if we did uh odd one well that's should tell us if this is odd which uh the result of which should be a Boolean and so we should be able to see yeah that's a Boolean that's all working um if we did something more adventurous let's add the parentheses just because I want to try uh let's say we did uh we had an identity function and we applied that to one which should you know just keep whatever the same type is um and then we said uh let o equals odd in uh odd of all of this right well what that should be doing is it should be taking one keeping it the same so it's still just a number and then uh applying this function which then defined here which is uh the odd function and applying it across all lists So eventually it should should return rule so if we hit save now it's not going to work because it's not understanding what these brackets are doing so just give us a pause error yeah exactly so let's go back to our parser and add that the way we're going to add that is uh in this kind of expression parser what you could have is rather than any of these Expressions we could just have some parentheses so we're going to say uh we can try just kind of uh interpreting some parentheses and down here let's say yeah just because this is kind of the set semi-sensible order I think um we can say this is a parenthesis uh which can be a single parser or an expression because there should be some kind of expression inside and that's really what we are returning and uh all that we uh should expect inside parentheses are left parenthesis symbol uh that's like you know the uh opening bracket basically uh those kind of brackets um then we should get uh the actual kind of content so again we're going to use f dot lazy on the um on on the expression because I always get that infinite loop as we did for let expressions and the abstraction Expressions uh and then we should expect a uh write parenthesis there's a couple different options of what we could do here uh we could either then do like a map and then get the Tuple out uh but you know as we said for the uh two pools don't really know the types because I think these are different types and that's why they're getting a bit confused um so what we could do instead is we could just drop these uh parentheses because we're not getting any useful information out of it and then it should all probably know that it's a it's an expression uh so that's cool so we're just going to return that and knows there'll just be a single expression inside our parentheses uh that looks all good so if we go back uh I just hit save and actually it's already updated and yeah just as we expected when you find like ordinal lists uh it knows that it's a Boolean so it looks like all our things are working we've got our function abstraction we've got our variables we've got our let bindings um we've got our function application here um we've only got our parentheses so I think that's almost everything thrown off in the Lambda calculus uh We've generated our type so we haven't shown our polymorphism yet uh so I guess that's with our generalized part uh so the way we could show that is for example because it's in uh let Bindings that this generalization happens right it's only in this let where we have this generalize uh we can do it here so we could say let um a classic one is saying let the identity function be this because then this can be a polymorphic identity function rather than a normal one so normally uh it will only take one type so for example it could only take the type into int whereas because it's polymorphic here it will take like the type for all a um a to a because we're doing that generalization uh where it doesn't matter uh so under the hood really this like t0 to t0 and then this gets unified with the other parts on here and then it says well t0 must be an integer uh whereas in this case it like is generalized at this point here so we get this for all thing and then when it's used here it's instantiated and so these are just like always new type variables and so they don't like Clash for the other ones and that's how that kind of works under the hood so let's say we have this ID and in this case we want to use this ID function on one and then also the ID function on odd right where in this case ID is you know into int because it's one and in this case it's I don't know interball uh to interval and what I mean by that is like it's a function from interval and then it's like copying that because it's the same thing uh it's something like that right and so these are obviously different types and it's being used polymorphically uh because of that for all uh binding here so if we hit save we can see yeah that still works it still tells us that it's a ball uh for example that so that works really cool uh I guess the other thing we could show is uh just to prove that's not always just retelling at all we could have like an ad expression in this case uh it's a function which takes a well if you think about the the ad expression what it really has is type int to inch to int which is how you usually see it written and um actually this is like the bracketing I guess so you pause and want it and then you get another function where you take the other in and then you get get another link back um so if we try and unlock that so we have int and then this thing this whole thing is like that inside there again um so you have int to a function of intent and so now when we try and use add for example let's say we want to add one and one um what we're going to get is we should get a number back so we should get it back uh because it understands that but if we just did add one this is basically going to return like a plus one function if you imagine this what what you're calling here you say let uh plus one equals add one in plus one one this plus one function just has the type into where you give it one integer and it returns like whatever that thing is called maybe you call this increment or something but again if you hit save now uh you still just get back and um and in the previous example where we just had a plus one for example uh it like can do this partially applied function where it says oh yeah the type you've got here is is it didn't um so you know you know we've given it these contact these types in the context uh but in our actual program we haven't annotated it with types and then we'll just be inferred using uh type and phones algorithm w so that's uh Arkham W uh in practice in from basically a completely blank slate implementing the entire algorithm uh all the helper functions um in the next video we'll look at algorithm M briefly and then we'll wrap up and that'll be end of the series thanks for watching cheers