Hindley-Milner Type System Explained | Polymorphic Lambda Calculus Theory

[00:00:00]hey everyone today we're talking about the hindley milner type system we're not going to spend quite as much time on the formal theory of semantic analysis and type system as we did for parsers and languages the reason is it's difficult to reason about parsers and languages and it's really useful to have this theory for semantic analysis most of the challenges are engineering challenges nevertheless there is some very good formal and fundamental work that has been done and this work actually has practical applications so i will be remiss not to talk to you about it the hindi miller type system and you can see in leo miller on the right it's a type system for the polymorphic lambda calculus which is also called system f it is relevant in practice because it underlies the type system of haskell and ml and probably other languages also of course languages are much more intricate than the lambda calculus which is an abstract story language however the hindu military type system is still the core of the algorithm behind the type system of those languages let's refresh your knowledge on the lambda calculus the lambda calculus is a set of expression that looks like this so there are variables there are function abstractions so basically just function definition with one parameter and there are function applications next there is the simply typed lambda calculus and the idea is to introduce types into the lambda clause and this takes the form of type annotations on the parameters of the abstractions we also need to introduce constants we'll also need a set of base types so for instance the set b which has the a and b types the universe of type so the set of all types that we can create in the simply typed learning calculus is made of the base types and all function types that can be made from the base types so here from a to the function type a to b so why are the constants necessary we didn't have them in the normal lambda calculus the reason is that in the normal lambda calculus you can represent things like numbers using functions and you do that using something called church encoding in the simply type lambda calculus because of the type annotations the church encoding does not work anymore and so you do need constants otherwise your language does not have any object you can never do function application because there is no value that inhibits the types finally the polymorphic claim the calculus the idea is to take the original lambda outlet and to have type for that without the type annotations that the simply typed lender calculus introduced and so this is the normal lambda class and then we also have this extra let's statement we will explain later why that is actually needed in the polymerase lambda calculus we haven't really said what a type system is type system is a formal system or a formalism that determines for any expression in the language if the expression is well typed and if the expression is well typed what its exact type is so let me give you an example in the simply type plan the calculus this expression is ill-typed and it's very simple it's an abstraction with parameter of type a and we apply it on a constant step b so obviously b to a that's not compatible so this is l types a few desirable properties of type systems assignability which means that or typing algorithm can make a decision it does not run forever and does not crash soundness which means that everything that we can prove everything the type system says is actually true and completeness which is that we can prove everything that is true this doesn't seem like asking for much but actually it is we know from godel's incompleteness theorem that there is no sound system of action describing natural number arithmetic that can be complete a natural number arithmetic that's positive integers and arithmetic means that we have multiplication and addition that doesn't seem like too much to ask and a sound system that describes that's a system that only proves true things can be complete which means that there are statements about natural numbers that we can approve for any system so this is one of the most hurt shattering results of mathematics of course we are computer scientists we are programmers we are not mathematicians and so we are also bounded by pragmatic considerations which means that in practice this does not always matter for instance java is not any of those it's not decidable because you can actually write programs that will crash the compiler this is arguably a compiled bug and so it should be disabled it is not sound because you can compile some programs that will always crash at runtime for type reasons and it's not complete because there are things that are true in the underlying theory that cannot compel in practice however it doesn't matter because the programs that exhibit these dispatch properties nobody would ever write them they are complete corner cases also in practice you probably want to get decidability and soundness you want your compiler to crash or to hang forever then you do not want to allow invalid program typically what you will sacrifice is completeness so there's going to be some programs that are well typed in theory that we're not going to accept and once again typically we're talking about porno cases before we discuss inle milner which is a type system for the polymorphic lambda calculus let us discuss type system for the simply typed lander calculus which is denoted by this symbol so we have four inference rules with one or multiple premises on the top and a conclusion on the bottom you may notice the symbols in the rules so gamma is a context which is a set of type bindings also called assignment or assumptions the symbol here that's called a turnstile denotes a type judgment and it's typically preceded by gamma a type judgment is what gives us information about the types and finally sigma and toe are characters used to denote types let's start with the first rule this says that if the type binding that x is of type sigma is within the context then we have a type judgment of the same effect this is just mathematical accounting it just says that the context tells the truth about types the second rule is similarly simple it just says that if c is a constant of type t then we have a type judgment to the same effect thing get interesting in the third row so in this rule we take a context but then we adjoin a type binding that says that x is of type sigma if we can show that using that context then the expression e has type 2 then we can show that a function or an abstraction with a parameter of type sigma and a body e as type sigma u2 sigma is the type annotation for the parameter if we assume it and if using another rule we can show that e has type 2 then this does make sense a function we know the parameter type and through the premise we do also know the written type so how do we get this premise well we get it through some other rule so for instance e could be a constant then we could use rule 2 to say that whatever actually the parameter type is the return time will always be the type of the constant and then this is easy to type finally we have the fourth rule which is for function application here is an example of function application so it says if we have an expression e1 which has a function type sigma-2 and e2 which has a type sigma so in this case this would be e1 and this would be e2 again how do we get this judgment from other rules so in this case i used a constant so we would get the type judgment from this rule this being an abstraction we would get the type judgment from this rule once we have that we can say that applying the function e1 to the value e2 has type 2 or this makes sense e1 is a function from sigma to 2.

[00:09:01]you give it a parameter sigma you get back a value of type 2.

[00:09:07]so none of this should be very surprising these are the normal rules to get the type of function and to type the usage of function to go towards the full inlet milner type system we can start by using the same rules we only have three rules because the polymorphic lambda calculus does not have constants otherwise it's pretty much the same you can ignore the d after a turn style that's because i took these equations from the wikipedia page and they have multiple formalization for the hindley milner type system and this is the declarative formalization the only difference is that abstraction does not have type annotations and this does have a very important consequence which is that functions can have many types so if you take this function here it's the identity function if you assume that x is of type end this function has type end to end if you assume that x is of type string this function has type string to string and so on and so forth so why is it actually called the polymorphic lambda calculus polymorphism means many forms and as we've seen some function may have many types but shouldn't they really have one canonical type can't we express the fact that this function works on all sorts of type as a matter of fact we can we can use such a type here and this is read as for all alpha alpha to alpha and this is a polymorphic type so you can see that the universe of types in the polymorphic lambda calculus is divided between monomorphic types which includes variable and abstraction there's this here that you should ignore that's used for other formalizations and polymorphic types which are either monomorphic types or quantified types now why do we actually need polymorphic types here is an example so this is a function application so the first line is an abstraction and the second line is also an abstraction it's the identity function and it's passed as a parameter to the abstraction on the first line the body of that abstraction is not really important it's that way so that it's syntactically correct what is important is that it calls the identity function twice it calls it once with an integer and calls it once with a string using the current rules this can never work because the parameter has to be typed before the whole application can be typed and so either you will give it the type into int then you can call this but you cannot call this or you will give it the type string to string then you cannot do this application but you can do this application the hope is that by using a polymorphic type we will be able to make this work somehow for that we will need new inference rules that actually include polymorphic types so how do we actually introduce polymorphic types into the calculus for this we need an inference rule that allows us to give a polymorphic types to functions this is the generalization rule here what it says is that if we can infer that e as type sigma and that the variable alpha is not free in gamma and we'll explain what that means then we can generalize the type of e to become flow alpha sigma so what does it mean for a variable to be bound it means that appears in gamma either as a quantified variable so for instance this variable is not free or it appears in a function type for instance here but it must also never appear on its own if you have a variable in gamma with type is alpha then you cannot generalize over alpha do you actually get this variable from well we get it from the abstraction rule as we said there are many functions such as the identity function that have many types and that means that we can actually pick whatever type we like for this function for instance for the identity function we could expect alpha for toe here and so that gives us the type alpha to alpha from the conclusion so that's the abstraction rule and then we use the generalization rule to generalize that to 40 alpha alpha to alpha so this is the first step and if we take our example again this means that now we can assign a polymorphic type this function however what we cannot do is apply this function why because if you look at the application rule the function has to be two to two prime and these are monomorphic types and there's no allowance for polymorphism there so what we need is an inference rule that goes from the polymorphic type to a specialized step and this is the instantiation rule what it says is that if we have inferred that e is of type sigma prime and we know that sigma is more specific than sigma prime then we can specialize e to b of type sigma so this notation here means sigma is more specific than sigma prime it's a bit confusing because it looks like set inclusion and the way i like to think of it is as a set of constraints so the set of constraints of sigma is bigger than a set of constraint of sigma prime because sigma is more specific so sigma includes all the constraint that sigma prime does in practice all you need to remember is that we use the instantiation rule to go from a polymorphic type into a specific type and with that we'll be able to instantiate here to a n-type function and here to a string type function and then we can actually use the application let's now talk about this let form that we have and at first glance it's very confusing because you might think that let x equals e1 and e2 would be exactly the same as this form here which is passing e1 into an abstraction or the body is e2 the only reason it is not the same is that the application rule says that e1 has to be of type 2 and if you remember 2 denotes a monomorphic type so before when we did this example actually light because sure you can type this to a polymorphic type but then you cannot do the application because this does not satisfy the premise it has to be monomorphic however and that's where let comes in you can rewrite this to be like this instead so now we say let id equals the identity function in the same body as before and this does work because of the later rule so the letter rule says if we can infer that e0 is of type sigma and if we assume that x is of type sigma then we can infer that e1 is up type 2 then let x equals e0 in e1 as of type 2.

[00:16:35]the best way to think of the let rule is that it's the combination of the abstraction rule and the application rule so this rule here is very similar to this premise here and this premise here for the value that gets assigned is very similar to this premise here and basically what the let does is that it plugs the conclusion of the abstraction into the premise of the application there so it does both steps at once the only difference of course is that it is able to handle polymorphic types whereas an application will stack with metamorphic types so why do we have this weird restriction why must application work only on many more tips the reason is that if we do not put this restriction then the polymorphic clander calculus becomes undecidable this is very undesirable remember that if it's undecidable then a practical decision procedure might not terminate as to why it is like this this is beyond the scope of the course it will be very difficult to explain in fact i couldn't explain it myself without doing some research but it suffices to know that the reason that let exists is to do things like this for this reason it's sometimes known as led generalization because using let lets you generalize function so that they may be called on arguments of different types and so that's the whole of the inliner type system these six rules it's really not that complicated it looks scary but once you understand the intuition behind it there's really nothing to be afraid of let me dispel some possible confusion what we have seen is a type system it is the semantics of a type system it's not typing algorithm so we have seen a bunch of inference rules and they can be used to prove statements about types we've called the statements type judgments we know that these statements are true because our system should be sound what's not given to us however is how to prove the statement which is to say which is to say which rules do we pick and when do we apply them and to do that we actually need a typing algorithm and so for in blah milner there are two typing algorithms algorithm j and algorithm w and typically the practical one is algorithm w these algorithms do have a close relationship with the underlying type system and they indeed help with efficiently selecting and applying inference rules so what have we learned in this video formal type systems usually work through the use of inference rules which are used to derive type judgments supported by a set of type bindings and we use these type bindings to make assumptions and types which can then be used to derive more type judgments inlay milner in particular is a type system for the polymorphic lambda calculus it only has six inference rules and they enable the use of polymorphic types and particular polymorphic function types this is relevant in practice as this is a theory behind the typing algorithm of sql ml and some other functional languages we've seen three desirable properties for typing systems decidability which means there exists a procedure that can make a typing decision soundness which is that everything the typing system proves is true and completeness which means that everything is true can be proven in the context of type system in the context of type system decidability means that there is an algorithm that is able to eventually make a decision so either the program is well typed ill-typed or the algorithm can also stop and decide not to type the program in the case is also incomplete soundness means that if the typing algorithm derives a type this type is correct it's never wrong completeness means that all program can be typed if you have to give up one of these three properties it's better to give up completeness right you don't want your program to assign types which are not correct and you don't want your type algorithm to hang forever finally pragmatically one reason i like to talk about formal type system is that the idea of inference rules has great practical applications even if you never write a formal type system the idea is that you can take some premises derive conclusions and this conclusion can be used as further premises this can be used to implement semantic analysis in practice type system but also the other form of analysis and in fact that's what we'll talk about next time and we'll use the uranium library that i wrote for that i hope this video has been instructive i wish you all the best see you next time