Type Inference by hand

Обновить

December 2018

Просмотры

292 раз

1

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

(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

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

1 ответы

3

Your proposed solution:

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

would make foo be a function that takes a single argument of type 'x and returns a function that takes a single argument of type ('y -> 'z) and returns a value of type 'z. But you can't call with foo with just one argument, so it's clearly not a function of one argument. It needs to be a function of three arguments. Let's take a closer look at the actual solution. The solution,

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

says that foo is a function that takes three arguments. The first argument has type

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

which means that it's a function that takes an 'x and returns a

'y -> 'z

which is a function that takes a 'y and returns a 'z. That first argument is the function f and, as you described, it has to be able to take x as an argument, and return a (function that can take y as an argument and return a 'z). Now that's just the first argument of foo. foo takes three arguments. The second is x, which has type 'x, and the third is y, which has type 'y. The * in the type of foo is separating the types of the arguments:

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