为什么Dialyzer告诉我这个有趣的合同有重叠的域名?

Pas*_*cal 5 erlang types dialyzer

我感兴趣地阅读在线书" 学习你一些二郎 ",并尝试一些练习来检查我的理解.

我对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.
Run Code Online (Sandbox Code Playgroud)

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

空({fifo,A,B})当is_list(A),is_list(B) - > false时.

Dialyzer告诉它因为重叠域而忽略规范.

有人能告诉我哪里弄错了吗?

我有另外一点,在尝试定义类型的fifo之前我有一个很好用的版本,An Dialyzer告诉我没有什么可以防止使用不正确的列表.令人惊讶的是,我找不到一种简单的方法(我可以在警卫中使用)来测试列表的正确/不正确的字符.

这真的很奇怪,因为当我使用bif长度/ 1时,它会因为badarg而失败!

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

24> is_list(L).==>是的

25>长度(L).==>异常错误:错误的参数

 in function  length/1

    called as length([1,2|3])
Run Code Online (Sandbox Code Playgroud)

谢谢

aro*_*tav 6

你的类型和规格没有问题。问题在于 Dialyzer 中用于表示类型的数据类型不能保持您提供的精度。具体来说,联合:{fifo, nonempty_list(A), list(A)} | {fifo, [], nonempty_list(A)}被“压缩”为{fifo, list(A), list(A)},因为元组具有相同的元数 (3) 和第一个原子元素 ( fifo)。Dialyzer 通常会进行过度近似(您也可以在此处看到)以使类型分析更加高效。您可以安全地忽略此警告。

对于第二个问题,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.
Run Code Online (Sandbox Code Playgroud)

然而,这不能放置在守卫中。在守卫中,您可以使用您在下面的评论中建议的那个(length(L) >= 0)。