相互递归的类型推断

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 类型推断 或 这篇博文，看起来比维基百科的文章友好得多。

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 

啊哈，g的返回类型必须是int，所以现在我们已经解决了'c=int。此时我们有：

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

继续...

and g x =

好吧，这里有一个不同的 x，让我们假设原始代码有 y，以使事情更加明显。也就是说，让我们将代码重写为

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

“Ok”，现在

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。