Понимание типа SML fn (f, g, x) => g (f (x)) или аналогичного

Question

Хорошо, извините заранее, это, вероятно, repost, но я потратил 30 минут на поиск stackoverflow и не смог найти что-то достаточно подобный, чтобы понять. В принципе, я не понимаю, почему

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

дает тип

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

от моего понимания он должен начать с

'a * 'b * 'c... 

Но это, очевидно, не так.

Заранее спасибо.

Answer 1

В самом деле, все начинается с 'a * 'b * 'c, где f : 'a, g : 'b, x : 'c но тогда механизм вывода типа видит, что f применяется x, поэтому так делает вывод, что функция f : 'd -> 'e (т.е. 'b = 'd -> 'e). Кроме того, тип x должен соответствовать входному типу f, таким образом, 'd = 'c и f : 'c -> 'e.

Кроме того, g является функцией, а также, так 'b = 'y -> 'z и это легко видеть, что f «тип выхода s должен быть равен g» тип входа s, что дает нам уравнение следующего типа 'y = 'e.

У нас есть x : 'c, f : 'c -> 'e, g : 'e -> 'z. Конкретные имена переменных не имеет значения, и мы можем переименовать их так:

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

Это дает в x : 'a, f : 'a -> 'b и g : 'b -> 'c

С fn (f,g,x) занимает тройка в качестве входных данных, он должен иметь тип

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

Расширение выше полуофициальное описания мы получаем

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