为什么Erlang透析器在以下代码中找不到类型错误？

Question

free_vars_in_dterm({var, V}) -> {var, V};显然不能进行类型检查，然而，透析器显示一切正常。

$ 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永远不会出错。Erlang programmers)
2. Dialyzer经常背诵的从不承诺会找出代码中的所有错误。(不是那么有名)

对于任何“为什么透析器没有捕捉到这个错误”的问题，Maxim 2是(诚然不是很令人满意的)“标准”答案。

更具解释性的答案：

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