6

このチュートリアルに基づいて、以下のスニペットを作成しました。最後の 2 行 (feed_squid(FeederRP)とfeed_red_panda(FeederSquid)) は明らかに定義された制約に違反していますが、Dialyzer はそれらを問​​題ないと判断しています。これはまさに、静的分析を実行するツールでキャッチしたいタイプのエラーであるため、非常に残念です。

チュートリアルに説明があります：

関数が間違った種類のフィーダーで呼び出される前に、まず正しい種類で呼び出されます。R15B01 の時点で、Dialyzer はこのコードのエラーを検出しませんでした。観測された動作は、指定された関数への呼び出しが関数の本体内で成功するとすぐに、Dialyzer が同じコード単位内のそれ以降のエラーを無視することです。

この動作の根拠は何ですか? サクセスタイピングの背後にある哲学が「オオカミを決して泣かない」ことであることは理解していますが、現在のシナリオでは、Dialyzer は意図的に定義された関数仕様を明確に無視します (関数が以前に正しく呼び出されたことを確認した後)。コードがランタイム クラッシュを引き起こさないことを理解しています。どういうわけか、Dialyzer に常に関数の仕様を真剣に考えさせることはできますか? そうでない場合、それを行うことができるツールはありますか？

-module(zoo).
-export([main/0]).

-type red_panda() :: bamboo | birds | eggs | berries.
-type squid() :: sperm_whale.
-type food(A) :: fun(() -> A).

-spec feeder(red_panda) -> food(red_panda());
            (squid) -> food(squid()).
feeder(red_panda) ->
    fun() ->
            element(random:uniform(4), {bamboo, birds, eggs, berries})
    end;
feeder(squid) ->
    fun() -> sperm_whale end.

-spec feed_red_panda(food(red_panda())) -> red_panda().
feed_red_panda(Generator) ->
    Food = Generator(),
    io:format("feeding ~p to the red panda~n", [Food]),
    Food.

-spec feed_squid(food(squid())) -> squid().
feed_squid(Generator) ->
    Food = Generator(),
    io:format("throwing ~p in the squid's aquarium~n", [Food]),
    Food.

main() ->
    %% Random seeding
    <<A:32, B:32, C:32>> = crypto:rand_bytes(12),
    random:seed(A, B, C),
    %% The zoo buys a feeder for both the red panda and squid
    FeederRP = feeder(red_panda),
    FeederSquid = feeder(squid),
    %% Time to feed them!
    feed_squid(FeederSquid),
    feed_red_panda(FeederRP),
    %% This should not be right!
    feed_squid(FeederRP),
    feed_red_panda(FeederSquid).
4

2 に答える 2

5

例をかなり最小限に抑えると、次の 2 つのバージョンがあります。

Dialyzer がキャッチできる最初のもの:

-module(zoo).
-export([main/0]).

-type red_panda_food() :: bamboo.
-type squid_food()     :: sperm_whale.

-spec feed_squid(fun(() -> squid_food())) -> squid_food().
feed_squid(Generator) -> Generator().

main() ->
    %% The zoo buys a feeder for both the red panda and squid
    FeederRP = fun() -> bamboo end,
    FeederSquid = fun() -> sperm_whale end,
    %% CRITICAL POINT %%
    %% This should not be right!
    feed_squid(FeederRP),
    %% Time to feed them!
    feed_squid(FeederSquid)

次に、警告のないもの:

    [...]
    %% CRITICAL POINT %%
    %% Time to feed them!
    feed_squid(FeederSquid)
    %% This should not be right!
    feed_squid(FeederRP).

キャッチできるバージョンに対する Dialyzer の警告は次のとおりです。

zoo.erl:7: The contract zoo:feed_squid(fun(() -> squid_food())) -> squid_food() cannot be right because the inferred return for feed_squid(FeederRP::fun(() -> 'bamboo')) on line 15 is 'bamboo'
zoo.erl:10: Function main/0 has no local return

...そして、ユーザーのより厳しい仕様に対して独自の判断を信頼することを好むケースです.

キャッチしないバージョンの場合、Dialyzer はfeed_squid/1引数の型fun() -> bambooが のスーパータイプであると想定しますfun() -> none()(クラッシュするクロージャーで、 内feed_squid/1で呼び出されない場合でも有効な引数です)。型が推論された後、Dialyzer は、渡されたクロージャーが実際に関数内で呼び出されているかどうかを知ることができません。

-Woverspecsオプションが使用されている場合、Dialyzer は依然として警告を表示します。

zoo.erl:7: Type specification zoo:feed_squid(fun(() -> squid_food())) -> squid_food() is a subtype of the success typing: zoo:feed_squid(fun(() -> 'bamboo' | 'sperm_whale')) -> 'bamboo' | 'sperm_whale'

...この関数が他のフィーダーまたは特定のフィーダーを処理することを妨げるものは何もないことを警告します! そのコードが一般的ではなく、クロージャーの期待される入出力をチェックした場合、Dialyzer が誤用をキャッチすることは間違いありません。私の観点からは、型仕様と Dialyzer に頼るよりも、実際のコードで誤った入力をチェックする方がはるかに優れています (いずれにせよ、すべてのエラーを見つけるとは約束されていません)。

警告: 奥深い難解な部分が続きます!

最初のケースでエラーが報告され、2 番目のケースではエラーが報告されない理由は、モジュール ローカルの改良の進行に関係しています。最初に、関数feed_squid/1は入力に成功しまし(fun() -> any()) -> any()た。最初のケースでは、関数feed_squid/1は最初に だけで洗練され、FeederRP間違いなく を返しbamboo、すぐに仕様を改ざんし、 のさらなる分析を停止しmain/0ます。2 番目の例では、関数feed_squid/1は最初にFeederSquidand が確実に返すだけで洗練され、次にandと return ORsperm_whaleの両方で洗練されます。次に、期待される戻り値で呼び出された場合、成功の入力はORです。仕様は、それがFeederSquidFeederRPsperm_whalebambooFeederRPsperm_whalebamboosperm_whaleダイアライザーはそれを受け入れます。一方、引数はfun() -> bamboo | sperm_whale成功のタイピングに基づいている必要fun() -> bambooがありfun() -> bambooます。それが仕様 ( fun() -> sperm_whale) に対してチェックされると、Dialyzer は引数が である可能性があると想定しますfun() -> none()。内部で渡された関数feed_squid/1(Dialyzer の型システムが情報として保持しないもの) を決して呼び出さず、常に を返すことを仕様で約束する場合sperm_whale、すべて問題ありません!

「修正」できるのは、型システムを拡張して、引数として渡されたクロージャーが実際に呼び出しで使用されていることに注意し、型推論の一部を「生き残る」唯一の方法が次の場合に警告することです。なるfun(...) -> none()。

于 2012-08-10T10:40:03.363 に答える
3

（注、ここでは少し推測しています。ダイアライザーのコードを詳しく読んでいません）。

「通常の」本格的な型チェッカーには、型チェックが決定可能であるという利点があります。「このプログラムは適切に型付けされていますか」と尋ねると、型チェッカーが終了すると、Yes または No のいずれかが返されます。ダイアライザーはそうではありません。それは本質的に停止問題を解決するビジネスにあります。その結果、あからさまに間違っているが、それでもダイアライザーのグリップをすり抜けてしまうプログラムが存在することになります。

ただし、これはそれらのケースの1つではありません:)

問題は 2 つあります。成功型とは、「この関数が正常に終了した場合、その型は何ですか?」というものです。上記では、関数は任意の type にfeed_red_panda/1一致する任意の引数で終了します。呼び出すことができ、それも機能するはずです。したがって、関数 in を 2 回呼び出しても問題は発生しません。どちらも終了します。fun (() -> A)Afeed_red_panda(fun erlang:now/0)main/0

問題の 2 番目の部分は、「仕様に違反しましたか?」です。多くの場合、仕様は実際にはダイアライザーで使用されていないことに注意してください。型自体を推論し、仕様の代わりに推論パターンを使用します。関数が呼び出されるたびに、パラメーターで注釈が付けられます。この場合、2 つのジェネレーター タイプで注釈が付けられますfood(red_panda()), food(squid())。次に、仕様に違反しているかどうかを判断するために、これらの注釈に基づいて関数のローカル分析が行われます。正しいパラメーターが注釈に存在するため、関数が一部の関数で正しく使用されていると想定する必要があります。コードの一部。squid でも呼び出されることは、他の状況で呼び出されることのないコードのアーティファクトである可能性があります。私たちは関数ローカルであるため、わからず、プログラマーに疑いの利益をもたらします。

squid-generator で間違った呼び出しのみを行うようにコードを変更すると、仕様の不一致が見つかります。唯一可能な呼び出しサイトが仕様に違反していることを知っているからです。間違った呼び出しを別の関数に移動すると、それも見つかりません。注釈はまだ呼び出しサイトではなく関数にあるためです。

各コールサイトを個別に処理できるという事実を説明するダイアライザーの将来の変形を想像することができます. ダイアライザーも時代とともに変化しているので、将来的にはこの状況に対応できるようになるかもしれません。しかし、現在、それはすり抜けていくエラーの1つです。

重要なのは、ダイアライザーが「型取りのチェッカー」として使用できないことに注意することです。プログラムに構造を強制するために使用することはできません。あなたはそれを自分で行う必要があります。より静的なチェックが必要な場合は、Erlang 用の型チェッカーを作成し、コード ベースの一部で実行することがおそらく可能です。しかし、コードのアップグレードと配布で問題が発生するため、扱いが容易ではありません。

于 2012-08-08T09:42:44.640 に答える