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¹. 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.