Type Inference by Example, Part 3

Inferring types for generic calls

Continuing where we left off in part 2, we’ll now consider calling a generic function:

function map<A, B>(array : Array<A>, body : A => B) : Array<B>

So this is the classic map function that applies a lambda function body to each element of the array and returns a new array with the results. Note that map takes two type parameters, A and B.

Here’s a function that squares each element of an array:

function square(items) {
return map(items, x => x * x);
}

Now, to add in the missing type annotations, we first must instantiate the type for map — that is, create a new copy of the function signature where every type parameter is replaced with a fresh type variable:

function map<$3, $4>(array : Array<$3>, body : $3 => $4) : Array<$4>

While adding the missing type annotations, we make the generics explicit at the call site of map:

function square(items : $1) : $2 {
return map<$3, $4>(items, (x : $5) => x * x);
}

The first parameter of our instantiated map has type Array<$3>, so we get the following constraint:

$1 == Array<$3>

Considering the lambda function, and assuming that * : (Int, Int) => Int, we get the duplicate constraint:

$5 == Int
$5 == Int

And from the return type of * we know that the return type of the lambda must be Int, such that the full type of the lambda becomes $5 => Int. It should be the same type as the second parameter to map, so we get the constraint:

($5 => Int) == ($3 => $4)

From the return statement, we know that the return type of square is the same as the return type of map:

$2 == Array<$4>

Now we have all the constraints:

$1 == Array<$3>
$5 == Int
$5 == Int
($5 => Int) == ($3 => $4)
$2 == Array<$4>

Since ($5 => Int) == ($3 => $4) has the same type constructor => on both sides, we can replace it by two simpler constraints $5 == $3 and Int == $4:

$1 == Array<$3>
$5 == Int
$5 == Int
$5 == $3
Int == $4
$2 == Array<$4>

Unification does this simplification internally — we’ll get to the algorithm in a bit — and yields us the following substitution:

$1 := Array<Int>
$2 := Array<Int>
$3 := Int
$4 := Int
$5 := Int

Applying the substitution to our syntax tree, we get:

function square(items : Array<Int>) : Array<Int> {
return map<Int, Int>(items, (x : Int) => x * x);
}

And we’re done.

It’s about time we look at how this is implemented under the hood. Stay tuned for part 4, where we’ll look at the unification algorithm.

MSc Computer Science, working with functional programming in the industry — github.com/ahnfelt