As we begin our study of type inference I want to start by making sure whereas clear as we can be about what type inference is and what problem its trying to solve. So, when you have type-checking at compile time, which is called static type-checking, it lets us reject programs before we ever run them. And we do this to prevent the possibility of some errors. So statistically typed programming languages are languages that have this feature. So you might have some function that does not type check because potentially it might say try to call a number, treat a number as. The function.We don't actually have to execute the function to get that error, we get that error before we ever run a program.Conversely dynamically type languages do little or perhaps none of that's what of checking so, you have to actually not just call the function but actually get the particular problematic expression. To evaluate with variables bound to the right things before you see the potential error. Now the relative advantages of static and dynamic type-checking is a major concept in the course and we're going to study it but I want to do that after we've used the dynamically typed programming language for a while. And Racket is one so we'll be in good shape Right there. At this point we've only seen ML and ML like Java, C, Scala etc. is statically typed. It has this property that certain things don't type check even before we run them. And what all of these statically typed languages have in common is every variable we introduce is given a type. Every binding has some type. And for the scope that it's usable, it maintains that type and can only hold values of that type. So we keep our strings, and our booles, and our functions and out tuples separate. Now the reason why I'm emphasizing this is that, even though ML is statically typed, it is implicitly typed. Ever since the beginning of section 2 or so, we have not been writing down the types of any of our variables. We never did for valve bindings, and only at the beginning of the course when you were using hash 1 and hash 2, did we for arguments to a function. So just because ml is implicitly typed, it can sometimes be confusing to remember that it is statically typed. In this first function here f, the 2 variables f and x both have a type. F has type n 0 int, x has type int and they're just as statically typed as if this were Java or C, where we have to write down the types of all of our variables when we introduce them. That is why when we have a function like g we under put the type error, the reason for the type error here is that one of the type checking rules in and all is that the then branch and the else branch of the conditional have to have the same type. So that, that can be the type of the entire if expression and in this case therefore the return type of g and so when these don't match like a bull here and a int here we get a type error.This is exactly the sort of thing in a dynamically typed language I would expect to be allowed and depending on the argument to g you either get back a bull. Or an int, okay, so in that sense of static type checking ML is more like Java or C and less like JavaScript or Python. So what then is the type inference problem? The type inference problem is take a program, like we saw in the previous slide, and try to give every variable and binding and expression in that program a type. Such that, if you wrote down all those types, type checking would succeed. So we need to infer all the types such that the program would type check. If we cannot do so, if it is impossible to give such types, like in that second example where true and x * 2 simply do not have the same type, then it's the role of type inference to fail, and presumably give some sort of error message. So, in principle, you could set it up exactly like this. You could have a type inference procedure that wrote down the types for everything, and then have a type checker, that checked those types. In practice, and in implementation of a language like SML, we often don't separate things out so cleanly. We just have the type inferencer and type checker be the same. Staying, and either your program type-checks, or it does not. The last thing I want to emphasize, before the next segment, when we get into type inference for ML, this segment was really about type inference in general, and what it is. As the type inference can be easy, or difficult, or impossible, it depends, on the type system, that That you're trying to infer types four. So as 2 extreme view points if if every program type checks, that's very easy to infer. Just say yes, if no program type checks that's also easy to infer, just say no. So type inference doesn't get easier or harder necessarily by having a type system that accepts more programs or excepts fewer programs. It's not so simply to figure that out. This is part of the difficulty of language design if you want type inference. But the reason why we're going to study ML type inference is that it is a bit subtle, but it's also extremely elegant, and it may at this point in the course seem magical. We've seen these polymorphic types sort of inferred for us, but through a series of examples I want to convince you that it's actually a fairly elegant and straightforward procedure.