# Type inference for Haskell, part 4

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

After seeing some examples but before getting to the actual type inference code, it is good to know the rules of the type system. If you wanted, you could start from these rules and arrive at a proof of the soundness of the type system. However, I’m interested in going in another direction with them, and using the rules to help clarify what the type inference code is doing. The code is actually a fairly direct translation of the rules. Hopefully knowing the rules will help bridge the gap between what the type inference code is doing and what is going on in the code it is inferring the type for.

These rules align to syntactic forms. To recap, those forms are literal values, variables, let expressions, function abstractions (aka lambda expressions), constructors, and function applications (aka function calls).

The process of type inference can be thought of as two processes: reading the syntax tree to find what rules apply and then finding a solution that conforms to those rules. In practice, these two steps are done at once, but it would be possible to separate them if wanted. All of the constraints either say something about the type of the current expression, or the type of one of the sub-expressions. The final solution will meet the constraints defined by all of the rules.

## Literals

Literals are simple. The only rule is that the type of a literal is determined directly by what sort of literal it is. `123`

is an `Int`

, `"foo"`

is a string, and so on.

## Variables

Variables, on the other hand, are somewhat subtle. The two rules could be summarized as: the variable must be in scope, and the type of an expression which is a variable is the type of that variable. However, there are some details not really captured by those two points.

The first detail is what it means for a variable to be in scope. In an expression like `let v1 = e1 in e2`

, the variable *v1* is in scope only in the expression *e2* (and not in *e1*^{1}). In an expression like `(\v1 -> e1)`

, *v1* is in scope in *e1*. In either case, *v1* might shadow another definition of the variable that is in scope already.

Second, “the type of that variable” is rather hand-wavey. This refers to the final type of the variable after all the constraints have been solved for. If a variable is used in multiple places, it will have exactly the same type in all of those places^{2}. That means that if one usage of a variable impacts the type, then it impacts the type for all the different places where that variable is used. More on that in a moment.

## Let bindings

Let bindings also have two rules. In an expression like `let v1 = e1 in e2`

, the type of the variable *v1* and the expression *e1* must be the same. Note that this constraint is bi-directional - the type of *v1* can influence the type of *e1* the same way that the type of *e1* can influence the type of *v1*. A restriction to the type of either applies to both. As mentioned previously, *v1* is not in scope in *e1*, so that needs to be taken into account when inferring the type for *e1*.

Note that this requirement that the types be equal is different from how languages like Java work where the expression could possibly be a subtype of the variable’s type (e.g. `List x = new ArrayList()`

). When the program is run, the value computed by the expression *e1* will be assigned to *v1*, which will certainly be valid if both *e1* and *v1* are the same type.

The second rule is that the type of the whole let expression is the type of the second sub-expression *e2*. The type of that is inferred with *v1* in scope. That’s because when a let expression is evaluated, the result of the second inner expression is used as the result of the whole expression.

## Function abstraction

(Remember that all functions actually have a single argument.)

First of all, the type of a function abstraction needs to be a function type. That is to say, the type for an expression like `(\v1 -> e1)`

will have some type `t1 -> t2`

.

The type *t1* will be whatever type is found for the variable *v1*. This refers to the final type the variable gets at the end of type inference, after all the usages of the variable have been taken into account.

Similarly, the return type *t2* will be the type that is found for the expression *e1*. The variable *v1* is in scope when inferring the type of *e1*. That variable shadows any existing definition of a variable with the same name.

## Function application

Function applications like `e1 e2`

have the function on the left-hand side (*e1*) and the argument on the right-hand side (*e2*).

Starting with the left-hand side, the type of *e1* must be some function type. That means it will be in the form `t1 -> t2`

, for some *t1* and *t2*.

Looking at the right-hand side, the type of *e2* must be the same as the argument type *t1* of the function.

Finally, the type of the whole expression is the return type of the function *t2*. Like with variables, this refers to the final type the return type of the function takes on when the type inference process has finished evaluating all the other rules.

## Constructors

Constructors (like `Just`

or `Left`

) are handled a bit differently. Their type is determined by the declaration of that data type. For example, the type of the constructor `Nothing`

would be `Maybe a`

. The constructor `Left`

would have the type `a -> Either a b`

. It’s a function type because you use `Left`

just like a function, applying it to another value. For example, `Left "an error"`

is an expression of type `Either String b`

.

We won’t be dealing with the logic to figure out what the types are based on the data type declarations, but it isn’t particularly complicated to implement.

## Clarifications

There are some details and implications of these rules that might not be clear from the statement of the rules themselves.

The equality of types is transitive. If one rule states that the expression *e1* has the same type as the expression *e2*, and *e2* has the same type as *e3*, then you know that the type of *e1* is the same as the type of *e3*. If some rules then tells you something about the type of *e1*, that gets applied to the type of *e2* and of *e3* as well. When a rule says that the type of one thing should be the same as the type of some other thing, it means “add that constraint to the list of things we need to solve for” not “use what we currently know about the type of the other thing as the type of this thing.” All the rules will be things that hold true when type inference has finished.

It’s also worth pointing out the fact that you can’t fully determine the type of an expression until you’ve looked at all of the other expressions. Any expression somewhere else in the program might use a variable and restrict its type. If the expression you are looking at also uses that variable, that could impact the resulting type of this expression.

Function applications can provide information about the type of both the left-hand side (the expression that results in a function) and the right-hand side (the expression that produces the value to use as an argument). In fact, function application is the only operation that provides more information about the type of other expressions. That information will ultimately result in updating the type of variables (assuming, of course, that there are no type errors).

An implicit assumption of these rules is that there are no type errors in inner expressions - these rules assume that the rules in sub-expressions also get solved for by the type inference algorithm.

Another implicit assumption is that the type of a variable is the same everywhere that variable is used (ignoring variable shadowing, which technically creates a new variable). This is not the case in Haskell. To extend this system to match Haskell’s behavior, the rule about a variable will need to be changed in an interesting way. For now, just assume that a variable has a single type and that any rules that talk about its type are all referring to the same thing.

It might sound like it would be really complicated to implement logic to figure out how to solve for all of these rules. However, you are in luck. The type inference algorithm actually consists of a few simple uses of a handful of smaller algorithms. That’s what we’ll look at in the next post.

For anyone comparing this to what they are reading elsewhere, know that the type system these rules describe is slightly less powerful than Hindley-Milner type inference (aka Algorithm-W). Our system is (at the moment) missing let-polymorphism.