Может ли Dialyzer видеть через функции транзакций Mnesia?

Question

Вот код с ошибкой, которую я думаю, что Dialyzer должен быть в состоянии определить:

-module(myapp_thing).

-spec exists(pos_integer()) -> yes | no.
exists(Id) ->
    myapp_mnesia:thing_exists(Id).

-module(myapp_mnesia).

thing_exists(Id) ->
    Exists = fun() -> 
                     case mnesia:read({thing, Id}) of
                         [] -> false;
                         _ ->  true
                     end
             end,
    mnesia:activity(transaction, Exists).

myapp_thing:exists/1 указан как возвращающийся yes | no, но тип возвращаемого значения на самом деле будет true | false (То есть, boolean()), который является то, что возвращается myapp_mnesia:thing_exists/1,

Однако, запуск Dialyzer на myapp проходит без предупреждений.

Если я изменю myapp_mnesia:thing_exists/1 просто вернуться true Я получаю соответствующее предупреждение; аналогично, если я добавлю правильную спецификацию:

-spec session_exists(pos_integer()) -> boolean().

Но похоже, что Dialyzer не может заглянуть внутрь функции транзакции mnesia Exists или по какой-то другой причине не может определить тип возврата для thing_exists.

Итак, являются ли функции транзакций mnesia барьером для Dialyzer или существует более общий барьер для вывода типа возврата Dialyzer?

Answer 1

В mnesia_tm:execute_transactionобеспеченное веселье вызывается внутри catch, что означает, что возвращаемый тип сворачивается в term() что касается Dialyzer. Таким образом, Dialyzer не может сделать вывод, что тип возвращаемого значения mnesia:activity/2 такой же, как и в предоставленной функции, и, следовательно, требует явной спецификации типа для этого.

Кроме того, я считаю, что Dialyzer обычно никогда не выводит тип возвращаемого значения на основе возвращаемого значения функции, предоставленной в качестве аргумента. Например, с этим модулем:

-module(foo).

-export([foo/1]).

foo(F) ->
    F(42).

Typer показывает следующее:

$ typer /tmp/foo.erl

%% File: "/tmp/foo.erl"
%% --------------------
-spec foo(fun((_) -> any())) -> any().

хотя, если я добавлю явную спецификацию типа -spec foo(fun((_) -> X)) -> X.Затем Тайпер принимает это.

(Я уверен, что разработчики Dialyzer будут иметь более полный и проницательный ответ на это.)