具有相互递归的类型推断答案

【问题标题】：Type inference with mutual recursion具有相互递归的类型推断
【发布时间】：2011-04-24 05:56:39
【问题描述】：

我一直在思考类型推断在以下 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 type inference 或 this blog post 的 Wikipedia 文章，这似乎比 Wikipedia 文章更友好。

【讨论】：

【解决方案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);;

好的，所以我们在

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。

【讨论】：