<div dir="ltr">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.<div><br></div><div>F.<br><div><div><br></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 10, 2015 at 3:46 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"><div>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).</div><div><br></div><div>Just to clarify the examples you mention:</div><div><br></div>If boop is inferred to be returning 'derp', then the spec is certainly wrong, so Dialyzer complains.<div><br></div><div>If boop is inferred to be returning 'hello', <span style="line-height:1.5">then the spec is certainly right, but underspecified, so Dialyzer stays silent unless -Wunderspecs is used.</span></div><div><span style="line-height:1.5"><br></span></div><div><span style="line-height:1.5">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).</span></div><div><span style="line-height:1.5"><br></span></div><div><span style="line-height:1.5">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 </span>corollary<span style="line-height:1.5"> is 'Dialyzer never promised to find all discrepancies'...!</span></div><span class="HOEnZb"><font color="#888888"><div><span style="line-height:1.5"><br></span></div><div><span style="line-height:1.5">Stavros</span></div></font></span></div><div class="HOEnZb"><div class="h5"><br><div class="gmail_quote"><div dir="ltr">On Fri, Dec 11, 2015 at 12:17 AM Felix Gallo <<a href="mailto:felixgallo@gmail.com" target="_blank">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">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><div dir="ltr"><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><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><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>
</blockquote></div>
</div></div></blockquote></div><br></div>