[erlang-questions] Dialyzer questions

[Prashanth Mundkur]

Kostis Sagonas wrote:

> Prashanth Mundkur wrote:
> > We've recently been getting the upcoming release of Disco to go through 
> > the Dialyzer wringer, and it has been a very useful exercise.  Thanks to 
> > Kostis' helpful wielding of the cluebat at the SF Erlang Factory!
> > 
> > We are trying to understand the following output (I hope the inline code 
> > pasting below comes out readable):
> 
> You already figured out some answers to your questions, but let me also 
> reply to them for completeness and hopefully also for more explanations.
> 
> > $ cat dial.erl
> > -module(dial).
> > -export([abort/2, extract/2,
> >          diskspace/1, monitor_diskspace/2, refresh_tags/1, 
> > monitor_launch/0]).
> > 
> > % We have helper functions like this:
> > abort(Msg, Code) ->
> >     error_logger:warning_report(Msg),
> >     exit(Code).
> > % which give rise to the following dialyzer message:
> > %
> > %   Function abort/2 only terminates with explicit exception
> > % How do we interpret this message?
> 
> First of all note that you do not get this warning by default. You only 
> get this warning because you explicitly enabled the -Werror_handling
> option.  I quote from the manual:
> 
>    -Werror_handling ***
>       Include warnings for functions
>       that only return by means of an exception.
> 
> You can suppress this warning by adding a spec of the form:
> 
>     -spec abort(some_type(), some_other_type()) -> no_return().
> 
> for this function, which will notify dialyzer that it is indeed your 
> intention that this function will never return a value
> 
> 
> > % Even with a plt that includes stdlib, there is no warning for the
> > % following code:
> > -spec extract(binary(), nonempty_string()) -> 'ok'.
> > extract(Pack, Dir) ->
> >     case zip:extract(Pack, [{cwd, Dir}]) of
> >         {ok, Files} ->
> >             Files;
> >         {error, Reason} ->
> >             exit({error, Reason})
> >     end.
> 
> This happens because module 'zip' does not have -spec information about 
> its functions.  Without such information, dialyzer's analysis infers 
> that zip:extract/2 will either return something of the form {ok, term()} 
> or {error, term()}.  Note that the only thing that dialyzer can infer 
> given this information is that Files will be some term().  Your spec 
> promises is that this term is 'ok'.  In such cases, where dialyzer 
> cannot find any reason not to trust you, it keeps its mouth shut about 
> it.  (Unless you use option -Woverspecs in this case.)

Thanks, this clarifies a lot.

> 
> Now, it's actually the case that I have a spec-ed version of zip.erl 
> which has not made it into OTP yet and in that version I get the 
> following warning in your code:
> 
>     Invalid type specification for function dial:extract/2.
>     The success typing is (binary() | string(),binary() | string()) ->
> 	[binary() | string() | {binary() | string(),binary()}]
> 
> I will see whether this version can be included as in OTP or not...
> 
> 
> > % Here, the spawn_link of monitor_diskspace in monitor_launch() gives:
> > %   The created fun has no local return
> > % whereas the spawn_link of refresh_tags doesn't.  If the spawn_link
> > % of monitor_diskspace() function is commented out, there is no
> > % warning.  It's not clear how to interpret the warning or the
> > % inconsistency.
> > %
> > % Converting the nested list comprehension in monitor_diskspace into a
> > % list:map made the warning go away, at the expense of readability and
> > % perhaps even efficiency.
> 
> You are right. There is some inconsistency in the behavior of the two 
> cases. But note that the funs that are created have no return -- they 
> both call functions that go into an infinite loop and actually they are 
> explicitly spec-ed as no returning. So the warning you get is correct. 
> Still, you would like the two cases to be consistent and ideally also 
> not get this warning, if possible. (So that you do not have to resort to 
> calls outside this module as e.g. using lists:map/2.)
> 
> We spend some time with Stavros today looking into this and Stavros has 
> come up with a way of making sure the treatment of these two cases is 
> consistent and the one you want. When such specs are in place for 
> functions that go into infinite loops, the warnings for uses of them in 
> funs are suppressed.
> 
> Stay tuned and Stavros' patch will soon find its place to an OTP version 
> near you!

Excellent!

> Hope this explains all issues,

Yes, this was very helpful, thanks!  One issue I forgot to ask about was the
following:

$ cat /tmp/dial.erl 
-module(dial).
-export([f/1]).

-type t() :: 'a' | 'b'.
-spec f(atom()) -> t().

f(x) ->
    g();
f(y) ->
    h().

-spec g() -> t().
g() -> a.

-spec h() -> t().
h() -> b.

$ dialyzer /tmp/dial.erl 
dial.erl:12: The specification for dial:g/0 states that the function
  might also return 'b' but the inferred return is 'a'
dial.erl:15: The specification for dial:h/0 states that the function
  might also return 'a' but the inferred return is 'b'

This seems like a common problem when we use helper functions and
don't want to separately type the return values of each of the
helpers.  Both -Wunderspecs and -Woverspecs don't help here.  Is there
an idiomatic way of avoiding this warning, other than omitting the
-specs for the helpers altogether?

--prashanth