What substitution should this unification return?

Question

What should be the result of unifying these two types?

1) a -> a
2) Int -> b

Is this the right result?

{ a |-> Int; b |-> a }

Answer 1

According to this article, I believe the correct substitution to return is:

{ a |-> Int; b |-> Int }

With me so far? OK, then it’s time to look at a more advanced case. What if we unify a -> a with int -> c? (We’d see a unification like this if we applied the identity function to an integer, for example. The type variable c is there to capture the resulting type.) As before, we start by unifying the left hand side: a and int. That results in the substitution {a: int}. Here’s the subtle bit: We have to substitute the other a (on the right hand side of the function type) with int before continuing. That’s because when you replace a type variable with something else, you have to replace it everywhere1. So, after unifying the left hand side, the two types become int -> int and int -> c. Now we can unify the right hand side: int and c. That gives the substitution {c: int}. Finally, we can compose the two substitutions and get the result: {a: int, c: int}. Congratulations, you just figured out that applying the identity function to an integer results in an integer!