[Haskell-cafe] Q: haskell type inference algorithm paper

[Chris Warburton]

Let's try explicitly unifying the types in your map example. We'll
assume that map already has the following explicit type:

data List a = Nil | Cons a (List a)

type Function a b = a -> b

map :: Function (Function a b) (Function (List a) (List b))

I've defined new "List" and "Function" types since the "[]" and "->" may
cause confusion.

The "a" and "b" are placeholders; they give us *constraints* by telling
us which types must be the same, but they don't tell us what those types
actually are. These placeholders can be re-used in different type
declarations, but I'll use different letters to prevent any confusion.

Now let's look at the arguments given to map in your example. First the
identity function, written like this in Haskell, with some unknown type:

(\x -> x) :: ?

The simple placeholder "?" is my way of saying 'we don't know yet'. In
fact, we already know that the value is a function, so we can write that
down:

(\x -> x) :: Function ? ?

Now we can calculate the output type by *assuming* that the input type
holds. In other words, to calculate the type of the output value we need
to assume that we've been given an input value. Here we will assume that
we've been given a value of some type "c":

x :: c

Now we can calculate the type of the output expression:

x :: ?

Since we assumed that x :: c, we can immediately write down the type of
the output, since it's the same:

x :: c

Hence we've found that the output type happens to be the same as the
input type:

(\x -> x) :: Function c c

Now let's look at the other argument:

(Cons 1 (Cons 2 (Cons 3 Nil))) :: ?

This is [1,2,3] written using my List type. We know that Cons gives us a
List, so we can write that down:

(Cons 1 (Cons 2 (Cons 3 Nil))) :: List ?

Now we need to know the types of "1", "2" and "3". Haskell treats
numbers in a special way, using the "Num" typeclass, but that will just
complicate things, so I'll pretend that they're Ints:

(Cons 1 (Cons 2 (Cons 3 Nil))) :: List Int

Notice that this type has no placeholders, it is 'concrete'.

Now let's look at the full example:

map (\x -> x) (Cons 1 (Cons 2 (Cons 3 Nil)))

We can only apply a function to arguments of the correct type, which
means that the following equations must be satisfied:

     Function a b = Function c c
           List a = List Int

We can see that the 'top level' constraints are OK: we have a Function
type equal to a Function type and a List type equal to a List type. Next
we need to check their arguments (known as "type arguments"):

           a = c
           b = c
           a = Int

This looks OK, since we don't have any nonsense like Int = Bool or
anything. However, we still haven't worked out what the types actually
are. It looks like this is where typed clojure gives up:

> We take the simple approach that all the the arguments' types must be
> determined before calculation of any missing type arguments.

In Haskell we can go a bit further by rearranging these equations using
substitution. We can see that the first and third equations both use
"a", hence we can substitute one for the other:

         Int = c

This uses "c" and so does the middle equation, so we can do another
substitution:

           b = Int

Now we have concrete types for all of our placeholders, specifically:

           a = Int
           b = Int
           c = Int

Hence we can substitute these back into the type of our map expression:

Function (Function Int Int) (Function (List Int) (List Int))

Or, with the conventional notation for types:

(Int -> Int) -> [Int] -> [Int]

The extra step of solving simultaneous equations to get the type
arguments is the reason Haskell can infer this type and typed clojure
cannot.

Regards,
Chris