<div dir="ltr">Stavros, thanks for the reply!<div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>And indeed, if I change boop/1 to be</div><div><br></div><div>boop(X) -></div><div> derp.</div><div><br></div><div>Then dialyzer rightfully corrects me with a primly emitted diagnostic:</div><div><br></div><div>tt.erl:9: Invalid type specification for function tt:boop/1. The success typing is ('hello') -> 'derp'<br></div><div><br></div><div>and dually if I change boop/1 to be</div><div><br></div><div>boop(X) -></div><div> hello.</div><div><br></div><div>Then dialyzer rightfully approves and emits no diagnostic.</div><div><br></div><div>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. </div><div><br></div><div>So I gather my inference that -spec operates as a constraint on the function's type is subtly invalid?</div><div><br></div><div>F.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 10, 2015 at 2:23 PM, Stavros Aronis <span dir="ltr"><<a href="mailto:aronisstav@gmail.com" target="_blank">aronisstav@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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><div class="h5"><div dir="ltr">On Thu, Dec 10, 2015 at 10:52 PM Felix Gallo <<a href="mailto:felixgallo@gmail.com" target="_blank">felixgallo@gmail.com</a>> wrote:<br></div></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><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></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>
</blockquote></div><br></div>