[erlang-questions] Dialyzer: Why do I get a 'will never return success typing error' with this recursive function?

Jeremy Raymond jeraymond@REDACTED
Fri Feb 24 14:24:23 CET 2012


  Thanks for the info. I'm using R15B. Why wouldn't this spec help Dialyzer
avoid the warning?

-spec test(noloop | loop) -> no_return() | ok.

--
Jeremy
------------------------------
*From:* "Jesper Louis Andersen" <jesper.louis.andersen@REDACTED>
*To:* "erlang-questions@REDACTED" <erlang-questions@REDACTED>
*Sent:* February 24, 2012 8:38 AM
*Subject:* Re: [erlang-questions] Dialyzer: Why do I get a 'will never
return success typing error' with this recursive function?

On 2/24/12 1:36 PM, Jeremy Raymond wrote:
> test(noloop) ->
> ok;
> test(loop) ->
> test(loop). % dialyzer warns about this call
It is usually worth it to give the version of Erlang/OTP you are using
since the dialyzer often changes from version to version. But I can tell
you why the dialyzer warns you:

We are looking a success typings. A success type says: "f : A -> B under
the *assumption* of termination. That is, we look for ways to make the
function terminate normally and then we annotate the function with an
input type A and an output type B which makes this termination happen.
If we pass 'noloop' then we get ok, hence we have the success type as
'noloop' -> 'ok'.. making the function terminate. Now, the recursive
call test(loop) will never terminate and we have figured this out. Hence
'loop' as input cannot be in the success type of this function. In other
words, the dialyzer just worked as a termination checker on your code.
> test(noloop) ->
> ok;
> test(loop) ->
> do_loop(loop).
>
> do_loop(loop) ->
> do_loop(loop).
>
My guess is that the dialyzer does not in this case look for the
discrepancy in the context of a recursive call to loop so it is
conservative and finds the success type to be 'noloop' -> 'ok' as well.
But unless it knows by some other means that you make a call test(loop)
somewhere in your code, this limited success type is not a problem.

-- 
Jesper Louis Andersen
Erlang Solutions Ltd., Copenhagen, DK

_______________________________________________
erlang-questions mailing list
erlang-questions@REDACTED
http://erlang.org/mailman/listinfo/erlang-questions
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20120224/2cd298c0/attachment.htm>


More information about the erlang-questions mailing list