[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