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

Я думал о том, как работает вывод типа в следующей программе 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".

Какова его магия?

Ответ 1

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

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

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

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

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

Ответ 2

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

let rec f x =

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

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

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

(g x)

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

g: 'a -> 'c

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

(g x) + 5

Aha, возвращаемый тип 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, а затем конечная строка - это возврат of g, который решает 'b=int.