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

Question

我正在尝试了解透析器如何使用 polymorphic/parametrized 类型。我知道这是乐观的，如果有任何路径通过代码不会导致崩溃，它就会成功；鉴于这一事实，我不明白如何使用类型变量。

我有一个简单的递归二叉搜索树类型规范，旨在生成仅具有一种类型值的 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

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

-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).

然后你得到了你期望的错误（加上一个奇怪的 "Function b/0 has no local return"，这显然是合同中断的结果）：

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}}

注意 dializer 发出警告的事实并不能阻止代码无错地编译和执行。如果要在运行时间

产生错误，需要在代码中添加guard

-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)

Answer 2

你没有收到警告的原因是规范中的无约束类型变量（即那些没有 when 子句的变量）被泛化并被视为 term().

请注意，在您的示例中，即使没有最大限度的概括，您的代码中 T 的实例也有可能是 atom() | integer() 类型，这不会给出任何警告。

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

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

Dialyzer not detecting obvious type error in parametrized type

erlang

dialyzer