OCaml 的 rectype 推断

Question

一边玩-rectypes在某些时候选择 OCaml 我只是迷路了。

这个表达式几乎可以打字:

# fun x -> x x;;
- : ('a -> 'b as 'a) -> 'b = <fun>

但是这里 OCaml 陷入了无限循环:

# (fun x -> x x) (fun x -> x x);;
  C-c C-cInterrupted.

好吧，我能理解，递归类型系统是一件相当困难的事情。但首先，我真的很想知道这个表达式的类型，它是否可以打字，其次，在这种情况下，我不明白 OCaml 如何仍然可以输入:

# fun _ -> (fun x -> x x) (fun x -> x x);;
- : 'a -> 'b = <fun>

那么，有人可以详细说明一下这个话题吗？

Answer 1

让我们首先尝试评估您的表达式。

# (fun x -> x x) (fun x -> x x);;
# let x = (fun x -> x x) in x x;; (* applying the function on the left *)
# (fun x -> x x) (fun x -> x x);; (* inlining the let-binding *)
(* We came back to our original state, infinite loop *)

所以无限循环不是来自打字系统，而是来自你给它的表达式的语义。

您可以使用 ocamlc -i 获取表达式的类型，而无需对其进行评估。

$ echo 'let x = (fun x -> x x) (fun x -> x x)' > rectypes.ml
$ ocamlc -i -rectypes rectypes.ml                                                                                                                                                                                                           
val x : 'a

所以在这里，你创建了一个 'a 类型的值(这通常意味着“这个表达式永远不会返回”)。

请注意，您可以在不使用 rectypes 的情况下执行相同的技巧:

# let x =
   let rec f () = f () in
   f ();;

正如你现在所理解的，你的最后一段代码接受任何参数并且永远不会返回，因此 'a -> 'b类型。