OCaml的直肠推断

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(通常意味着"这个表达式永远不会返回").

请注意,您可以在不使用rectype的情况下执行相同的操作:

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

正如您现在可以理解的那样,您的最后一段代码接受任何参数并且永远不会返回,因此'a -> 'b类型.