統合された縮小処理

以下の文章はこちらの記事を翻訳したものです。https://github.com/HypothesisWorks/hypothesis/blob/master/HypothesisWorks.github.io/_posts/2016-12-05-integrated-shrinking.md

HypothesisとHaskellのQuickCheckの間にはいくつかの大きな違いがありますが、その中でも特に縮小処理の方法において顕著な差異があります。

具体的に言うと、HaskellのQuickCheckで行われる縮小処理はあまり効果的ではありませんが、Hypothesis（およびtest.checkやEQCにおいても）では非常に効果的です。プロパティベースドのテストシステムを実装する場合、効果的な縮小処理の方法を選択することが重要です。もし現在使っているプロパティベースドのテストシステムが効果的な方法を採用していないならば、そのシステムの失敗モードをしっかり理解する必要があります。

残念ながら、多くのプロパティベースドテストの実装は、HaskellのQuickCheckをモデルにしています。そのため、QuickCheckの持つ問題点をそのまま引き継いでいることが多いのです。

これらの違いの中でも特に重要なのは、縮小処理が値の生成過程にどのように組み込まれているかという点です。

HaskellのQuickCheckでは、縮小処理は型に基づいて定義されています。これは、どのような方法で生成された値であっても、与えられた型の任意の値が同じ方法で縮小されることを意味します。一方で、Hypothesisやtest.checkでは、縮小処理は生成過程の一部として扱われ、生成器がどのように値を縮小するかを制御します（これはHypothesisとtest.checkで異なり、EQCではさらに異なるかもしれませんが、ユーザーにとっての最終結果はほぼ同じです）。

この違いは些細なものではありません。生成過程に縮小を統合することで、次の2つの大きな利点が得られます。

1. 縮小処理が簡潔に構成され、生成されるどんなものでも縮小することができます。これは型がどのように生成されるかに依存しません。
2. 縮小処理が生成時と同じ不変条件を満たすことが保証されます。

最初の点は、主に利便性の面から重要です。型ベースのアプローチでは難しいことが、これによって可能になりますが、これは副次的なものです。主なメリットは、独自の縮小処理を書く手間を省けることにあります。

しかし、2番目の点は非常に重要です。これがなければ、テストの失敗が非常に混乱する可能性があります。

例えば、Hypothesisを使用した次のようなテストケースを考えてみましょう。

from hypothesis import given
from hypothesis.strategies import integers

even_numbers = integers().map(lambda x: x * 2)

@given(even_numbers)
def test_even_numbers_are_even(n):
    assert n % 2 == 0

このテストは常に合格します。なぜなら、生成される整数に2を掛けることで、常に偶数が生成されるからです。

しかし、テストを次のように変更した場合を考えてみましょう。

from hypothesis import given
from hypothesis.strategies import integers

even_numbers = integers().map(lambda x: x * 2)

@given(even_numbers)
def test_even_numbers_are_even(n):
    assert n % 2 == 0
    assert n <= 4

このテストは失敗します。nが5以上の場合、テストは失敗するからです。Hypothesisでは、失敗するとn=6で失敗することが多いです。これは渡された数が依然として偶数であり、テストに失敗する最小の偶数だからです。

しかし、もしHypothesisが型ベースの縮小を実装していたら（初期のバージョンではそうでしたが、1.0リリース前に変更されました）、n=1でテストが失敗する可能性があります。これは「1はどうでしょうか？1は完全に有効な整数です」という考え方から来るものです。これは期待した結果ではありません。私たちは偶数の整数でテストを行いたいのですが、型ベースの縮小がそれを妨げるのです。

これは「shrinkers are fuzzers」という問題の一例で、一つのエラーが別のエラーに置き換わることがあります。特に、重要なエラーが重要でないエラーに置き換わることが問題です。

この問題を解決するためには、テストに制約ロジックを導入する必要があります。

from hypothesis import assume, given
from hypothesis.strategies import integers

even_numbers = integers().map(lambda x: x * 2)

@given(even_numbers)
def test_even_numbers_are_even(n):
    assume(n % 2 == 0)
    assert n % 2 == 0
    assert n <= 4

この場合、assumeと最初のassertが重複しています。この例では問題は明白ですが、不変条件がより暗黙的で微妙な場合、問題はより深刻になります。Hypothesisでは複雑なデータの生成が簡単で便利ですが、それをテストやカスタム縮小で再現しようとすると、すぐに困難になります。

動的言語でこれを正しく実装するのは偶然ではありません。Haskell向けのtest.checkの元の提案やJackのようなHaskell用の別のプロパティベースドのシステムがこれを行っています。Haskellでは、新しい型を定義することが一般的な回避策ですが、動的言語ではこれがすぐに問題になります。これにより、型のデフォルトの縮小を無効にし、独自の縮小を定義することができます。

しかし、本来はそうした回避策が必要ないはずです。それを使用すると、縮小ロジックに不変条件をエンコードする必要があります。これは、自動的にうまく機能する方法よりも、多くの作業と脆弱性を伴います。

したがって、現在人気の静的型付け言語向けのプロパティベースドのテストシステムがこの動作を正しく実装していないことを考えると、それらは絶対に実装でき、そして実装すべきです。それによってユーザーの体験が大幅に改善されるでしょう。

もちろん、動的言語ではこの問題を回避することがさらに困難です。

結論として、型に基づく縮小手法には反対しましょう。それは良くないアイディアで、存在すると、プロパティベースドテストの失敗の理解がずっと難しくなる可能性が高いです。