Skip main navigation

£199.99 £139.99 for one year of Unlimited learning. Offer ends on 28 February 2023 at 23:59 (UTC). T&Cs apply

Find out more

Type Inference by Example

Wim Vanderbauwhede presents an intuitive explanation of how type inference works in Haskell.
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.

Type inference is the process by which Haskell ‘guesses’ the types for variables and functions, without you needing to specify these types explicitly. Many functional languages feature type inference.

There is lots of theory behind type inference — Hindley-Milner type systems and Unification.

However we don’t need this level of detail. Like most car drivers, we don’t know too much about how the engine works — we just drive the car. This video gives a high-level intuition for how type inference operates, which is all we need to grasp for now.

This article is from the free online

Functional Programming in Haskell: Supercharge Your Coding

Created by
FutureLearn - Learning For Life

Our purpose is to transform access to education.

We offer a diverse selection of courses from leading universities and cultural institutions from around the world. These are delivered one step at a time, and are accessible on mobile, tablet and desktop, so you can fit learning around your life.

We believe learning should be an enjoyable, social experience, so our courses offer the opportunity to discuss what you’re learning with others as you go, helping you make fresh discoveries and form new ideas.
You can unlock new opportunities with unlimited access to hundreds of online short courses for a year by subscribing to our Unlimited package. Build your knowledge with top universities and organisations.

Learn more about how FutureLearn is transforming access to education