Why does Dialyzer not catch this simple error?

Question

Dialyzer does not signal the inconsistency in the return type of this function:

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

but it detects in the case of the last line being

myfun(_) -> other_number.

Why is this so? I believe the above should be a very simple case.

Thanks

score 4 · Answer 1 · answered Apr 15 '16 at 14:06

The easy answer to questions of type "why Dialyzer doesn't..." is "because it has been designed to be always correct" or "because it never promises that it will catch everything or anything specific".

For the more complex answer, you need to specify your question further. If I write your example in a module:

-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.

And Dialyze it:

$ 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)

... neither discrepancy is 'detected', cause neither is an "error". It's just the case that the code is in some ways more generic (can return extra values) and in some ways more restrictive (cannot handle every integer, for version 1) than the spec.

The second version's problem can be found with -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)

The warning explains exactly that the spec is more restrictive than the code.

Both problems can also be detected by the extremely unusual -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)

Neither -Woverspecs nor -Wspecdiffs mode of operation is encouraged, as Dialyzer's type analysis can and will generalize types, so "something being specified in a more restrictive way" can be the result of generalization.

It can also be the case that you intend these functions to be called only with 0 and 1 as arguments, in which case the spec is 'ok'.

Can you explain "as Dialyzer's type analysis can and will generalize types ..." more clearly, perhaps with an example? — mljrg, Apr 15 '16 at 15:10
Example1: Say that you have another function call one of yours, with an argument that will always be "<=0". Dialyzer will not always infer that the result of such a call can only be `'zero'`. Example2: Say that you have a function that works for all even numbers. Dialyzer will infer that it works for all integers. And so on... — aronisstav, Apr 15 '16 at 15:50
So, if the options `-Woverspecs` and `-Wspecdiffs` can be used to detect (directly or indirectly) the presence of a potential problem, why is their use discouraged? I think you either remove these options, or people will tend to used them ... — mljrg, Apr 15 '16 at 16:03
As I explained, there is the possibility that a specification is found to be "too tight" (i.e.. too restrictive, overspecified) only due to Dialyzer doing generalizations during its own inference. So using `-Woverspecs` can result in warnings that are wrong and can be safely ignored. Dialyzer tries hard to reduce such noise. — aronisstav, Apr 15 '16 at 16:15
So, by not encouraging the use of those options you are avoiding the developer to be overloaded with missleading warnings. I suppose those warnings could be a waste of time in the case of big projects, hence the recommendation to not used them. Is this right? — mljrg, Apr 15 '16 at 16:42
I think there is a misunderstanding what "not encouraged" means: not encouraged as default setting on each run. But you can do occasional runs with unusual flags to see if you need to fix something in you specs. Since it reports a lot of noise which you have to chcheck manually you don't do this on every run — Peer Stritzinger, Apr 17 '16 at 08:43
Thanks for the explanation @PeerStritzinger. That's what I also had in mind. — aronisstav, Apr 18 '16 at 08:36

Why does Dialyzer not catch this simple error?

1 Answers1