[erlang-questions] dialyzer apparently-erroneously thinking a spec is underspecified

[Felix Gallo]

Stavros, thanks for the reply!

So I do understanding that Dialyzer gets to boop/1 :: 'hello' |
'micronauts', and that it then cannot decide if it can really ever truly
return both 'hello' and 'micronauts'.  So far, so good.

But then, I would expect the glory() spec to act as a second-pass
constraint after the type for boop/1 has been inferred.  My expectation is
derived entirely from the ancient oral tradition folkways of my primitive
people, rather than a formal type theoretical foundation, but I would
expect the proposition 'hello' to be tested against {'glory' | 'hello'} and
pass; and then for the proposition 'micronauts' to be tested against
{'glory' | 'hello'} and fail, and for a diagnostic to be emitted.

And indeed, if I change boop/1 to be

boop(X) ->
  derp.

Then dialyzer rightfully corrects me with a primly emitted diagnostic:

tt.erl:9: Invalid type specification for function tt:boop/1. The success
typing is ('hello') -> 'derp'

and dually if I change boop/1 to be

boop(X) ->
   hello.

Then dialyzer rightfully approves and emits no diagnostic.

It is only in the case where the function's return is inferred to be
either-correctly-typed-or-not-correctly-typed where my expectation seems to
be failing.

So I gather my inference that -spec operates as a constraint on the
function's type is subtly invalid?

F.


On Thu, Dec 10, 2015 at 2:23 PM, Stavros Aronis <aronisstav@REDACTED>
wrote:

> Hi Felix!
>
> The type system that Dialyzer is based on (success types) allows for the
> return value of a function to be over-approximated (i.e. include more
> values). An unfortunate side effect of that characteristic is that, in
> general, Dialyzer cannot be sure whether a particular value can really be
> returned from a function or not neither can it discern whether a particular
> value is an overapproximation or not.
>
> Assume e.g. that instead of random:uniform/0 you had a call to another
> function foo:bar(X) (using boop's argument) with the following code:
>
> -module(foo).
> -export([bar/1]).
> bar(X) when is_atom(X) -> 1;
> bar(_) -> 0.
>
> With no spec provided, the inferred type for foo:bar/1 one will be "any()
> -> 0 | 1". Notice however that for every call from your module (with an
> argument of type glory/0, or specifically 'hello') the result will be 1,
> thus safe. Unfortunately Dialyzer cannot be sure about this and the
> inferred type of boop/1 will be "hello -> hello | micronauts", an
> overapproximation of the accurate "hello -> hello".
>
> Now in either example, since there can be some overlap, Dialyzer makes the
> 'safe' assumption that any extra values in the inferred type are just due
> to overapproximation and stays silent. It only complains about the
> impossible *extra* value in the spec (glory) which can never be returned.
>
> Hope this helps,
>
> Stavros
>
>
> On Thu, Dec 10, 2015 at 10:52 PM Felix Gallo <felixgallo@REDACTED> wrote:
>
>> consider:
>>
>> https://gist.github.com/anonymous/e5165c443f6bdf0f0780
>>
>> by inspection, the spec on the boop function is "wrong", but this code
>> passes dialyzer, unless you run it with -Wunderspecs or -Wspecdiffs, at
>> which point it complains:
>>
>> tt.erl:10: The specification for tt:boop/1 states that the function might
>> also return 'glory' but the inferred return is 'hello' | 'micronauts'
>>
>> So dialyzer does notice that 'micronauts' might be returned, and does
>> know that the glory() type does not include that as a choice, but believes
>> that the spec is just underspecified, rather than violated.  Why is that?
>>
>> F.
>> _______________________________________________
>> erlang-questions mailing list
>> erlang-questions@REDACTED
>> http://erlang.org/mailman/listinfo/erlang-questions
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20151210/c5b4ad00/attachment.htm>