recursion - 相互递归的类型推断

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

Say the algorithm considers "f" first: the only constraint it can get there is that the return type of "g" must be "int", and therefore its own return type is also "int". But it cannot infer the type of its argument by the definition of "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 ，这似乎比维基百科的文章友好得多。