types - 为什么 Erlang Dialyzer 在以下代码中找不到类型错误？

Question

free_vars_in_dterm({var, V}) -> {var, V}; 显然不能类型检查，然而，dialyzer 说一切正常。

$ dialyzer *erl
  Checking whether the PLT ~/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.66s
done (passed successfully)

代码如下:

-module(formulas).

-type formulas() :: {predicate(), [dterm()]}
                  | {'~', formulas()}
                  | {'&', formulas(), formulas()}
                  | {'|', formulas(), formulas()}
                  | {'->', formulas(), formulas()}
                  | {'<->', formulas(), formulas()}
                  | {'exist', variable(), formulas()}
                  | {'any', variable(), formulas()}.

-type dterm() :: constant()
               | variable()
               | {func(), [dterm()]}.

-type constant() :: {const, atom()}
                  | {const, integer()}.

-type variable() :: {var, atom()}.

-type func() :: {function,
                 Function_name::atom(),
                 Arity::integer()}.

-type predicate() :: {predicate,
                      Predicate_name::atom(),
                      Arity::integer()}.


-include_lib("eunit/include/eunit.hrl").

-export([is_ground/1, free_vars/1, is_sentence/1]).

-spec is_ground(formulas()) -> boolean().
is_ground({_, {var, _}, _}) -> false;
is_ground({{predicate, _, _}, Terms}) ->
    lists:all(fun is_ground_term/1, Terms);
is_ground(Formulas) ->
    Ts = tuple_size(Formulas),
    lists:all(fun is_ground/1, [element(I, Formulas)
                                || I <- lists:seq(2, Ts)]).

-spec is_ground_term(dterm()) -> boolean().
is_ground_term({const, _}) -> true;
is_ground_term({var, _}) -> false;
is_ground_term({{function, _, _}, Terms}) ->
    lists:all(fun is_ground_term/1, Terms).


-spec is_sentence(formulas()) -> boolean().
is_sentence(Formulas) ->
    sets:size(free_vars(Formulas)) =:= 0.

-spec free_vars(formulas()) -> sets:set(variable()).
free_vars({{predicate, _, _}, Dterms}) ->
    join_sets([free_vars_in_dterm(Dterm)
               || Dterm <- Dterms]);
free_vars({_Qualify, {var, V}, Formulas}) ->
    sets:del_element({var, V}, free_vars(Formulas));
free_vars(Compound_formulas) ->
    Tp_size = tuple_size(Compound_formulas),
    join_sets([free_vars(element(I, Compound_formulas))
               || I <- lists:seq(2, Tp_size)]).

-spec free_vars_in_dterm(dterm()) -> sets:set(variable()).
free_vars_in_dterm({const, _}) -> sets:new();
free_vars_in_dterm({var, V}) -> {var, V};
free_vars_in_dterm({{function, _, _}, Dterms}) ->
    join_sets([free_vars_in_dterm(Dterm)
               || Dterm <- Dterms]).

-spec join_sets([sets:set(T)]) -> sets:set(T).
join_sets(Set_list) ->
    lists:foldl(fun (T, Acc) -> sets:union(T, Acc) end,
                sets:new(),
                Set_list).

Answer 1

首先是一个简短的回答，使用 Dialyzer 的格言:

1. Dialyzer is never wrong.(Erlang 程序员经常背诵)
2. Dialyzer 从未 promise 会发现您代码中的所有错误。(不太出名)

最大数字 2 是(诚然不是很令人满意)对任何“为什么 Dialyzer 没有捕获到这个错误”问题的“标准”答案。

---

更具解释性的答案:

Dialyzer 对函数返回值的分析经常会过度逼近。因此，类型中包含的任何值都应被视为“可能返回”的值。这有一个不幸的副作用，有时肯定会返回的值(例如您的 {var, V} 元组)也被视为“可能返回”。 Dialyzer 必须保证 maxim 1(永远不会出错)，因此在“可能返回”意外值的情况下，它不会发出警告，除非无法返回任何实际指定的值。最后一部分在整个函数级别进行检查，并且由于在您的示例中某些子句确实返回集合，因此不会生成任何警告。