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

Felix Gallo felixgallo@REDACTED
Fri Dec 11 01:10:21 CET 2015

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.


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

> 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>

More information about the erlang-questions mailing list