Type inference for Haskell, part 3

Posted on January 3, 2019

This is part 3 of the series on type inference for Haskell.

The next post in this series will lay out the rules that type inference follows. But before seeing the rules, it will be useful to have an intuitive understanding of how type inference behaves. To help give you a sense of what it does, in this post I’ll walk through some examples of code and what the type inference algorithm does with them. These examples will assume a few functions like +, :, and others are already in scope, but are otherwise self-contained. Each example can be run in GHCi to test it out for yourself.

You will need to put :t before these expressions to have GHCi print out the type it infers. Note that in the examples involving numbers, it will infer a more general Num a type instead of Int. That involves type classes, which our subset of Haskell doesn’t support just yet. Those will get added later in this series.

To start with, not all expressions are valid. An undefined variable is an error:

Prelude> :t someUndefinedVariable

<interactive>:4:1: error:
    Variable not in scope: someUndefinedVariable

This is a sort of error that the type inference algorithm will need to be able to handle.

Let statements are one of the ways that a variable can be introduced.

let a = 10 in [a, a]

In our type system, the type inferred for this will be [Int] (though Haskell will infer a more general type involving typeclasses, Num t => [t]). There are a number of things that can be seen in this small example. First, the type of the overall expression is the type of the second sub-expression (the [a, a]). Second, the second sub-expression is allowed to use the variable introduced (a). Third, note how the type of that second sub-expression depends on the type of the first (the 10). The fact that a is an Int is important for figuring out the fact that the whole expression is a [Int].

Like full-blown Haskell, our language allows shadowing variables. This means that an inner definition of a variable can re-use a name that is already used in and outer definition. When this happens, the outer definition is hidden (or, “shadowed”) while the inner one is in scope. For example:

let a = "foo"
in  let a = 10
    in  a + a

(Put that example on a single line when trying it out.)

The type of this expression is Int because the expression a + a uses the inner definition of a where it is bound to 10. That definition shadows the one where a is bound to "foo". (Since our language doesn’t support type classes yet, I’m working under the assumption that + has the type Int -> Int -> Int.)

In function expressions, the body of the function determines the return type while the argument to the function determines the argument type. Sometimes the argument type can be any type. Consider this function literal:

(\x -> 'q')

If you try to evaluate this directly in GHCi, it will complain that it cannot print it. However, running :t (\x -> 'q') will succeed in giving you the type. Our type for this will be t1 -> Char. You can see that the type for the argument x can be anything. Because since x is never referenced, any value would work without causing a type error. The return type of the function matches up with the type of the expression the function evaluates to.

The return type of a function might be tied to the argument type. As a simple example,

(\x -> x)

The type is simply t -> t. That means that whatever type of the value given as the argument is will be the type of the return value. That makes sense, given that whatever value is given as an argument will be the return value. This type could just as well have been written a -> a or t1 -> t1. All that matters is that the two type variables are the same. Note that it would not have been correct to use a different type variable for the return type than for the argument type. Doing that would imply that you are allowed to expect a different type to be returned than what you gave the function (e.g. expecting an Int out after giving it a Bool).

The function body could also be a larger expression.

(\x -> x + x)

This function is an Int -> Int. The return type is an Int because the returned value is the result of applying + (which I’m assuming to be Int -> Int -> Int). The most interesting fact is that the argument type is also an Int. This means that the usage of x inside the function body influenced its type out in the function definition.

That’s part of a more general principle: any usage of a variable can influence what its type is allowed to be. Multiple usages of the same variable can restrict it in different ways, and the resulting type of that variable needs to be something that meets all of those restrictions. If that is not possible, there is a type error.

As an example of that sort of type error, consider this code that tries to use x as both a function and as a number:

(\x -> (x 123) + x)

Trying to find a type for this function fails because there is no possible type for x that meets the restrictions here - it can’t be both a function taking numbers (which it has to be in order to be applied to 123) and a number itself (in order to be added with +).

That being said, there is nothing wrong with applying an argument as a function:

(\foo -> foo 123)

This has the type (Int -> a) -> a. (Note the difference in grouping between this type and the type Int -> (a -> a), which is equivalent to Int -> a -> a. Our type means we take a function (Int -> a) as an argument and return an a, whereas the other type means we take an Int as an argument and return an a -> a.) Notice that, since this code doesn’t do anything with the return value of foo, the function’s type doesn’t place any restrictions on what that return type can be.

What happens if the return type of foo is used for something?

(\foo -> foo 1 + foo 2)

The type for this one does end up being (Int -> Int) -> Int, meaning that the argument foo must be something of type (Int -> Int). By using the return value of foo as an argument to +, we have forced it to be an Int as well. Again, note how the information gained by examining how foo is used bubbles up to the type of the function expression.

Another interesting way that type information can spread around is by going across the = sign in a let expression. This is a result of the fact that the variable introduced ends up being the same type as whatever expression produces the value that you assign to that variable.

(\a -> let b = a in b)

The type of this is t -> t. Hopefully this makes intuitive sense once you trace what the function does: Whatever value is given to the function is bound to a. That value then gets assigned to b, and then finally b is returned, meaning that whatever value is passed in to the function is the value that gets returned. Type inference needs to know that b has the same type as a (even though it doesn’t know what either of those are) in order to figure this out.

If you extend that example to apply some operation to b, you can see the type information go backwards across the =.

(\a -> let b = a in b + b)

This has the type Int -> Int. That’s interesting because it means that the fact that b is an Int caused it to realize that a also had to be an Int. It knows that because, in order to make b be an Int, whatever gets assigned to it had better also be an Int.

Take a look at this expression.

let a = 123
in (\x -> a)

That expression results in the function (\x -> a). That function ignores its argument and always returns 123 (the value of a). The type is then t -> Int. For all practical purposes, this is the same as the expression (\x -> 123). The thing I’m trying to show with this example is the fact that the type of a function might depend on a variable that is defined outside that function.

Function applications are where most type errors come from. That makes sense, given that almost all operations are represented as function applications. One simple way to get a type error is to try to use something that is not a function as though it were a function:

123 "foo"

That’s a type error because 123 clearly is not a function.

You can also get a type error when the function’s argument type doesn’t work with the argument given:

(\s -> "s is: " ++ s) 99

The type of (\s -> "s is: " ++ s) is String -> String (which Haskell spells [Char] -> [Char]). 99 is definitely not a String, so this function application fails.

Those are actually the only two ways that a function application can fail to type. If there was any problem with the return type, that would be discovered somewhere else (like another function application).

As you saw a few pages back, (\x -> x) has the type a -> a. Let’s look at what happens when you apply that function.

let identity = (\x -> x)
in identity "foo"

This expression evaluates to "foo", so its type is String. That means that the return type of identity must have also been String. But wait, didn’t identity have the type a -> a? How is its return type now String?

This is one of the really interesting properties of Haskell’s type system. The usage of a variable can change its type. More specifically, the usage of a variable can restrict its type. Here, though identity “starts out” as the type a -> a, using it with a String restricts the type to String -> String. Other languages with milder forms of type inference (e.g. Go) don’t have this behavior. In those languages, the type of the variable is determined entirely by the type of the expression the variable is initialized to.

There are several technical details around this topic that I’ll save for the next post. This includes things like what exactly it means to restrict a type.

In the meantime, let’s look at another example. In that use of identity, the argument type was known, and that was used to figure out the return type. Can it go the other way? If the return type is known, can that be used to figure out the argument type?

The code is a little more complicated, but it turns out that yes, you can construct a case where the argument type is figured out by knowing the return type:

(\s -> let identity = (\x -> x)
       in "foo" ++ (identity s))

The type of this is String -> String. Because it is being concatenated to another string, (identity s) must also be a string. In other words, we know that the return type of the identity call must be String. Besides this function application, there isn’t any other information about the type of s. The fact that the return type of identity is a String is enough to figure out the fact that s must also be a String. Knowing the type of s and the type of the expression the function evaluates to is enough to determine that the type of the whole function is String -> String.

What if neither the return type nor the argument type is known? What type is given for this?

(\a -> let identity = (\x -> x) in identity a)

Nothing tells what the return type of identity needs to be - the value is returned from the outer function without any other operations applied to it. And nothing tells what the type of a is, either. Besides applying identity to a, we don’t do any operations on it. What happens then? Without anything to constrain it, the type of identity stays generic (t -> t). As a result, the type of the whole expression remains generic, having type t -> t as well.

I mentioned before that with a function application, you can get type errors due to the left-hand side not being a function type, or due to the two sides disagreeing about the argument type (you could say that they have an argument about it. I’ll show myself out). You can get a very interesting variant of the second kind of error by trying to apply a function to itself:

(\f -> f f)

Haskell will give an error like “Occurs check: cannot construct the infinite type.” This is because any valid type would be infinitely large. Say the type of f was a -> b. That means the right-hand side of the function application f f has type a -> b, which means the argument type to f on the left-hand side must be a -> b. That means that the a in a -> b must be a -> b. So the type of f is actually (a -> b) -> b. But wait, that’s the type of the argument, too. So the type of the left copy of f must be ((a -> b) -> b) -> b. This continues forever without getting anywhere.

That being said, it can be OK to apply a function to itself. This, for example, works:

let identity = (\x -> x)
in identity identity

The type of this is t -> t because it ends up returning the identity function unmodified. But why was that allowed? Wouldn’t the type of identity end up becoming infinitely large? This works because of an interesting feature called “let-polymorphism” (poly- means many, morphḗ means shape, and let refers to the let expression). This feature allows variables introduced by a let block to have different types in different places where they are used (with some restrictions), just as long as each of those types agrees with the original definition.

In the identity identity, the right-hand side’s type is t -> t. The left-hand side’s type is (t -> t) -> (t -> t). By allowing the two usages to have different types, we don’t get stuck in an infinite loop when trying to figure out the type.

Let-polymorphism is one of the first features that will get added to our type system after getting the basics working.

Speaking of infinite loops, when they appear in expressions they can do weird things with types.

let foo = (\a -> foo a)
in foo "x"

Trying to evaluate this expression results in an infinite loop, foo forever calling itself over and over again. The weird part is that the type is simply t. There are no restrictions at all to what type you consider this expression to have. Is it a Int? Sure. Is it a [String]? Why not. Can it be used as a a -> a -> b? Yes! No matter what type you try to use it as, it will work. Running that code won’t result in a type error, either (it will just sit running that infinite loop). This is an interesting quirk of the type system, where every type is inhabited by a term. In fact, there is a simpler way to make this same effect:

let bar = bar in bar

Evaluating this is also an infinite loop in Haskell. Like let-polymorphism, recursion (whether silly like this or practically useful) is a feature that we’ll have to add after getting the basics working.

In the next post, we’ll look at the rules that give rise to the behavior seen here. My hope is that these examples will help the rules to make sense when you see them.