-module(test).
-export([f/0, g/0]).
-spec f() -> RESULT when
RESULT :: 0..12 .
-spec g() -> RESULT when
RESULT :: 0..13 .
f () -> 100 .
g () -> 100 .
Running dialyzer (and typer) only the function f is caught.
dialyzer test.erl
Checking whether the PLT /Users/ben/.dialyzer_plt is up-to-date... yes
Proceeding with analysis...
test.erl:4: Invalid type specification for function test:f/0. The success typing is () -> 100
done in 0m0.53s
done (warnings were emitted)
the same with typer
typer test.erl
typer: Error in contract of function test:f/0
The contract is: () -> RESULT when RESULT :: 0..12
but the inferred signature is: () -> 100
Is this "expected" behaviour?
Yes it does seem to be "expected".
Looking at the source code here
It tests against the value of
-define(SET_LIMIT, 13).
in the test
t_from_range(X, Y) when is_integer(X), is_integer(Y) ->
case ((Y - X) < ?SET_LIMIT) of
true -> t_integers(lists:seq(X, Y));
false ->
case X >= 0 of
false ->
if Y < 0 -> ?integer_neg;
true -> t_integer()
end;
true ->
if Y =< ?MAX_BYTE, X >= 1 -> ?int_range(1, ?MAX_BYTE);
Y =< ?MAX_BYTE -> t_byte();
Y =< ?MAX_CHAR, X >= 1 -> ?int_range(1, ?MAX_CHAR);
Y =< ?MAX_CHAR -> t_char();
X >= 1 -> ?integer_pos;
X >= 0 -> ?integer_non_neg
end
end
end;
IMHO this seems dangerous, and does not provide any real guarantees. It should definitely be documented clearly. there is passing reference on the learn you some Erlang website.
A range of integers. For example, if you wanted to represent a number
of months in a year, the range 1..12 could be defined. Note that
Dialyzer reserves the right to expand this range into a bigger one.
But nothing official on the front page of google using the keywords dialyzer integer ranges
Edit... looking a bit closer you can see that if you try:
-module(test).
-export([h/0]).
-spec h() -> RESULT when
RESULT :: 1..13 .
h () -> 100 .
Dialyzer will catch the error! (Typer will not) ...
Yes, it is "expected" behaviour. Or rather "accepted".
Disclaimers:
- Dialyzer never promised to catch all the errors.
- Code like the above is fairly artificial.
Explanation:
Dialyzer's designers have decided to use overapproximations like this to (among other reasons) make the tool's type inference analysis terminate (reach a fixpoint) when analyzing recursive functions (the internal steps really look like this: "factorial's base case works for 0, so it's recurssive case also works for 1, so it also works for 2, so it also works for 3, [...], so it works for 12, ok so it also works for any char(), but it also works for char_range + 1 so it works for all integers()").
It is fairly rare that this (arbitrary indeed) limit becomes critical, and then again, Dialyzer never promised to report anything...
