and we can use that. Then for each binding,

say, a val binding, or file, fun binding, we have to figure out the type of that

binding. What we do is we analyze the definition

for all necessary facts. These are essentially things that are

going to constrain the type in some way. So, for example, if you see the

expression x > or = 0 inside a function that takes a parameter x,

then x must have type int. We simply look at the, function body in

order to figure out the type of the function overall.

We gather all these facts, we figure out what those constraints imply and

sometimes, they imply things that can't possibly all be true.

That's exactly when you get a type error. If we try to have in our function body x

> or = 0, and x concatenated with the string high, then x has to be an int and

a string, and that's impossible and so you get an error message.

Now, after we've figured out everything the constraints imply and it's, if it's

not a contradiction, so the function or variable will type-check.

Sometimes, we still have too few constraints.

Things that can still be anything, it doesn't matter what type they have.

And that's exactly when we get to infer a polymorphic function, something with a a'

or a b' in it. For example, if you have some function

argument that the function body never uses, then it can clearly be anything, it

doesn't have to be the same as any other type and we can introduce a fresh type

variable for that argument. And then, there is this last step, which

is we have to enforce the value restriction and we're going to ignore

that until one segment later in the section that's focused just on the value

restriction. Alright.

So, here's an example. In future segments, we're going to do our

examples much more step-by-step very much like the actual algorithm does it.

But do get a sense of how these constraints work, let's just keep it

high-level and do this like more how humans would do it.

So, we have two bindings, which we're going to do in order.

First, val x = 42. That's easy.

You see 42, it has type int so x must have type int.

Now, we have this function f, so we know it's going to have some function type.

We have to figure out the types of the arguments and the return type.

So, we just look at the function body. We see if y, then something,

well, y must have type bool. We see z + x, z must have type int,

because x is an int and the only thing you can add to an int is an int.

So great, y is a bool, z is an int. There's a bunch of other things we have

to check. We have to check that this x really does

have an appropriate argument for plus, it does.

We have to check that this 0 has the same type as the type of the expression in the

then branch, it does. So, we're checking all this as

we're doing inference and now, we're basically done.

The entire body here can have type int, so the return type of f will be int. And

then, we notice that w over here never got constrained.

w can be anything. There are no facts that constrain, well,

it has to be in any way, so we know that f must return an int, and we know it must

take a bool, an int, and anything you want.

So, as that sort of last step, we turn that anything you want into a type

variable and we give f this type, bool * int * alpha arrow int.

And if we go over here and try it out, we'll see that that's exactly what the

type checker says as well, okay? So, one more point I want to make,

which is that a central feature of ML type inference is that it does generate

these polymorphic expressions things with type variables whenever it can.

This is great for code reuse and for understanding functions.

It actually tells us in that example that you know, you're never using the argument

w which is why I was able to give it this more general type.

But I want to emphasize because it is often confused, that type inference and

polymorphism with type variables are entirely different concepts, you could

have a language that has type inference and doesn't have type variable.

It would make it harder to infer a type for that previous example but they really

are separate concepts. And conversely, you can have languages with type

variables that do not have type inference, that require programmers to

write down all the types. And Java, in most situations, is a pretty good example

of that. If you want a polymorphic function in

Java, you still have to write down all the types of all the arguments of the

method that happens to be polymorphic.