ocaml - OCaml的Rectype推断

在某些时候使用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>

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

最佳答案

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

# (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类型。