爲什麼透析器告訴我這個有趣的合同有重疊的域名？

我正在閱讀有趣的在線圖書「learn you some erlang」並嘗試一些練習來檢查我的理解。爲什麼透析器告訴我這個有趣的合同有重疊的域名？

我提出的FIFO例如，一些變型中，在章節型規格和Erlang，試圖定義一個「typed_fifo（T）」（一個FIFO其中所有元素必須是相同的類型T的）

我喜歡的類型規格有：

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

透析r說明由於重疊的域，它將忽略規範。

有人可以告訴我我犯了什麼錯誤嗎？

我還有一點，在嘗試定義鍵入的fifo之前，我有一個很好的工作版本，Dialyzer告訴我沒有任何東西阻止使用不正確的列表。令人驚訝的是，我沒有找到一種簡單的方法（我可以用在警衛中）來測試列表的正確/不恰當的特徵。

這真的很奇怪，因爲當我使用bif長度/ 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]) 

感謝

來源

2012-08-30 Pascal

您的類型和規格沒有任何問題。問題是Dialyzer中用於表示類型的數據類型並不像您提供的那樣精確。具體而言，因爲元組具有相同的元素（3）和第一個原子元素（fifo），所以聯合：{fifo, nonempty_list(A), list(A)} | {fifo, [],nonempty_list(A) }被「擊碎」爲{fifo, list(A), list(A)}。透析儀通常會做出過分逼近（如您還可以看到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.

這不能被放置在一個後衛但是。在警衛中，你可以使用你在下面評論中建議的那個（length(L) >= 0）。

來源

2012-08-30 19:24:02 aronisstav

謝謝你Aronis。我想我比Dialyzer打算提供的要多。我試圖找出使用這些規格定義的好處，透析器可以做什麼，以及我的努力是什麼。至少我發現這個問題與不正確的名單。順便說一下，我仍然在尋找解決我的第二個問題的方法。我有一個有趣的後衛測試，如：is_list（X），也是length（X）> -1。但它在函數內部崩潰。 – Pascal

我已經編輯了可能的解決方案的答案。哦，我的名字是斯塔夫羅斯！ :-) – aronisstav

關於你的第二個問題，有list工作的正確方法是：

1> L = [1,2|[3]]. 
[1,2,3] 
2> is_list(L). 
true 
3> length(L). 
3

注意，那[Head|Tail]符號需要從你Tail是list（不int）。

來源

2012-08-30 13:49:23

謝謝你的回答。我知道這一點，但我寫的問題可能太快了。我故意做了這個任務，以創建一個不正確的列表。事實是，我的fifo模塊只會創建有效的fifo，但是沒有什麼能夠阻止另一個模塊創建一個建立在不正確列表上的fifo，我想檢查它（爲了鍛鍊當然，在現實生活中我使用sdlib之一...） – Pascal

爲什麼透析器告訴我這個有趣的合同有重疊的域名？

回答

相關問題