<div dir="ltr">Hi Felix!<div><br></div><div>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.</div><div><br></div><div>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:</div><div><br></div><div>-module(foo).</div><div>-export([bar/1]).</div><div>bar(X) when is_atom(X) -> 1;</div><div>bar(_) -> 0.</div><div><br></div><div>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".</div><div><br></div><div><span style="line-height:1.5">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.</span><br></div><div><span style="line-height:1.5"><br></span></div><div><span style="line-height:1.5">Hope this helps,</span></div><div><span style="line-height:1.5"><br></span></div><div><span style="line-height:1.5">Stavros</span></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Dec 10, 2015 at 10:52 PM Felix Gallo <<a href="mailto:felixgallo@gmail.com">felixgallo@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">consider:<div><br></div><div><a href="https://gist.github.com/anonymous/e5165c443f6bdf0f0780" target="_blank">https://gist.github.com/anonymous/e5165c443f6bdf0f0780</a><br></div><div><br></div><div>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:</div><div><br></div><div>tt.erl:10: The specification for tt:boop/1 states that the function might also return 'glory' but the inferred return is 'hello' | 'micronauts'<br></div><div><br></div><div>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?</div><div><br></div><div>F.</div></div>
_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" rel="noreferrer" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
</blockquote></div>