Search code examples
smlsmlnj

Understanding an SML type fn (f,g,x) => g(f(x)) or similar

Ok, sorry in advance this probably is repost but I spent a good 30 minutes searching stackoverflow and couldn't find something similar enough to understand. Basically, I don't understand why 

fn (f,g,x) => g(f(x))

gives the type 

(’a -> ’b)*(’b -> ’c)*’a -> ’c

from my understanding it should start with

'a * 'b * 'c...

But this is evidently wrong.

Thanks in advance.

Solution

  • Indeed, it all starts with 'a * 'b * 'c, where f : 'a, g : 'b, x : 'c but then the type inference mechanism sees that f is applied x, so so it concludes that the function f : 'd -> 'e (i.e. 'b = 'd -> 'e). Also, the type of x must comply with f's input type, thus 'd = 'c and f : 'c -> 'e.

    Furthermore, g is a function as well, so 'b = 'y -> 'z and it's easy to see that f's output type must be equal to g's input type, which gives us the following type equation 'y = 'e.

    We have x : 'c, f : 'c -> 'e, g : 'e -> 'z. Concrete variable names don't matter and we can rename them like so:

    'c -> 'a
'e -> 'b
'z -> 'c

    That gives as x : 'a, f : 'a -> 'b, and g : 'b -> 'c

    Since fn (f,g,x) takes a triple as its input, it must have the type 

    <type of f> * <type of g> * <type of x> -> <output type of g>

    Expanding the above semi-formal description we get

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