[erlang-questions] When can an integer > 0 not be a pos_integer() in the Dialyzer?

Bill M. <>
Sat Nov 15 06:44:14 CET 2008


Hello All:

Please consider the following functions
(which perform a sieve of Eratosthenes to find all primes < N where N > 1,
 for convenience we assume relatively small values of N, like 2^10 or 2^20).

Here is the code:
%%%%%%%%%%%%%%%%%%% Cut Here%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-module(test).
-export([test/0,list_primes/1]).

test()->
    list_primes(64).

%% Functions supporting the Sieve Of Erastothenes For Computing Primes
%% Not designed to be incredibly efficient, but correct and simple.
%% @todo Check syntax on the @spec statement for this function
%% @doc Computes the list of all primse up to N using Sieve of Erastotanes
(correct, perhaps not efficient)
-spec(list_primes/1 :: ( N :: pos_integer() )->[pos_integer()]).
list_primes(N) when (is_integer(N) and (N > 1))-> 
    Candidates = lists:seq(2,N),
    MaxFactor = round(math:sqrt(N) + 0.5) , %% poor man's ceiling function
    list_primes_helper(MaxFactor, Candidates).

%% @private
%% @doc Helper function for list_primes, does all the actual work of
%%      the sieve of Erastothanes
%% @todo the PrimeCandidates should be of type [ pos_integer() ] but the
dialyzer can't deal with it, so we must weaken it :-(
-spec(list_primes_helper/2 ::
     (MaxFactor :: pos_integer(), PrimeCandidates :: [ pos_integer() ]) ->
     [ pos_integer() ]).
list_primes_helper(MaxFactor, [Prime|Candidates]) when is_integer(MaxFactor) 
and is_integer(Prime) and (Prime > 0) and (MaxFactor > Prime) ->
    PrunedCandidates = [X || X <- Candidates, (X rem Prime) /= 0],
    [ Prime | list_primes_helper(MaxFactor, PrunedCandidates) ];
list_primes_helper(MaxFactor, [Prime|Candidates]) when
is_integer(MaxFactor) and is_integer(Prime) and (MaxFactor > 0) and 
(Prime >= MaxFactor) ->
    [Prime | Candidates]; %% all pruning is complete, 
list_primes_helper(_MaxFactor, [])
   when is_integer(_MaxFactor) and (_MaxFactor > 0)->
    [].
%%%%%%%%%%%%%%%%%%% Cut Here %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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()]

My guess is dialyzer didn't accurately guess the type of lists:seq(2,N).

I'd like to ask a few questions of the dialyzer maintainers.
1) When there is a conflict between a signature and the usage of a function,
    would it be possible for the dialyzer to suggest why it thinks that
    would happen.  Here it could extend the error message saying something like

" as invoked by list_primes/1 at line 15, since actual parameter 2,
  Candidates, is of type [integer()] instead of [pos_integer()]."

In practice, I think if the tool gives one reason why it thinks such an error
is justified (enumerating all of the reasons would probably be overkill),
then the user could address it (I know of a tool that does this for
another language, and I find it helpful).

Regards:

Bill M.




More information about the erlang-questions mailing list