Тип вывода вручную

Question

У меня есть тест завтра, и одна из тем, которую мы рассматриваем, - это вывод типа. Я просматриваю задание, которое мы сделали, вместе с ответами, которые нам дали за это. Однако, похоже, я не могу следовать. Вопрос, который я не могу подключить ответ для этой функции:

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

Теперь, чтобы сделать вывод типов, во-первых, создавать типы:

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

Тогда вы делаете ограничения. Глядя на первый блок, где вы посылаете x в f дает:

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

Чтобы включить у сейчас (z будучи еще один новый тип с результатом функции w):

'w = 'y -> 'z 

Это будет, следовательно, сделать 'r = 'z ('z - это то, что будет возвращено). Наконец, где я смущен, это то, где все собрано. Для меня это стало бы:

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

, который можно переписать в виде:

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

Однако полученный ответ включает в себя еще два вида ('x и 'y):

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

Может кто-то объясняет мне, почему они добавлены, и когда использовать *?

Answer 1

предложил Ваше решение:

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

бы foo функция, которая принимает один аргумент типа 'x и возвращает функцию, которая принимает один аргумент типа ('y -> 'z) и возвращает значение типа 'z. Но вы не можете позвонить с foo только одним аргументом, поэтому он явно не является функцией одного аргумента. Он должен быть функцией трех аргументов. Давайте подробнее рассмотрим фактическое решение. Решение,

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

говорит, что foo это функция, которая принимает три аргумента. Первый аргумент имеет тип

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

, что означает, что это функция, которая принимает 'x и возвращает

'y -> 'z 

, которая является функцией, которая принимает 'y и возвращает 'z. Этот первый аргумент является функцией f и, как вы описали, он должен принимать в качестве аргумента x и возвращать функцию (функцию, которая может принимать y в качестве аргумента и возвращает 'z). Теперь это только первый аргумент foo. foo принимает три аргумента.Второй - x, который имеет тип 'x, а третий - y, который имеет тип 'y. * в типе foo отделяющий типы аргументов:

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