OCaml 的 rectype 推断答案

【问题标题】：OCaml's rectype inferenceOCaml 的 rectype 推断
【发布时间】：2018-05-24 13:27:26
【问题描述】：

在使用 OCaml 的 -rectypes 选项时，我迷路了。

这个表达式非常适合打字：

# 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>

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

【问题讨论】：

OCaml 不仅对您提供给顶层的条款进行类型检查，它还执行它们。这里的无限循环在执行中。
是的。找到不同术语类型的最简单方法可能是将它们包装在 lazy 中，并忽略结果类型的 lazy_t 部分。
在 emacs+merlin 上，C-c C-t 非常有用（虽然我不知道 merlin 处理 rectype 的能力如何）。
另外，在旁注中。除非您非常熟悉打字系统，否则强烈建议不要在生产代码中使用-rectypes。
@PatJ 是的，我知道，就像我说的，这只是为了好玩

标签： ocaml

【解决方案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 类型。

【讨论】：