erlang - 为什么 Dialyzer 无法捕获这个简单的错误？

Question

Dialyzer 不会发出此函数返回类型不一致的信号:

-spec myfun(integer()) -> zero | one.
myfun(0) -> zero;
myfun(1) -> one;
myfun(2) -> other_number.

但它检测到最后一行是

myfun(_) -> other_number.

为什么会这样呢？我相信以上应该是一个非常简单的案例。

谢谢

Answer 1

对“为什么 Dialyzer 不......”类型的问题的简单回答是“因为它被设计为始终正确”或“因为它从不 promise 它会捕获所有内容或任何特定内容”。

<小时/>

对于更复杂的答案，您需要进一步具体说明您的问题。如果我将你的示例写在模块中:

-module(bar).

-export([myfun1/1, myfun2/1]).

-spec myfun1(integer()) -> zero | one.

myfun1(0) -> zero;
myfun1(1) -> one;
myfun1(2) -> other_number.

-spec myfun2(integer()) -> zero | one.

myfun2(0) -> zero;
myfun2(1) -> one;
myfun2(_) -> other_number.

并透析它:

$ dialyzer bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.64s
done (passed successfully)

...这两种差异均未“检测到”，因为两者都不是“错误”。只是代码在某些方面比规范更通用(可以返回额外的值)，并且在某些方面更具限制性(对于版本 1，无法处理每个整数)。

第二个版本的问题可以通过-Woverspecs找到:

$ dialyzer -Woverspecs bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
 done in 0m0.58s
done (warnings were emitted)

该警告准确地解释了规范比代码更具限制性。

这两个问题也可以通过极其不寻常的 -Wspecdiffs 来检测:

$ dialyzer -Wspecdiffs bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
bar.erl:5: Type specification bar:myfun1(integer()) -> 'zero' | 'one' is not equal to the success typing: bar:myfun1(0 | 1 | 2) -> 'one' | 'other_number' | 'zero'
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
 done in 0m0.61s
done (warnings were emitted)

不鼓励使用 -Woverspecs 和 -Wspecdiffs 操作模式，因为 Dialyzer 的类型分析可以并且将会概括类型，因此“以更严格的方式指定某些内容”可以是泛化的结果。

也可能出现这样的情况:您希望仅使用 0 和 1 作为参数来调用这些函数，在这种情况下，规范为“ok”。