# Type inference for Haskell, part 8

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

*(THIH Section 6, Unification and Matching)*

Unification is the heart of type inference. It’s only about 20 lines of code, and it’s not that hard to understand what the code is doing. However, it’s going to take a while to explain *why* it does what it does.

Let’s start with what problem unification solves. Remember how I said that there are some points where we need to make two types equal to each other? One of the places where this happens is when we see a function application. The type of the function needs to be the same as another function type built out of the type of the argument and the return type.

Unification figures out how to actually accomplish causing those types to become the same.

The solution thus far is stored as a substitution. That substitution will (eventually) get applied to all the resulting types. So, to make the types be the same, we need to make the substitution be one that will, when applied to either of the two types, turn them into the same thing.

To put that another way, we want a substitution *S* such that `apply S t1 == apply S t2`

. That substitution is said to unify the types *t1* and *t2*.

Note that finding that substitution might fail. Since substitutions are only allowed to replace type variables, if the types differ by anything other than type variables, it won’t be possible for a substitution to make them into the same thing. For example, unifying `Bool`

with `Int`

will fail. Unifying `Int`

with `a -> a`

will also fail.

It would succeed for cases where the two types are already the same - that just gives an empty substitution.

What does it do for unifying a variable with another variable, e.g. `a`

and `b`

? It replaces one variable for the other. It happens to pick `a`

to be replaced with `b`

, but replacing `b`

with `a`

have been valid, too.

Let’s look at a more realistic example. If you applied the identity function to an integer, it would involve unifying `a -> a`

with `Int -> b`

. The resulting substitution replaces `a`

with `Int`

and `b`

with `Int`

, making both types `Int -> Int`

. Why does it do that? On the left-hand side, it sees that we need to unify `a`

with `Int`

. That’s easy, just replace `a`

with `Int`

. Now that `a`

is gone, the problem has become unifying `Int -> Int`

with `Int -> b`

. The right-hand side, unifying `Int`

with `b`

, can be solved by replacing `b`

with `Int`

.

I mentioned this could fail if the types are very different, like `Bool`

and `Int -> Int`

. This failure case can be a little bit more subtle because you can’t replace `a`

with two different things. For example, unifying `a -> a`

with `Int -> Bool`

will fail.

There’s also a different sort of case where this can fail. For example, you can’t unify `a`

with `a -> Int`

. Why not? Couldn’t you have a substitution that replaces `a`

with `a -> Int`

? The problem is that applying the substitution never “finishes” - you can always keep applying it again and get a different result. If you apply it once, you get `a -> Int`

. Apply it again, and you get `(a -> Int) -> Int`

, and so on. You end up with an infinitely large type. That’s covered by the `fail "occurs check fails"`

check below - it makes sure you aren’t replacing a type variable with something that contains that type variable.

Remember that `@@`

is the infix operator for composing two substitutions.

```
mgu :: Monad m => Type -> Type -> m Subst
mgu (TAp l r) (TAp l' r') = do
s1 <- mgu l l'
s2 <- mgu (apply s1 r) (apply s1 r')
return (s2 @@ s1)
mgu (TVar u) t =
varBind u t
mgu t (TVar u) =
varBind u t
mgu (TCon tc1) (TCon tc2)
| tc1 == tc2 = return nullSubst
mgu t1 t2 = fail "types do not unify"
varBind u t | t == TVar u = return nullSubst
| u `elem` tv t = fail "occurs check fails"
| otherwise = return (u +-> t)
```

Break down the logic by case to see what it is doing. (Case 1) If both types are type applications, recursively unify the left and right-hand sides and combine the result. This needs to take the solution to the left-hand side into account when processing the right-hand side, otherwise it would accidentally allow unifying things like `a -> a`

with `Int -> Bool`

. (Cases 2 & 3) If either type is a type variable, it can be substituted for the other type. (Case 4) If the two types are the same type constructor, succeed with an empty substitution. (Case 5) The two are different in some way that means they cannot be unified.

The `mgu`

function is wrapped by the `unify`

function. Before staring, the unify function gets the current substitution and applies it to the two types. This ensures that all we know so far about the solution is taken into account. After finding that substitution, it gets added to to the current solution with the `extSubst`

function.

```
unify :: Type -> Type -> TI ()
unify t1 t2 = do
s <- getSubst
u <- mgu (apply s t1) (apply s t2)
extSubst u
```

There’s one last detail to go over. Why is the function called `mgu`

? That is an acronym standing for “Most General Unifier.” The substitution that it returns is called the unifier of the two types (because it “unifies” them into the same thing). So what does it mean for a unifier to be the most general?

In unification problems, there are multiple possible solutions^{1}. For example, if you unify `a`

with `b`

, the substitution `{a: b}`

would be valid. However, `{a: Int, b: Int}`

would also technically be valid - it does turn both of them into the same type, `Int`

. That’s not really what we want, though. Replacing them both with `Int`

is less general. It’s less general because there are things we could use `b`

for that we couldn’t use `Int`

for, but we could use `b`

for everything that we could use `Int`

for (by replacing `b`

with `Int`

).

The mathematical way to state this is that if `S`

is the most general unifier, then we produce any other valid unifier by composing another substitution with `S`

. Note that there can be multiple unifiers that are considered to be the most general. In the `a`

and `b`

example, replacing `a`

with `b`

is a most general unifier. Replacing `b`

with `a`

is another. Replacing both of them with `c`

would be yet another. All those are equivalent in how general they are because you can get from any of them to any other one of them by applying another substitution.

That wraps up the core logic of type inference. As a breif recap, unification finds a substitution that makes two types into the same thing. A substitution stores the current solution so far by mapping type variables to other types. Type inference walks the expression tree, applying the rules for the current expression, updating the substitution as it goes. Those rules dictate how the type system for the language works.

There is still some boilerplate to cover (mostly to make the monad work) which will have to wait until the next post.

- TODO: Thih section numbers

If there is any valid unifier, then there are an infinite number of valid unifiers (assuming you allow the unifiers to include substitutions for unrelated type variables).↩