OCaml-什么是声音不好的类型? [英] OCaml - What is an unsound type?

问题描述

最近我收到了代码

Recently I was given the code

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

我对这个具有功能的部分应用程序完全满意 类型exn list -> int的值，以及它产生警告的事实 不足为奇.但是，我不确定警告的那一半 意思是:

I'm completely fine with this partial application having a functional value of type exn list -> int, and the fact it yields a warning isn't surprising. I am, however, not certain what half of the warning means:

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

在不是该警告的地方，我实际上找不到任何参考 不归还声明的结果.即使是ocamlc的手册页 提到此警告的非返回语句，以及warnings.ml 简称为Nonreturning_statement.

I can't actually find any reference to this warning where it isn't the result of a non-returning statement. Even the man page for ocamlc only mentions non-returning statements for this warning, and warnings.ml refers to it merely as Nonreturning_statement.

我熟悉与类型有关的稳健性概念 系统，但类型本身本质上不健全的想法似乎 对我来说很奇怪.

I am familiar with the concept of soundness as it relates to type systems, but the idea of a type itself being inherently unsound seems odd to me.

所以我的问题是:

什么是不正确的类型?

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

What's a situation in which an unsound type would arise when OCaml would only issue a warning rather than failing hard outright?

有人发布了这个问题，而当我写一个答案时，它被删除了.我认为这个问题非常有趣，值得重新发布.请考虑您可能会有愿意帮助您的人:-(

Someone has posted this question, and while I was writing an answer, it was deleted. I believe the question is very interesting and worth for reposting. Please consider you may have someone who is willing to help you :-(

推荐答案

如何报告警告21

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

How Warning 21 is reported

First, let's think of functions which returns unrelated 'a: I do not mean function like let id x = x here since it has type 'a -> 'a and the return type 'a relates with the input. I mean functions like raise : exn -> 'a and exit : int -> 'a.

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

These functions return unrelated 'a are considered never returning. Since the type 'a (more precisely forall 'a. 'a) has no citizen. Only thing the functions can do are terminating the program (exit or raising an exception) or falling into an infinite loop: let rec loop () = loop ().

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

Warning 21 is mentioned when the type of a statement is 'a. (Actually there is another condition but I just skip for simplicity.) For example,

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

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

This is the main purpose of warning 21. Then what is the latter half?

警告21.在这种情况下，如警告消息所示，该语句的类型不正确.

Warning 21 can be reported even if the statement returns something actually. In this case, as the warning message suggests the statement has a unsound type.

为什么声音不好?由于表达式确实返回类型为forall 'a. 'a的值，该值没有任何公民.它打破了OCaml所依赖的类型理论的基础.

Why unsound? Since the expression does return a value of type forall 'a. 'a, which has no citizen. It breaks the basis of the type theory OCaml depends on.

在OCaml中，有 种方法可以编写具有这种不健全类型的表达式:

In OCaml, there are several ways to write an expression with such an unsound type:

使用Obj.magic.它是螺丝类型系统，因此您可以编写类型为'a的表达式，该表达式返回:

Use of Obj.magic. It screws type system therefore you can write an expression of type 'a which returns:

(Obj.magic 1); print_string "2"

使用external.与Obj.magic相同，您可以为任意外部值和函数赋予任意类型:

Use of external. Same as Obj.magic you can give arbitrary type to any external values and functions:

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

对于OCaml类型系统，无法区分非返回表达式和具有不正确类型的表达式.这就是为什么它不能排除不正确的东西作为错误的原因.跟踪定义以告诉语句是否具有不正确的类型通常也是不可能的，即使可能也要花费很多.

For OCaml type system, it is impossible to distinguish non-returning expressions and expressions with unsound types. This is why it cannot rule out unsound things as errors. Tracking the definitions to tell a statement has an unsound type or not is generally impossible either and costs a lot even when possible.

这篇关于OCaml-什么是声音不好的类型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！