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

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 的实例也有可能使用 atom() | 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:\git\XXXXX\src>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)