<html><head> <style> body {white-space: pre-wrap; word-wrap: break-word} </style> </head> <body>Thanks for the info. I'm using R15B. Why wouldn't this spec help Dialyzer avoid the warning?<div><br></div><div>-spec test(noloop | loop) -> no_return() | ok.</div>
<div><br><div id="1330043364072-sig-id">--<br>Jeremy </div><hr><div><strong>From:</strong> "Jesper Louis Andersen" <<a href="mailto:jesper.louis.andersen@erlang-solutions.com">jesper.louis.andersen@erlang-solutions.com</a>><br>
<strong>To:</strong> "<a href="mailto:erlang-questions@erlang.org">erlang-questions@erlang.org</a>" <<a href="mailto:erlang-questions@erlang.org">erlang-questions@erlang.org</a>><br><strong>Sent:</strong> February 24, 2012 8:38 AM<br>
<strong>Subject:</strong> Re: [erlang-questions] Dialyzer: Why do I get a 'will never return success typing error' with this recursive function?<br></div><br>On 2/24/12 1:36 PM, Jeremy Raymond wrote:<br>> test(noloop) -><br>
>      ok;<br>> test(loop) -><br>>      test(loop). % dialyzer warns about this call<br>It is usually worth it to give the version of Erlang/OTP you are using <br>since the dialyzer often changes from version to version. But I can tell <br>
you why the dialyzer warns you:<br><br>We are looking a success typings. A success type says: "f : A -> B under <br>the *assumption* of termination. That is, we look for ways to make the <br>function terminate normally and then we annotate the function with an <br>
input type A and an output type B which makes this termination happen. <br>If we pass 'noloop' then we get ok, hence we have the success type as <br>'noloop' -> 'ok'.. making the function terminate. Now, the recursive <br>
call test(loop) will never terminate and we have figured this out. Hence <br>'loop' as input cannot be in the success type of this function. In other <br>words, the dialyzer just worked as a termination checker on your code.<br>
> test(noloop) -><br>>      ok;<br>> test(loop) -><br>>      do_loop(loop).<br>><br>> do_loop(loop) -><br>>      do_loop(loop).<br>><br>My guess is that the dialyzer does not in this case look for the <br>
discrepancy in the context of a recursive call to loop so it is <br>conservative and finds the success type to be 'noloop' -> 'ok' as well. <br>But unless it knows by some other means that you make a call test(loop) <br>
somewhere in your code, this limited success type is not a problem.<br><br>-- <br>Jesper Louis Andersen<br>   Erlang Solutions Ltd., Copenhagen, DK<br><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">http://erlang.org/mailman/listinfo/erlang-questions</a><br> </div></body></html>