erlang - 为什么Dialyzer无法捕获此简单错误？

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

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

但它会检测到最后一行是

myfun(_) -> other_number.

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

最佳答案

对于“为什么Dialyzer不...”类型的问题，简单的答案是“因为它被设计为总是正确的”或“因为它从不保证它将捕获所有内容或特定内容”。

对于更复杂的答案，您需要进一步指定问题。如果我在模块中编写示例:

-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作为参数来调用这些函数，在这种情况下，规范是“确定的”。

关于erlang - 为什么Dialyzer无法捕获此简单错误？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/36645013/