使用相互递归键入推断-Java 学习之路

我一直在考虑类型推断如何在以下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” .

它背后的魔力是什么？

2 回答

8
假设算法首先考虑“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的维基百科文章，该文章似乎比维基百科的文章更友好 .
回复于 2024-05-13T21:27:29+08:00
8
这是我发生的事情的心理模型，可能与现实相匹配，也可能不相符 .
```
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 .
回复于 2024-05-13T21:27:29+08:00

使用相互递归键入推断

2 回答

相关问题