Deriving type expression in ML

Question

All,

I want to derive the type expression for the function below in ML:

fun f x y z = y (x z)

Now I know typing the same would generate the type expression. But I wish to derive these values by hand.

Also, please mention the general steps to follow when deriving type expressions.

Answer 1

I'm going to try to do this in the most mechanical way possible, exactly as the implementation in most compilers would.

Let's break it down:

fun f x y z = y (x z)

This is basically sugar for:

val f = fn x => fn y => fn z => y (x z)

Let's add some meta-syntactic type variables (these are not real SML-types, just place holders for this example's sake):

val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T5

OK, so we can start generating a system of constraints from this. T5 is the eventual return type of f. For the moment, we're going to just call the eventual type of this whole function "TX" - some fresh, unknown type variable.

So the thing that is going to be generating constraints in the example you've given is function application. It tells us about the types of things in the expression. In fact, it's the only information we have!

So what do the applications tell us?

Ignoring the type variables we assigned above, let's just look at the body of the function:

y (x z)

z is not applied to anything, so we're going to just look up what the type variable we assigned to it was earlier (T4) and use that as its type.

x is applied to z, but we don't know its return type yet, so let's generate a fresh type variable for that and use the type we assigned x (T2) earlier to create a constraint:

T2 = T4 -> T7

y is applied to the result of (x z), which we just called T7. Once again, we don't know the return type of y yet, so we'll just give it a fresh variable:

T3 = T7 -> T8

We also know that the return type of y is the return type for the whole body of the function, we we called "T5" earlier, so we add the constraint:

T5 = T8

For compactness, I'm going to kludge this a little and add a constraint for TX based on the fact that there are functions being returned by functions. This is derivable by exactly the same method, except it's a little more complex. Hopefully you can do this yourself as an exercise if you're not convinced that we would eventually end up with this constraint:

TX = T2 -> T3 -> T4 -> T5

Now we collect all the constraints:

val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T5
TX = T2 -> T3 -> T4 -> T5
T2 = T4 -> T7
T3 = T7 -> T8
T5 = T8

We start to solve this system of equations by substituting left hand sides with right hand sides in the system of constraints, as well as in the original expression, starting from the last constraint and working our way to the top.

val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T8
TX = T2 -> T3 -> T4 -> T8
T2 = T4 -> T7
T3 = T7 -> T8

val f : TX = fn (x : T2) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8
TX = T2 -> (T7 -> T8) -> T4 -> T8
T2 = T4 -> T7

val f : TX = fn (x : T4 -> T7) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8
TX = (T4 -> T7) -> (T7 -> T8) -> T4 -> T8

val f : (T4 -> T7) -> (T7 -> T8) -> T4 -> T8 = fn (x : T4 -> T7) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8

OK, so this looks horrible at the moment. We don't really need the whole body of the expression sitting around at the moment - it was just there to provide some clarity in the explanation. Basically in the symbol table we would have something like this:

val f : (T4 -> T7) -> (T7 -> T8) -> T4 -> T8

The last step is to generalise all the type variables that are left over into the more familiar polymorphic types that we know and love. Basically this is just a pass, replacing the first unbound type variable with 'a, the second with 'b and so on.

val f : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

Which I'm pretty sure you'll find is the type that your SML compiler will suggest for that term too. I did this by hand and from memory, so apologies if I've botched something somewhere :p

I found it difficult to find a good explanation of this inference and type constraint process. I used two books to learn it - 'Modern Compiler Implementation in ML' by Andrew Appel, and 'Types and Programming Languages' by Pierce. Neither one was independently completely illuminating for me, but between the two of them I figured it out.

Answer 2

To determine the type of something you need to look at every place where it is used. For example if you see val h = hd l, you know that l is a list (because hd takes a list as an argument) and you also know that the type of h is the type that l is a list of. So let's say the type of h is a and the type of l is a list (where a is a placeholder). Now if you see val h2 = h*2, you know that h and h2 are ints, because 2 is an int, you can multiply an int with another int and the result of multiplying two ints is an int. Since we previously said the type of h is a this means that a is int, so the type of l is int list.

So let's tackle your function:

Let's consider the expressions in the order in which they are evaluated: First you do x z, i.e. you apply x to z. That means x is a function, so it has the type a -> b. Since z is given as an argument to the function it has to have the type a. The type of x z is therefor b because that is the result type of x.

Now y is called with the result of x z. This means y is also a function and its argument type is the result type of x, which is b. So y has the type b -> c. Again the type of the expression y (x z) is therefor c because that is the result type of y.

Since those are all the expressions in the function, we cannot restrict the types any further and therefor the most general types for x, y and z are 'a -> 'b, 'b -> 'c and 'a respectively and the type of the whole expression is 'c.

This means the overall type of f is ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

For an explanation of how types are inferred programatically read about Hindley–Milner type inference.