OCaml - 什么是不安全类型？

Question

最近我收到了这段代码。

List.fold_left (fun acc x -> raise x ; acc) 3

我完全赞成这个偏应用程序具有类型为 exn list -> int 的函数值，它产生警告并不奇怪。然而，我不确定警告的一半含义是什么：

Warning 21: this statement never returns (or has an unsound type.)

我实际上找不到任何关于此警告的参考，除非是非返回语句的结果。即使ocamlc的man页面也仅提到此警告的非返回语句，并且warnings.ml仅将其称为Nonreturning_statement。

我熟悉与类型系统相关的完整性的概念，但一个类型本身本质上是不完整的这个想法对我来说很奇怪。

所以我的问题是：

什么是不完整的类型？

在仅发出警告而不是直接失败的情况下，OCaml中会出现什么样的不完整类型？

- camlspotter

---

我相信这个问题被删除是因为它是 https://dev59.com/BYzda4cB1Zd3GeqPqsWK 的重复，其中警告是由使用具有无约束结果类型的外部（js_of_ocaml）函数引起的 - 就像您在下面的答案中所述。我怀疑提问者就是刚刚给我接受的答案点了+1的人。当然，那里的重点略有不同。 - antron

我是那个提问/删除的人；我刚刚注意到了这一点。@antron所说的就是我删除它的原因。是的，那个+1就是我加的。;) - Will

Answer 1

如何报告警告21

首先，让我们考虑返回不相关的'a类型的函数：我并不是指像let id x = x这样的函数，因为它的类型为'a -> 'a，返回类型'a与输入相关。我指的是像raise: exn ->'a和exit: int ->'a这样的函数。

这些返回不相关'a类型的函数被认为是永远不会返回的。因为类型'a（更确切地说是forall 'a.'a）没有任何值。这些函数能做的事情只有终止程序（使用exit或引发异常）或进入无限循环：let rec loop() = loop()。

当语句的类型为'a时，就会提到警告21。（实际上还有另一个条件，但为了简洁起见，我跳过了。）例如，

# loop (); print_string "end of the infinite loop";;
Warning 21: this statement never returns (or has an unsound type.)

这是警告21的主要目的。那么后半部分是什么？

“不安全的类型”

即使语句实际上返回某些东西，警告21也可能被报告。在这种情况下，与警告信息所示一样，语句具有不安全的类型。

为什么是不安全的？因为该表达式返回forall 'a. 'a类型的值，这个类型没有对应的实例。它破坏了OCaml依赖的类型理论基础。

在OCaml中，有几种写出这种不安全类型表达式的方式：

使用Obj.magic。它破坏了类型系统，因此你可以编写一个类型为'a的表达式，它返回：

(Obj.magic 1); print_string "2"

使用external。和 Obj.magic 一样，你可以给任何外部值和函数指定任意类型：

使用external。和Obj.magic类似，您可以为任何外部值和函数指定任意类型：

external crazy : unit -> 'a = "%identity"
let f () = crazy ()  (* val f : unit -> 'a *)
let _ = f (); print_string "3"

对于OCaml类型系统来说，它无法区分非返回表达式和具有不合规类型的表达式。这就是为什么它不能将不合规的内容作为错误排除的原因。即使可能，追踪定义以确定语句是否具有不合规类型也通常是不可能的，甚至会耗费大量成本。

- camlspotter

---

不错的回答。为了完整起见，您可能需要提到反序列化（input_value和Marshal.from_*）作为不安全的函数。（事实上，我认为它们比Obj.magic更有用，特别是对于那些不是类型系统专家的人来说）。 - Virgile