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的手册页也只提到了这个警告的非返回语句,而warnings.ml仅仅提到了它Nonreturning_statement.

我熟悉声音的概念,因为它与类型系统有关,但类型本身本身就不健全的想法对我来说似乎很奇怪.

所以我的问题是:

什么是不健全的类型？

当OCaml只发出警告而不是彻底失败时,会出现不健全类型的情况是什么？

有人发布了这个问题,在我写答案时,它被删除了.我相信这个问题非常有趣,值得重新发布.请考虑你可能有人愿意帮助你:-(

Answer 1

如何报告警告21

首先,让我们考虑返回不相关的函数'a:我不是指let id x = x这里的函数,因为它有类型'a -> 'a,返回类型'a与输入相关.我的意思是像raise : exn -> 'a和的功能exit : int -> 'a.

这些返回无关的函数'a被认为永远不会返回.由于类型'a(更准确地说forall 'a. 'a)没有公民.函数唯一能做的就是终止程序(退出或引发异常)或陷入无限循环:let rec loop () = loop ().

当语句的类型是时,会提到警告21 'a.(实际上还有另一个条件,但我只是为了简单起见.)例如,

# 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 crazy : unit -> 'a = "%identity"
let f () = crazy ()  (* val f : unit -> 'a *)
let _ = f (); print_string "3"

对于OCaml类型系统,不可能用不健全的类型区分非返回表达式和表达式.这就是为什么它不能排除不合理的错误.跟踪定义以告诉语句有一个不健全的类型通常是不可能的,并且即使在可能的情况下也要花费很多.