← back

Type of compose (midterm 2012 Problem 1A)

1 November 2015

Question

I'm having trouble understanding why the type inferred for this statement fun f g x -> f (g x)

would be this...

('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>
                            ^^^^

instead of this ...

('a -> 'b) -> ('c -> 'a)  -> 'a -> 'b = <fun>
                            ^^^^^

I gathered that

variable x -> 'c

function f:

input = g x -> 'a
output = f g x -> 'b

function g:

input = x -> 'c
output = g x -> 'a

f ( g x):

input = g x -> 'a          ( According to the solution, this should be 'c ? I'm not sure why... does the parenthesis change anything ? )
        ^^^^^^^^^^^
output = f g x  -> 'b

Breaking down the function to this f g x -> g x -> f g x I got this ('a -> 'b) -> ('c -> 'a) -> 'a -> 'b = <fun>

Could anyone lend a little hint as to why this is wrong ?

Answer

tl;dr

(g x) : 'a

is the type of the result of applying g to x. But the type of x itself is 'c.

Type inference in ML works like this:

First, you have a function

fun f g x -> f (g x)

the type of the lambda, say Tlam0, is

Tlam0 == Tf -> Tg -> Tx -> Tbody

stepping into the body, we find that it is the result of f is applied to something, so f must be a function:

TBody == <app f ??> == Tfo

Tf == Tfi -> Tfo

Next, look at the thing applied to f

Tfi == <app g ??> == Tgo

Because g is applied to something, g is a function

Tg == Tgi -> Tgo

Now examine the type of the argument to g, which is just the x we passed in as an argument to the lambda.

Tx == Tx

Tgi == Tx

And we're done examining the whole body expression.

Now substitute everything back:

Tx == Tx

Tgi == Tx

Tg == Tgi -> Tgo == Tx -> Tgo

Tfi = Tgo

Tf == Tfi -> Tfo == Tgo -> Tfo

Tbody == Tfo

----------------------------

Tlam0 == Tf -> Tg -> Tx -> Tbody

      == (Tgo -> Tfo) -> (Tx -> Tgo) -> Tx -> Tfo

Now just rename all the placeholders to ABC's

Tx == a

Tg == a -> b

Tf == b -> c

Tbody == c

----------------------------

Tlam0 == Tf -> Tg -> Tx -> Tbody

      == (b -> c) -> (a -> b) -> a -> c

Which by alpha-conversion is equivalent to the inferred type of

('a -> 'b) -> ('c -> 'a) -> 'c -> 'b

(i.e. if you just picked different characters.)