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

[Felix Gallo]

Stavros -- thanks, that gave me the proper intuition.  I had been wanting
to defend a library against erroneous calls at library authoring time, as
one is trained to do with other type systems, but I now see that the
library user is going to have to dialyze the whole system in order to reap
those benefits.  Probably a small price to pay.  Appreciate the elucidation
as always.

F.


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

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