透析器未检测到参数化型的明显类型误差

Question

我试图了解透析器如何与多态/参数化类型一起工作。我知道它是乐观的，如果有任何不会导致崩溃的代码路径，它就会成功;鉴于这一事实，我不明白如何使用类型变量。

我有一个简单的递归二叉搜索树类型规范，旨在生成仅具有一种类型值的 BST。我知道(例如(原子和整数在 Erlang 中是可比较的，但我不希望我的 BST 允许这些比较。我编写并导出了一个函数b/0，该函数用整数和原子构建BST，透析器没有痛苦。

-module(bst).
-export([add/2, b/0, new/1]).
-type bst(T) :: {T, bst(T), bst(T)} | nil.
-spec new(T) -> bst(T).
-spec add(T, bst(T)) -> bst(T).
new(Root) -> {Root, nil, nil}.
add(Val, nil) -> {Val, nil, nil};
add(Val, {Root, Left, Right}) ->
case Val =< Root of
true -> {Root, add(Val, Left), Right};
false -> {Root, Left, add(Val, Right)}
end.
% Why no type error here? Adding atom to bst(integer()),
% but type spec allows only same type.
b() -> N = new(8), add(why_no_type_error, N).

运行透析器可得出以下成功结果：

dialyzer-tests ❯ dialyzer bst.erl
Checking whether the PLT /home/.../.dialyzer_plt is up-to-date... yes
Proceeding with analysis... done in 0m0.12s
done (passed successfully)

我能够通过编辑我的add/2规范来使此示例失败，如下所示：

-spec new(integer()) -> bst(integer());
(atom()) -> bst(atom()).
-spec add(integer(), bst(integer())) -> bst(integer());
(atom(), bst(atom())) -> bst(atom()).

这是惯用语，还是有更好的方法可以做到这一点？我不一定想为树上的每个可能操作详细说明每种可能的类型。

Answer 1

您没有收到警告的原因是，规范中的无约束类型变量(即没有when子句的变量(被泛化并被视为term()。

请注意，在您的示例中，即使没有最大泛化，代码中的T实例也可能使用 Typeatom() | integer()，而不会发出警告。

我想不出使用类型变量会导致错误的示例，因为我不完全理解您要查找的内容。

Answer 2

将元组的第一个元素限制为整数有效

-module(bst).
-export([add/2, b/0, new/1]).
-type bst() :: {integer(), bst(), bst()} | nil.
-spec new(integer()) -> bst().
-spec add(integer(), bst()) -> bst().
new(Root) -> {Root, nil, nil}.
add(Val, nil) -> {Val, nil, nil};
add(Val, {Root, Left, Right}) ->
case Val =< Root of
true -> {Root, add(Val, Left), Right};
false -> {Root, Left, add(Val, Right)}
end.
% this will generate a warning with dialyzer,
% but compile and execute without error.
b() -> 
N = new(8), 
add(why_no_type_error, N).

然后你得到你期望的错误(加上一个奇怪的"函数 b/0 没有本地返回"，这显然是合约中断的结果(：

C:gitXXXXXsrc>dialyzer bst.erl
Checking whether the PLT c:/Users/YYYYY/.dialyzer_plt is up-to-date... yes
Proceeding with analysis...
bst.erl:22: Function b/0 has no local return
bst.erl:24: The call bst:add
('why_no_type_error',
N :: {integer(), 'nil', 'nil'}) breaks the contract
(integer(), bst()) -> bst()
done in 0m0.20s
done (warnings were emitted)

在运行时：

1> c(bst).                
{ok,bst}
2> bst:b().
{8,nil,{why_no_type_error,nil,nil}}

请注意，拨号程序发出警告的事实不会阻止代码编译和执行而没有错误。如果要在运行时生成错误，则需要在代码中添加保护

-module(bst).
-export([add/2, b/0, new/1]).
% this version of code has the same warning with dialyzer
% and issues an exception at run time
-type bst() :: {integer(), bst(), bst()} | nil.
-spec new(integer()) -> bst().
-spec add(integer(), bst()) -> bst().
new(Root) when is_integer(Root) -> {Root, nil, nil}.
add(Val, nil) when is_integer(Val) -> {Val, nil, nil};
add(Val, {Root, Left, Right}) when is_integer(Val) ->
case Val =< Root of
true -> {Root, add(Val, Left), Right};
false -> {Root, Left, add(Val, Right)}
end.
b() -> 
N = new(8), 
add(why_no_type_error, N).

在运行时：

3> c(bst).                
{ok,bst}
4> bst:b().               
** exception error: no function clause matching 
bst:add(why_no_type_error,{8,nil,nil}) (bst.erl, line 13)