Type Inference by Example

WIM: Hello, everyone. In this short video, I want to give you an intuition on how type inference in Haskell works. As you know, in Haskell, you can provide type signatures to functions, but you don’t have to. And if you don’t, then the type checker will work out what the types are of the functions that you have provided. And I want to kind of give an idea of how that works, that process that the type checker uses to figure out what types your functions that you defined would actually have. So let’s just take an example of a function of x and xs, which we define like this.

So we have a function of two arguments– x and xs. And it returns the sum of the first argument and the length of the second argument. So then the question is, what is the type of this particular function? And so the answer is that the type checker will try putting very general types. So it will say this– this is a and this is b. And this is as good as it gets for me now. And so it will say f is a b, and then some c. And then it will try to infer the constraints on each of these type variables. And the more it can be constrained, the better.

So in the end, hopefully it will be so constrained that it will no longer be a type variable, but a particular concrete type. So in this particular case, we have already, from the Prelude, we have types for the plus operation and for the length function. So we know that plus is of type Num a, and that the length is of type– let’s call this b, maybe, because they don’t have to be the same. So we know that length of xs, if this has to be a valid type checking function, this will have to be of type Int. And we know, from the type signature of the addition, that the types of both arguments must be the same.

So consequently, this will also have to be of type Int. So, because the x here is the x here, we already know that our type of our first argument must be Int. For the type of our next argument, well, we know that it’s a list because we call the length function on it. But that’s really all we can tell because we don’t need to know what’s in the list to calculate its length. So the type of the arguments of the list are not important. So that means that, in the end, the type inference will say that it has found a function which takes an Int and something– a list of some arbitrary type– and it will return an Int.

And so it works. So the type checker tries to apply more and more constraints so that it can actually resolve the entire types. So for instance, if we had done something like this, then automatically, we would know that head xs would have to be also type Int. Now, we know the signature for the head function. So we know this, which means that this list would have to be of type Integer. So you see, by making the expression a little bit different, we used the element of the list, and immediately, the type inference can tell us that this has to be a list of Integers. And so, in general, that’s how the whole process works.

It works by a combination of the structure of the types and the type definitions of the basic functions in the Prelude. There’s actually a lot more to this, but we will cover this in a later lecture.