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

Question

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

Какая у него магия?

Answer 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 type inference или this blog post, что кажется намного более дружественным, чем статья Википедии.

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