なぜDialyzerはこの単純なエラーをキャッチしませんか？

Question

ダイアライザーは、この関数の戻り値の型

-spec myfun(integer()) -> zero | one. 
myfun(0) -> zero; 
myfun(1) -> one; 
myfun(2) -> other_number. 

に矛盾を通知しませんが、これがそうであるなぜそれが

myfun(_) -> other_number. 

ている最後の行の場合に検出さ？ は、上記の非常に単純な場合でなければなりません「ダイアライザーがない理由...」、私は...

おかげ

Answer 1

タイプの質問に簡単に答えを信じてできるように設計されているため」であります常に正しい "または"それがすべてのものや特定のものを捕まえることを約束することがないため "である。

---

もっと複雑な回答については、さらに質問を指定する必要があります。

-module(bar). 

-export([myfun1/1, myfun2/1]). 

-spec myfun1(integer()) -> zero | one. 

myfun1(0) -> zero; 
myfun1(1) -> one; 
myfun1(2) -> other_number. 

-spec myfun2(integer()) -> zero | one. 

myfun2(0) -> zero; 
myfun2(1) -> one; 
myfun2(_) -> other_number. 

そして、それを透析：：私はモジュールであなたの例を記述する場合

$ dialyzer bar.erl 
    Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes 
    Proceeding with analysis... done in 0m0.64s 
done (passed successfully) 

を...どちらの不一致を '検出' され、 "エラー" はありませんどちらも起こします。コードがいくつかの点で、より一般的な（余分な値を返すことができる）場合があり、仕様よりもいくつかの点で制限が厳しい（バージョン1のすべての整数を処理できない）場合があります。

番目のバージョンの問題が-Woverspecsで見つけることができます：

$ dialyzer -Woverspecs bar.erl 
    Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes 
    Proceeding with analysis... 
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero' 
done in 0m0.58s 
done (warnings were emitted) 

警告は仕様は、コードよりも限定的である正確と説明しています。

両方の問題にも極めて珍しい-Wspecdiffsによって検出することができます。操作の

$ dialyzer -Wspecdiffs bar.erl 
    Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes 
    Proceeding with analysis... 
bar.erl:5: Type specification bar:myfun1(integer()) -> 'zero' | 'one' is not equal to the success typing: bar:myfun1(0 | 1 | 2) -> 'one' | 'other_number' | 'zero' 
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero' 
done in 0m0.61s 
done (warnings were emitted) 

-Woverspecsも-Wspecdiffsどちらのモードが奨励され、透析装置のタイプの分析ができると種類を一般化されますので、「何かがAで指定されているとより制限的な方法 "は一般化の結果である可能性があります。

これらの関数を引数として0と1だけを指定して呼び出すこともできます。この場合、仕様は「ok」です。