types - 为什么 Dialyzer 告诉我这个有趣的合约有重叠的域？

Question

我正在饶有兴趣地阅读在线书籍“learn you some erlang”并尝试一些练习来检查我的理解。
我在 一章中对 fifo 示例做了一些修改。类型规范和 Erlang ，试图定义一个“typed_fifo(T)”(一个所有元素都必须是相同类型T的fifo)
我的类型规范是:

-type typed_empty_fifo() :: {fifo, [], []}.

-type typed_nonempty_fifo(A) :: {fifo, nonempty_list(A), list(A)} | {fifo, [],nonempty_list(A) }.

-type typed_fifo(A) :: typed_empty_fifo() | typed_nonempty_fifo(A).

当我在以下函数规范中使用它时:

-spec empty (typed_empty_fifo()) -> true;

  (typed_nonempty_fifo(_)) -> false.

empty({fifo, [], []}) -> true;

empty({fifo, A, B}) when is_list(A), is_list(B) -> false.

Dialyzer 告诉它会因为重叠域而忽略规范。
有人能告诉我我哪里出错了吗？
我还有一点，在尝试定义类型化的 fifo 之前，我有一个运行良好的版本，一个透析器告诉我没有什么可以阻止使用不正确的列表。令人惊讶的是，我没有找到一种简单的方法(我可以在 guard 中使用)来测试列表的正确/不正确字符。
这真的很奇怪，因为当我使用 bif length/1 时，它会因 badarg 的原因而失败!

23> L=[1,2|3]. ==> [1,2|3]

24> is_list(L). ==> true

25> length(L). ==> exception error: bad argument

 in function  length/1

    called as length([1,2|3])

谢谢

Answer 1

您的类型和规范没有问题。问题是 Dialyzer 中用于表示类型的数据类型并没有像您提供的那样精确。具体工会:{fifo, nonempty_list(A), list(A)} | {fifo, [], nonempty_list(A)}被“粉碎”成 {fifo, list(A), list(A)} ，因为元组具有相同的元数 (3) 和第一个原子元素 ( fifo )。 Dialyzer 通常会进行过度近似(如您所见 here )以使类型分析更有效。您可以放心地忽略此警告。

对于您的第二个问题，is_list/1仅检查作为参数传递的术语的第一个构造函数是否为 cons 单元格。偶is_list([1|2])返回 true .

如果你想确保一个参数是一个正确的列表，你可以在 case 中使用自定义函数。像这样的表达:

case is_proper_list(L) of
  true -> ...;
  false -> ...
end

is_proper_list([]) -> true;
is_proper_list([_|L]) -> is_proper_list(L);
is_proper_list(_) -> false.

但是，这不能放在 guard 中。在 guard 中，您可以使用您在下面的评论中建议的那个 ( length(L) >= 0 )。