[erlang-questions] When can an integer > 0 not be a pos_integer() in the Dialyzer?
Kostis Sagonas
kostis@REDACTED
Sat Nov 15 09:39:33 CET 2008
Bill M. wrote:
> Hello All:
>
> Please consider the following functions
> (which perform a sieve of Eratosthenes to find all primes < N where N > 1,
... CODE OMITTED ...
> Running the dialyzer from R12B4 gives (Note, I had to make the lines
> in the code snippet above fit in 80 columns or less, so the line
> number might be off):
>
> test.erl:20: Type specification test:list_primes_helper/2 ::
> (MaxFactor::pos_integer(),PrimeCandidates::[pos_integer()]) ->
> [pos_integer()] is a subtype of the success typing:
> (pos_integer(),[integer()]) -> [integer()]
Well, running dialyzer on your code will not give you this.
You will only get this if you explicitly turn on the option -Woverspecs.
You should not.
From the options that are turned off by default, the only two options
we recommend turning on are: -Wunmatched_returns and -Wunderspecs
The remaining options are mainly for developers & debugging.
(The manual could have been more explicit regarding this point - it will
be in the next version.)
> My guess is dialyzer didn't accurately guess the type of lists:seq(2,N).
Your guess is correct, but it also has to do with the fact that the spec
for this function is not as refined as it can be. In R12B-4, it reads:
-spec(seq/2 :: (integer(),integer()) -> [integer(),...]).
and it nowhere specifies that if you feed it two pos_integer() it will
return a list of pos_integer().
Kostis
More information about the erlang-questions
mailing list