为什么Erlang Dialyzer在以下代码中找不到类型错误? [英] Why Erlang Dialyzer cannot find type error in the following code?
问题描述
free_vars_in_dterm({var, V}) -> {var, V};显然不能键入检查，但是，透析器说一切正常.
free_vars_in_dterm({var, V}) -> {var, V}; obviously cannot type check, however, dialyzer says everything is OK.
$ 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).
推荐答案
首先，使用Dialyzer的格言:
First a short answer, using Dialyzer's maxims :
- Dialyzer永远不会出错.(Erlang程序员经常引用)
- Dialyzer从未承诺要在代码中找到所有错误.(不太出名)
- Dialyzer is never wrong. (recited very often by Erlang programmers)
- Dialyzer never promised to find all errors in your code. (not so famous)
最大数字2是(为什么Dialyzer没有捕获此错误"问题)的(标准的，不是很令人满意的)答案.
Maxim number 2 is the (admittedly not very satisfying) "standard" answer to any "Why Dialyzer didn't catch this error" question.
更多解释性答案:
Dialyzer对函数的返回值的分析经常做得过于逼近.因此，类型中包含的任何值都应视为可能返回"值.不幸的是，有时肯定要返回的值(例如您的{var, V}元组)也被视为可能返回". Dialyzer必须保证最大值为1(永远不会出错)，因此，在可能返回"意外值的情况下，它将不会发出警告，除非无法返回任何实际指定的值.最后一部分是在整个函数的级别进行检查的，并且由于在您的示例中某些子句确实返回了集合，因此不会生成警告.
Dialyzer's analysis for return values of functions is frequently doing over-approximations. As a result, any value included in the types should be considered to be a "maybe returned" value. This has the unfortunate side-effect that sometimes values that are certainly going to be returned (such as your {var, V} tuple) are also considered "maybe returned". Dialyzer must guarantee maxim 1 (never be wrong), so in cases where an unexpected value "may be returned" it will not give a warning, unless none of the actually specified values can be returned. This last part is checked at the level of the entire function, and since in your example some of the clauses indeed return sets, no warnings are generated.
这篇关于为什么Erlang Dialyzer在以下代码中找不到类型错误?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
