Erlang Dialyzerが次のコードで型エラーを見つけられないのはなぜですか？

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

まず短い答え、ダイアライザーの格言を使用して：

1. ダイアライザーは決して間違っています。（非常によくErlangのプログラマーが引用）
2. Dialyzerはコード内のすべてのエラーを見つけることを決して約束しませんでした。 （そう有名ではない）は

マキシム番号2は、任意の「ダイアライザーは、このエラーをキャッチしていないのはなぜ」という質問に（確かに非常に満足していない）「標準」の答えです。

---

詳しい説明答：関数の戻り値のため

ダイアライザーの分析は、頻繁に過近似やっています。その結果、型に含まれる値は「多分返される」値であるとみなされるべきです。これは残念なことに、確かに返される値（例えば、{var, V}タプルなど）が「多分返される」と考えられるという不都合な副作用があります。 Dialyzerは最大1を保証する必要があります（間違ってはなりません）。したがって、予期しない値が返される可能性がある場合は、実際に指定された値が返されない限り、警告は出ません。この最後の部分は関数全体のレベルでチェックされます。例では実際にいくつかの句が返されるため、警告は生成されません。