Type Inference by hand

Question

I've got a test tomorrow, and one of the topics we're covering is type inference. I'm reviewing an assignment we did, along with the answers we were given for it. However, I can't seem to follow. A question that I can't seem to connect the answer to is for this function:

(define foo (lambda (f x y) ((f x) y)))

Now to do the type inferencing, first, create types:

f : 'f  
x : 'x  
y : 'y  
return = 'r

Then you do the constraints. Looking at the first chunk where you send x into f gives:

'f = 'x -> 'w (w being a new type representing the result of that function).

To include the y now (z being another new type with the result of the function w):

'w = 'y -> 'z 

This would therefore make 'r = 'z ('z is what would be returned). Lastly, where I'm confused about, is where it's all put together. To me, it would become:

val foo = fn: 'x -> 'w -> 'z

which can be rewritten as:

val foo = fn: 'x -> ('y -> 'z) -> 'z

However, the answer given includes two more types ('x and 'y):

val foo = fn: 'x -> ('y -> 'z) * 'x * 'y -> 'z

Can someone explain to me why those are added, and when to use *?

Answer 1

Your proposed solution:

val foo = fn: 'x -> ('y -> 'z) -> 'z

would make foo be a function that takes a single argument of type 'x and returns a function that takes a single argument of type ('y -> 'z) and returns a value of type 'z. But you can't call with foo with just one argument, so it's clearly not a function of one argument. It needs to be a function of three arguments. Let's take a closer look at the actual solution. The solution,

val foo = fn: 'x -> ('y -> 'z) * 'x  * 'y  -> 'z
              ----------------   ---   ---    -----------
                    1st          2nd   3rd    result type

says that foo is a function that takes three arguments. The first argument has type

'x -> ('y -> 'z)

which means that it's a function that takes an 'x and returns a

'y -> 'z

which is a function that takes a 'y and returns a 'z. That first argument is the function f and, as you described, it has to be able to take x as an argument, and return a (function that can take y as an argument and return a 'z). Now that's just the first argument of foo. foo takes three arguments. The second is x, which has type 'x, and the third is y, which has type 'y. The * in the type of foo is separating the types of the arguments:

val foo = fn: 'x -> ('y -> 'z) * 'x * 'y -> 'z.
              ----------------   --   --
                    f             x    y