我一直在考虑类型推断如何在以下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”。
它背后的魔力是什么？
假设算法首先考虑“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型推论 要么 这篇博文，这似乎比维基百科文章更友好。
这是我发生的事情的心理模型，它可能与现实相匹配，也可能不匹配。
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。