An appetizer for those preparing to delve into the depths of type inference.

Consider the following function that takes an argument ‘x’ of some type and returns the result of applying the addition operator on it:

f (x) : x + x

We want to find out the type of x and the type of f (which is the type of the value returned by f). The first step is to assign placeholder types to each expression:

Expression      Type
----------      ----
x                tx
x + x            t0
f (x) : x + x    tf

Next, we generate some equations based on the above types assignments:

1. t0 = tx + tx
2. tf = t0

We can now solve these equations systematically. This process is called unification. The first equation is easy to solve, as our simple language specification dictates that the addition operator can be applied only to integers. (This is true also for OCaml, a much more complicated language that employs type inference!):

t0 = tx + tx
   = (int + int) -> int
hence,
tx = int

Please take note of how we replaced parts of the equation with information we already had. This is called substitution. As the type of the second equation is the same as the first, we have now inferred the types of the argument of f and its return value. So we can write down the type signature of the function f as:

int -> int