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

Stavros Aronis aronisstav@REDACTED
Fri Dec 11 00:46:01 CET 2015


Felix, you are right at inferring that specs are additional constraints,
but *only* in a function's calls: the return value of any call to boop will
be assumed to be something that is both in the inferred *and* the specified
type (here 'hello'); 'micronauts' will never be an expected return value
(try to pattern match it against 'micronauts' and see what happens).

Just to clarify the examples you mention:

If boop is inferred to be returning 'derp', then the spec is certainly
wrong, so Dialyzer complains.

If boop is inferred to be returning 'hello', then the spec is certainly
right, but underspecified, so Dialyzer stays silent unless -Wunderspecs is
used.

If boop is inferred to be returning 'hello' OR 'micronauts', then there is
the possibility that the spec is right (still underspecified; glory is
impossible) but Dialyzer overapproximated something, resulting in the
inclusion of an additional value which is impossible (see example in the
previous message).

Dialyzer's rule #1 is 'only warn if something is definitely wrong' (also
known as 'Dialyzer is never wrong'), so in that last case no warnings are
emitted. It is unfortunate that Dialyzer doesn't believe more in its own
deductive powers (in the original example 'micronauts' is certainly
possible and not an overapproximation) but then again rule #1's corollary is
'Dialyzer never promised to find all discrepancies'...!

Stavros

On Fri, Dec 11, 2015 at 12:17 AM Felix Gallo <felixgallo@REDACTED> wrote:

> 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/408bab4e/attachment.htm>


More information about the erlang-questions mailing list