Эрланг Диализатор целочисленных диапазонов

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 .

Запуск диализатора (и тайпера) только с функцией 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)

то же самое с 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

Это "ожидаемое" поведение?

Answer 1

Да, это кажется "ожидаемым". Глядя на исходный код здесь, он проверяет значение

-define(SET_LIMIT, 13).

в тесте

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;

ИМХО это кажется опасным и не дает никаких реальных гарантий. Это должно быть четко задокументировано. есть ссылка на ваш сайт Erlang.

Диапазон целых чисел. Например, если вы хотите представить количество месяцев в году, можно определить диапазон 1..12. Обратите внимание, что Dialyzer оставляет за собой право расширить этот диапазон в более широкий.

Но ничего официального на главной странице Google, используя ключевые слова dialyzer integer ranges

Отредактируйте... посмотрев немного ближе, вы увидите, что если попытаетесь

-module(test).
-export([h/0]).

-spec h() -> RESULT when
      RESULT :: 1..13 .

h () -> 100 .

Диализатор поймает ошибку! (Тайпер не будет) ...

Answer 2

Да, это "ожидаемое" поведение. Вернее "принято".

Отказ от ответственности:

1. Диализатор никогда не обещал отлавливать все ошибки.
2. Код, подобный приведенному выше, довольно искусственный.

---

Объяснение:

Разработчики Dialyzer решили использовать такую ​​избыточную приближение, чтобы (среди прочих причин) заставить анализ вывода типа инструмента прекратить (достичь фиксированной точки) при анализе рекурсивных функций (внутренние шаги действительно выглядят так: "базовый случай факториала работает для 0, поэтому рекурсивный регистр также работает для 1, поэтому он также работает для 2, поэтому он также работает для 3, [...], поэтому он работает для 12, хорошо, поэтому он также работает для любого char(), но это также работает для char_range + 1 так работает на всех integers()").

Довольно редко этот (действительно произвольный) предел становится критическим, и опять же, Диализер никогда не обещал ничего сообщать...