Deriving expression type in SML

Question

I'm kinda new to sml and i'm trying to understand how to derive the expression type.
I read Deriving type expression in ML and I'm trying to follow what he did to derive my expression, but I can't understand one passage.

The expression I'm trying to derive is:

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

What I'm doing is as follow:

fn x : T1 => fn y : T2 => fn z : T3 => z(z(y x)) : T4

At this point it should be

T2 = T1 -> T5                       //y x
T3 = T5 -> T6                       //z(y x)
T3 = T6 -> T7                       //z(z(y x))

which is where I think I'm doing the mistake.

Also there should be a constraint like

T7 = T4 or T6 = T4.    

I'm not sure nor clear on this point tho.

Thanks in advance for the help.

Answer 1

You have already assigned T4 to z(z(y x)), so we can use it in the last equation.

T3 = T5 -> T6                       //z(y x)
T3 = T6 -> T4                       //z(z(y x))

Since T5 -> T6 = T6 -> T4, it follows that T5 = T6 and T6 = T4.