Вывод типа с взаимной рекурсией - PullRequest
Новая
       74

Вывод типа с взаимной рекурсией

11 голосов
/ 12 октября 2010

Я думал о том, как вывод типов работает в следующей программе OCaml: 

let rec f x = (g x) + 5
and g x = f (x + 5);;

Конечно, программа довольно бесполезна (зацикливание навсегда), но как насчет типов?OCaml говорит: 

val f : int -> int = <fun>
val g : int -> int = <fun>

Это было бы моей интуицией, но как алгоритм определения типа узнает это?

Скажем, алгоритм сначала рассматривает "f": единственное ограничение, которое он может получитьсуществует то, что тип возвращаемого значения "g" должен быть "int", и поэтому его собственный тип возвращаемого значения также является "int".Но он не может определить тип своего аргумента по определению «f».

С другой стороны, если он сначала рассматривает «g», он может видеть, что тип его собственного аргумента должен быть «int».».Но, не рассматривая «f» ранее, он не может знать, что тип возвращаемого значения «g» также является «int».

Что за магия стоит за ним?

Ответы [ 2 ]

8 голосов
/ 13 октября 2010

Вот моя ментальная модель того, что происходит, которая может соответствовать или не соответствовать реальности. 

let rec f x =

Хорошо, на данный момент мы знаем, что f - это функция, которая принимает аргумент x. Таким образом, имеем: 

f: 'a -> 'b
x: 'a

для некоторых 'a и 'b. Далее: 

(g x)

Хорошо, теперь мы знаем, g - это функция, которая может быть применена к x, поэтому мы добавляем 

g: 'a -> 'c

к нашему списку информации. Продолжение ... 

(g x) + 5

Ага, тип возврата g должен быть int, так что теперь мы решили 'c=int. На данный момент мы имеем: 

f: 'a -> 'b
x: 'a
g: 'a -> int

Двигаемся дальше ... 

and g x =

Хорошо, здесь есть другой x, давайте предположим, что вместо исходного кода было y, чтобы сделать вещи более очевидными. То есть давайте перепишем код как 

and g y = f (y + 5);;

Хорошо, мы находимся на 

and g y =

так что теперь наша информация: 

f: 'a -> 'b
x: 'a
g: 'a -> int
y: 'a

, поскольку y является аргументом g ... и мы продолжаем: 

f (y + 5);;

и это говорит нам от y+5, что y имеет тип int, который решает 'a=int. И поскольку это возвращаемое значение g, которое, как мы уже знаем, должно быть int, это решает 'b=int. Это было много за один шаг, если код был 

and g y = 
    let t = y + 5 in
    let r = f t in
    f r;;

тогда первая строка будет показывать y как int, таким образом, решение для 'a, а затем следующая строка скажет, что r имеет тип 'b, а затем последняя строка - возвращаемая g, который решает 'b=int.

8 голосов
/ 12 октября 2010

Скажем, алгоритм сначала рассматривает «f»: единственное ограничение, которое он может получить, это то, что тип возвращаемого значения «g» должен быть «int», и поэтому его собственный тип возвращаемого значения также «int». Но он не может определить тип своего аргумента по определению «f».

Он не может вывести его на конкретный тип, но может что-то вывести. А именно: тип аргумента f должен совпадать с типом аргумента g. Итак, после просмотра f ocaml знает следующее о типах: 

for some (to be determined) 'a:
f: 'a -> int
g: 'a -> int

После просмотра g он знает, что 'a должно быть int.

Более подробно о том, как работает алгоритм вывода типов, вы можете прочитать в Википедии о выводе типа Хиндли-Милнера или в этом блоге , который быть намного дружелюбнее, чем статья в Википедии.

...