9

Haskellプラットフォームで取得するApplicative型クラスのすべてのHaskellインスタンスは、すべてのApplicative法を満たしていることが証明されていますか？はいの場合、それらの証明はどこにありますか？

Control.Applicativeのソースコードには、さまざまなインスタンスの適用法が適用されるという証拠が含まれていないようです。それはただそれを述べています

-- | A functor with application.
--
--Instances should satisfy the following laws:

次に、コメントに法律を記載します。

他の型クラス（AlternativeとMonad）のインスタンスについても同様のケースを見つけました。

これらの図書館の利用者は、これらの法律を自分で確認することになっていますか？

しかし、私はこれらの法律の厳格な証拠が開発者によって他の場所で与えられたのかどうか疑問に思いましたか？

繰り返しになりますが、IO MonadのApplicate（またはMonad）法の厳密な証明には、一般に、外部との会話が含まれるため、非常に複雑になる可能性があることを認識しています。

ありがとう。

4

3 に答える 3

11

はい、立証責任は完全にライブラリの作成者にあります。これらの法律に違反する実装の例がいくつかあります。法律違反の標準的な例は でありListT、これはほとんどの基本モナドのモナド法則に従わない (例を参照)。これは非常にバグのある動作をListTもたらし、結果として誰も実際に使用しません。

私は、これらの種類の証明のほとんどが、標準的な場所で石にエッチングされていないことを確信しています. 証明のほとんどは、コミュニティのさまざまな好奇心旺盛なメンバーによって単純に繰り返され、完全にチェックされているため、しばらくすると、どの実装がそれらの法則を満たしているか、満たしていないかがわかります。

具体的な例を挙げると、ライブラリを作成するときは、自分のpipesライブラリが法律pipesを満たしていることを証明するCategory必要がありますが、誰かが要求した場合に備えて、将来の記録のためにこれらの証明をテキスト ファイルまたは hpaste に保存します。それらをソースに含めることは、特に結合法則の場合、非常に長くなる可能性があるため、実際には実行可能ではありません。

ただし、可能であれば、ユーザーが必要に応じて参照できるように、元のリポジトリに機械でチェックされたプルーフを含めることをお勧めします。

于 2012-09-26T16:59:21.013 に答える