Dyalizer warnings for too wide return type

[Alexey Romanov]

One problem I have with Dialyzer is that it complains about cases
where the return type specified is too wide.

E.g.

-type handle_cast_return() :: {noreply, tuple()} | {noreply, tuple(),
integer()} | {stop, any(), tuple()}.
-spec handle_cast(any(), tuple()) -> handle_cast_return().
handle_cast(_Msg, State) ->
    {noreply, State}.

The definition says that handle_cast returns what it is supposed to
return according to behaviour, but it gives this warning:

sqlite3.erl:520: The specification for sqlite3:handle_cast/2 states
that the function might also return {'noreply',tuple(),integer()} |
{'stop',_,tuple()} but the inferred return is {'noreply',_}

Given this definition of success typing (from "A Language for
Specifying Type Contracts in Erlang"):

"A success Typing of a function, f, is a type signature, (α) → β ,
such that whenever an application f(p) reduces to a value v, then p ∈
α and v ∈ β."

the given specification satisfies it, and shouldn't result in a
warning. Or at least, there should be an option to turn this set of
warnings off, and I don't see one in
`dialyzer -Whelp`.

Obviously, I can narrow the return type, but then if implementation
changes later, I have to review it. In some cases I _know_ that the
implementation will change, which makes this even more annoying:

-spec some_test() -> boolean().
some_test() -> false. %% TODO implement later

%% in a different module
foo() ->
  case m1:some_test() of
    true -> ...
    false -> ...
  end.

In addition to the warning about some_test() I get warnings about
foo(): "Pattern 'true' can never match type 'false' ", any functions
called only from the 'true' branch are reported to be unused, etc.
While these warnings are correct, they ignore my specification for
some_test(). Can Dialyzer be forced to prefer the return type given in
the spec over the` one it infers?

Yours, Alexey Romanov

________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]

[Vincent de Phily]

On Tuesday 12 October 2010 08:48:57 Alexey Romanov wrote:

> One problem I have with Dialyzer is that it complains about cases
> where the return type specified is too wide.
>
> E.g.
>
> -type handle_cast_return() :: {noreply, tuple()} | {noreply, tuple(),
> integer()} | {stop, any(), tuple()}.
> -spec handle_cast(any(), tuple()) -> handle_cast_return().
> handle_cast(_Msg, State) ->
>     {noreply, State}.
>
> The definition says that handle_cast returns what it is supposed to
> return according to behaviour, but it gives this warning:

[...]
> the given specification satisfies it, and shouldn't result in a
> warning. Or at least, there should be an option to turn this set of
> warnings off, and I don't see one in
> `dialyzer -Whelp`.

It sounds like -Wunderspecs or -Woverspecs would do that, but that doesn't
seem to work. Actually it looks like (contrary to documentation) -Wunderspecs
is on by default and we actually need a -Wno_underspecs option.

But a global no_underspec for the program sounds dangerous too (you'll hide
actual underspecs which should be fixed). Maybe dialyzer could ease the pain
by handly behaviour spec specially ?

> -spec some_test() -> boolean().
> some_test() -> false. %% TODO implement later
>
> %% in a different module
> foo() ->
>   case m1:some_test() of
>     true -> ...
>     false -> ...
>   end.
>
> In addition to the warning about some_test() I get warnings about
> foo(): "Pattern 'true' can never match type 'false' ", any functions
> called only from the 'true' branch are reported to be unused, etc.
> While these warnings are correct, they ignore my specification for
> some_test(). Can Dialyzer be forced to prefer the return type given in
> the spec over the` one it infers?

Yes, that annoys me as well. I understand the warning for the some_spec
function, but I think it shouldn't trickle down to the foo function. I have
another use-case where I recompile a module at runtime but provide an initial
implementation that always returns false.

I'd like dializer to trust me when I declare my interface, even if the
implementation doesn't match that. Actually, maybe we could make the case that
non-exported functions must have an exact spec whereas exported function can
have a spec that is more allowing than the implementation ?

--
Vincent de Phily
Mobile Devices
[phone]
[phone]

Warning
This message (and any associated files) is intended only for the use of its
intended recipient and may contain information that is confidential, subject
to copyright or constitutes a trade secret. If you are not the intended
recipient you are hereby notified that any dissemination, copying or
distribution of this message, or files associated with this message, is
strictly prohibited. If you have received this message in error, please
notify us immediately by replying to the message and deleting it from your
computer. Any views or opinions presented are solely those of the author
[hidden email] and do not necessarily represent those of
the
company. Although the company has taken reasonable precautions to ensure no
viruses are present in this email, the company cannot accept responsibility
for any loss or damage arising from the use of this email or attachments.

________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]

[Alexey Romanov]

Yours, Alexey Romanov



On Fri, Oct 15, 2010 at 1:45 PM, Vincent de Phily
<[hidden email]> wrote:

> On Tuesday 12 October 2010 08:48:57 Alexey Romanov wrote:
>> One problem I have with Dialyzer is that it complains about cases
>> where the return type specified is too wide.
>>
>> E.g.
>>
>> -type handle_cast_return() :: {noreply, tuple()} | {noreply, tuple(),
>> integer()} | {stop, any(), tuple()}.
>> -spec handle_cast(any(), tuple()) -> handle_cast_return().
>> handle_cast(_Msg, State) ->
>>     {noreply, State}.
>>
>> The definition says that handle_cast returns what it is supposed to
>> return according to behaviour, but it gives this warning:
> [...]
>> the given specification satisfies it, and shouldn't result in a
>> warning. Or at least, there should be an option to turn this set of
>> warnings off, and I don't see one in
>> `dialyzer -Whelp`.
>
> It sounds like -Wunderspecs or -Woverspecs would do that, but that doesn't
> seem to work.
> Actually it looks like (contrary to documentation) -Wunderspecs
> is on by default and we actually need a -Wno_underspecs option.

If I enable -Wunderspecs, I get a lot more warnings, so it isn't on by default.
These warnings don't seem to be considered underspecs for some reason.

>> In addition to the warning about some_test() I get warnings about
>> foo(): "Pattern 'true' can never match type 'false' ", any functions
>> called only from the 'true' branch are reported to be unused, etc.
>> While these warnings are correct, they ignore my specification for
>> some_test(). Can Dialyzer be forced to prefer the return type given in
>> the spec over the` one it infers?
>
> Yes, that annoys me as well. I understand the warning for the some_spec
> function, but I think it shouldn't trickle down to the foo function. I have
> another use-case where I recompile a module at runtime but provide an initial
> implementation that always returns false.
>
> I'd like dializer to trust me when I declare my interface, even if the
> implementation doesn't match that. Actually, maybe we could make the case that
> non-exported functions must have an exact spec whereas exported function can
> have a spec that is more allowing than the implementation ?

This may be reasonable.

> --
> Vincent de Phily
> Mobile Devices
> [phone]
> [phone]
>
> Warning
> This message (and any associated files) is intended only for the use of its
> intended recipient and may contain information that is confidential, subject
> to copyright or constitutes a trade secret. If you are not the intended
> recipient you are hereby notified that any dissemination, copying or
> distribution of this message, or files associated with this message, is
> strictly prohibited. If you have received this message in error, please
> notify us immediately by replying to the message and deleting it from your
> computer. Any views or opinions presented are solely those of the author
> [hidden email] and do not necessarily represent those of
> the
> company. Although the company has taken reasonable precautions to ensure no
> viruses are present in this email, the company cannot accept responsibility
> for any loss or damage arising from the use of this email or attachments.
>

________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]

[Kostis Sagonas-2]

Vincent de Phily wrote:

> On Tuesday 12 October 2010 08:48:57 Alexey Romanov wrote:
>> One problem I have with Dialyzer is that it complains about cases
>> where the return type specified is too wide.
>>
>> E.g.
>>
>> -type handle_cast_return() :: {noreply, tuple()} | {noreply, tuple(),
>> integer()} | {stop, any(), tuple()}.
>> -spec handle_cast(any(), tuple()) -> handle_cast_return().
>> handle_cast(_Msg, State) ->
>>     {noreply, State}.
>>
>> The definition says that handle_cast returns what it is supposed to
>> return according to behaviour, but it gives this warning:
> [...]
>> the given specification satisfies it, and shouldn't result in a
>> warning. Or at least, there should be an option to turn this set of
>> warnings off, and I don't see one in
>> `dialyzer -Whelp`.
>
> It sounds like -Wunderspecs or -Woverspecs would do that, but that doesn't
> seem to work. Actually it looks like (contrary to documentation) -Wunderspecs
> is on by default and we actually need a -Wno_underspecs option.
>
> But a global no_underspec for the program sounds dangerous too (you'll hide
> actual underspecs which should be fixed). Maybe dialyzer could ease the pain
> by handly behaviour spec specially ?
>
>> -spec some_test() -> boolean().
>> some_test() -> false. %% TODO implement later
>>
>> %% in a different module
>> foo() ->
>>   case m1:some_test() of
>>     true -> ...
>>     false -> ...
>>   end.
>>
>> In addition to the warning about some_test() I get warnings about
>> foo(): "Pattern 'true' can never match type 'false' ", any functions
>> called only from the 'true' branch are reported to be unused, etc.
>> While these warnings are correct, they ignore my specification for
>> some_test(). Can Dialyzer be forced to prefer the return type given in
>> the spec over the` one it infers?
>
> Yes, that annoys me as well. I understand the warning for the some_spec
> function, but I think it shouldn't trickle down to the foo function. I have
> another use-case where I recompile a module at runtime but provide an initial
> implementation that always returns false.

I could have written a much longer reply in this thread, but I'll keep
this reply a bit short with the risk of sounding a bit impolite. This is
not my intention.

The whole discussion above is a bit naive, but perhaps this is primarily
my fault because there is no document that explains dialyzer's decisions
and philosophy in general terms. For a long time now I wanted to write a
"dialyzer FAQ". I hope I can come around to that pretty soon.

Anyway, the short answer is that dialyzer will never do what users may
initially think it would be better if it did.  The only information that
dialyzer has to work with is the code and whenever it finds something
that is a discrepancy between what the code does and what the programmer
claims it does (e.g. in a spec) it spits a warning about it.  Dialyzer
cannot be in the minds of programmers and what's their ultimate
intention even if they add "%% TODO implement later" comments :-)

So, my reply to Alexey's message is that in a situation like the one he
describes the proper action is to either comment out the true case in
foo's code or realize that now is the time for this "later".

Now, having written all these, there is a dialyzer option that we have
primarily added for internal debugging purposes, but may come in handy
in situations like that. If you want dialyzer to do its analysis based
on success typings only and ignore the specs of the analyzed modules,
you can use the option '--no_spec'.

But there is no option "trust the specs, please" for cases where
dialyzer can determine that they do not correspond to the code.
Whenever you want to do that, simply don't use dialyzer!


> I'd like dializer to trust me when I declare my interface, even if the
> implementation doesn't match that. Actually, maybe we could make the case that
> non-exported functions must have an exact spec whereas exported function can
> have a spec that is more allowing than the implementation ?

Sorry, but I firmly believe that this last part is wrong. Having
published interfaces that do not correspond to the implementation is not
a good idea. Among other things, what sort of confidence do you have
that the client code works ok? How do you test things in this situation?

Cheers,
Kostis

________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]

[Vincent de Phily]

On Sunday 17 October 2010 18:11:59 Kostis Sagonas wrote:
> Vincent de Phily wrote:
> I could have written a much longer reply in this thread, but I'll keep
> this reply a bit short with the risk of sounding a bit impolite. This is
> not my intention.

Not at all, it's good to get an informed reply.
 
> The whole discussion above is a bit naive, but perhaps this is primarily
> my fault because there is no document that explains dialyzer's decisions
> and philosophy in general terms. For a long time now I wanted to write a
> "dialyzer FAQ". I hope I can come around to that pretty soon.

That'd be nice.
 

> Anyway, the short answer is that dialyzer will never do what users may
> initially think it would be better if it did.  The only information that
> dialyzer has to work with is the code and whenever it finds something
> that is a discrepancy between what the code does and what the programmer
> claims it does (e.g. in a spec) it spits a warning about it.  Dialyzer
> cannot be in the minds of programmers and what's their ultimate
> intention even if they add "%% TODO implement later" comments :-)
>
> So, my reply to Alexey's message is that in a situation like the one he
> describes the proper action is to either comment out the true case in
> foo's code or realize that now is the time for this "later".

I never said (and neither did the OP I think) that dialyzer should ignore the
spec/code discrepancy inside a module. For the obvious reason, as you say,
that dialyzer can't read minds.

What I thought (and it's quite possibly naive, but I'm not convinced yet) is
that callers of the function could sometimes use the spec instead of the code
to infer what the function returns. However, defining that "sometimes" may be
tricky, a pandora's box we don't want to open.

> Now, having written all these, there is a dialyzer option that we have
> primarily added for internal debugging purposes, but may come in handy
> in situations like that. If you want dialyzer to do its analysis based
> on success typings only and ignore the specs of the analyzed modules,
> you can use the option '--no_spec'.
>
> But there is no option "trust the specs, please" for cases where
> dialyzer can determine that they do not correspond to the code.
> Whenever you want to do that, simply don't use dialyzer!

But I do want to use dialyzer, I like it (insert kiddy tantrum here). And I'm
happy to get a dializer warning for that function, I just don't want the
warning to propagate. If the warning is justified I'll correct it. If it isn't
justified, I'll have less dialyzer noise to check and dismiss.
 
> > I'd like dializer to trust me when I declare my interface, even if the
> > implementation doesn't match that. Actually, maybe we could make the case
> > that non-exported functions must have an exact spec whereas exported
> > function can have a spec that is more allowing than the implementation ?
>
> Sorry, but I firmly believe that this last part is wrong. Having
> published interfaces that do not correspond to the implementation is not
> a good idea. Among other things, what sort of confidence do you have
> that the client code works ok? How do you test things in this situation?

I'll stand ground here, because it is a frequent and normal usecase (no buggy
or unfinished code involved). Whenever you use pluggable implementations
you're confronted with the "implementation does less that the interface
states" problem. How many gen_server handle_call/3 did you write that could
return all 8 possible Result types mentioned in the erlang docs ? Even for my
own interfaces (of which I have tighter control than the standard OTP
behaviours) I have that problem, because one module can return more types of
results than another, but the declared interface is the same for both modules.

Unless you say that specs should always follow the code exactly, but I think
that misses an opportunity to make them more usefull. If the spec is just
mirroring what dializer can infer automatically anyway, why do I keep writing
them by hand (or at all) ?


--
Vincent de Phily
Mobile Devices
[phone]
[phone]

Warning
This message (and any associated files) is intended only for the use of its
intended recipient and may contain information that is confidential, subject
to copyright or constitutes a trade secret. If you are not the intended
recipient you are hereby notified that any dissemination, copying or
distribution of this message, or files associated with this message, is
strictly prohibited. If you have received this message in error, please
notify us immediately by replying to the message and deleting it from your
computer. Any views or opinions presented are solely those of the author
[hidden email] and do not necessarily represent those of
the
company. Although the company has taken reasonable precautions to ensure no
viruses are present in this email, the company cannot accept responsibility
for any loss or damage arising from the use of this email or attachments.

________________________________________________________________
erlang-questions (at) erlang.org mailing list.
See http://www.erlang.org/faq.html
To unsubscribe; mailto:[hidden email]