使用相互递归键入推断

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);; 

好的,所以我们在

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.