<div dir="ltr"><div>Well, this was what I ended up trying to improve in my master thesis back in 2010...</div><div><br></div><div>(Mainly for Tobias:) The attempted solution was to take all the type constraints that Dialyzer generates, convert them to disjunctive normal form and then carefully assemble an 'intersection type', able to infer things like bar(1) -> 'foo';(2) -> 'bar'. Still far from things like <anything but 1> though.<br></div><div><br></div><div>For the provided examples, intersection types together with standard call refinement would produce the desired warnings (I had a brief moment of nostalgia trying it out with just erts in the PLT on: <a href="https://github.com/aronisstav/otp/tree/intersection">https://github.com/aronisstav/otp/tree/intersection</a>):</div><div><br></div><div><div>$ dialyzer test2.erl</div><div>[...]</div><div>test2.erl:5: Function main/0 has no local return<br></div><div>test2.erl:7: The call test2:foo('bar') will never return since it differs in the 1st argument from the success typing arguments: ('foo')</div><div>[...]</div><div> done in 0m0.11s<br></div><div>done (warnings were emitted)</div></div><div><br></div><div><div>$ typer test2.erl </div><div><br></div><div>%% File: "test2.erl"</div><div>%% -----------------</div><div>-spec main() -> none().</div><div>-spec foo('foo') -> 'ok'.</div><div>-spec bar(1) -> 'foo'; (2) -> 'bar'.</div></div><div><br></div><div>Unfortunately, this extension made the analysis too slow (my dead-stupid conversion to disjunctive normal form leads to a lot of duplication of work), so it never went into OTP and as the code has been evolving significantly I would need to redo everything from scratch...</div><div><br></div><div>Other than that, I fully agree with Tobias.</div><div><br></div><div>Stavros</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 1, 2015 at 11:57 PM, Tobias Lindahl <span dir="ltr"><<a href="mailto:tobias.lindahl@gmail.com" target="_blank">tobias.lindahl@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><div>Hi Philip,<br></div></div><div><div><br></div><div>You are confusing Dialyzer with a static type checker (which it isn't [1]).</div><div><br></div><div>In one of your examples, there is no problem, and in the other one, the analysis would have to be pretty strong (and have a different type domain) to find the problem.<br></div><div><br></div><div>In test.erl, you have the success typings (written as specs)</div><div><br></div><div>-spec bar() -> 1 | 0. </div><div>-spec foo(1) -> 'ok'</div><div><br></div><div>So applying foo(bar()) _can_ succeed, which makes it perfectly fine in Dialyzer's eyes.</div><div><br></div><div>Similarly, in test2.erl you have the success typings</div><div><br></div><div>-spec bar(any()) -> 'foo' | 'bar'.</div><div>-spec foo('foo') -> 'ok'.</div><div><br></div><div>So applying </div><div><br></div><div>    ok = foo(bar(1)),<br></div><div><div>    ok = foo(bar(2)).</div></div><div><br></div><div>once again _can_ succeed (based on the success typings) so Dialyzer remains quiet.</div><div><br></div><div>Arguably, if Dialyzer's analysis was strong enough to infer the type</div><div><br></div><div>-spec bar (1) -> 'foo';</div><div>                (<Anything but 1>) -> 'bar',</div><div><br></div><div>it could warn, but the above typing is way beyond Dialyzer.</div><div><br></div><div>Tobias</div><div><br></div><div>[1] <a href="http://www.it.uu.se/research/group/hipe/dialyzer/publications/succ_types.pdf" target="_blank">http://www.it.uu.se/research/group/hipe/dialyzer/publications/succ_types.pdf</a></div><div><div class="h5"><div><br></div><div><div class="gmail_extra"><br><div class="gmail_quote">2015-01-01 17:24 GMT+01:00 Philip Müller <span dir="ltr"><<a href="mailto:mail@philip.in-aachen.net" target="_blank">mail@philip.in-aachen.net</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">Hi there,<br>
<br>
a few days ago I wanted to demonstrate the dialyzer to a friend who is unfamiliar with erlang/otp.<br>
<br>
Unfortunately, my simplest demo case did not work. I made a github project for it at [1] which documents the steps taken.<br>
<br>
For me, the first case (test.erl) looks like dialyzer is ignoring -Wunmatched_returns completely. The second case (test2.erl) I don't understand at all.<br>
<br>
Can someone explain what's going on there? Or should I file a bug report?<br>
<br>
Best regards<br>
 Philip<br>
<br>
[1]: <a href="https://github.com/exterm/dialyzer-fail-example" target="_blank">https://github.com/exterm/<u></u>dialyzer-fail-example</a><br>
______________________________<u></u>_________________<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" target="_blank">http://erlang.org/mailman/<u></u>listinfo/erlang-questions</a><br>
</blockquote></div><br></div></div></div></div></div></div>
<br>_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
<br></blockquote></div><br></div>