Target ranges Erlang Dialyzer

Question

-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 . 

Dialyser (and typer) startup is delayed only by f .

 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) 

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 the “expected” behavior?

Answer 1

Yes, it seems to be "expected." Looking at the source code here, He checks the meaning

-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 it seems dangerous and does not give any real guarantees. This should be clearly documented. There is a link to find out about this Erlang site .

The range of integers. For example, if you want to represent the number of months in a year, a range of 1.12 can be defined. Please note that Dialyzer reserves the right to expand this range to a larger one.

But nothing official on the Google homepage using the dialyzer integer ranges keywords

Edit ... a little closer, you can see that if you try:

 -module(test). -export([h/0]). -spec h() -> RESULT when RESULT :: 1..13 . h () -> 100 . 

The dialyzer will catch a mistake! (Typer will not) ...

Answer 2

Yes, this is the “expected” behavior. Rather, "accepted."

Denial of responsibility:

• Dialyzer never promised to catch all the bugs.
• Code like the one above is pretty artificial.

---

Explanation:

Dialysis designers decided to use excessive approximations such as this (among other reasons) so that the analysis of the output of the type of tool ends (reaches a fixed point) when analyzing recursive functions (the internal steps really look like this: "factorial base register works for 0, so it also works for 1, so it also works on 2, so it also works on 3, [...], so it works on 12, fine, so it also works for any char() , but it also works for char_range + 1 , so it works for in integers() ").

It is quite rare that this (arbitrary) limit becomes critical, and then again, Dealer never promised to report anything ...