10

たとえば、カテゴリの法則がデータ型の一部の操作に適用されることを証明するために、等値を定義する方法をどのように決定すればよいでしょうか? ブール式を表すために次のタイプを検討します。

data Exp
    = ETrue
    | EFalse
    | EAnd Exp Exp
    deriving (Eq)

Expが ID ETrueと演算子を持つカテゴリを形成することを証明しようとすることは実行可能ですか?

(<&>) = EAnd

Eqインスタンスを再定義せずに? Eqのデフォルトのインスタンスを使用すると、左恒等法則が破られます。つまり、次のようになります。

ETrue <&> e == e

Falseと評価されます。ただし、eval 関数を定義する:

eval ETrue =  True
eval EFalse = False
eval (EAnd e1 e2) = eval e1 && eval e2

Eqインスタンスは次のようになります。

instance Eq Exp where
    e1 == e2 = eval e1 == eval e2

問題を修正します。(==)に関する比較は、そのような法則を満たしていると主張するための一般的な要件ですか、それとも特定のタイプの等値演算子に対して法則が成り立つと言うだけで十分ですか?

4

1 に答える 1

8

平等は悪です。強すぎるため、構造的平等 が必要になることはめったにありません。あなたがやっていることに対して十分に強い同等性だけが欲しいのです。これは特に圏論に当てはまります。

Haskell では、構造的な等価性が得られます。これは、多くの場合、独自の/deriving Eqの実装を作成したいことを意味します。==/=

簡単な例: 有理数を整数のペア として定義します data Rat = Integer :/ Integer。構造的等価性 (Haskell とは何か deriving)を使用する(1:/2) /= (2:/4)と、 が分数として になり 1/2 == 2/4ます。本当に気にするのは、タプルの表現ではなく、タプルが表す値 です。これは、換算された分数を比較する同等性が必要になることを意味するため、代わりにそれを実装する必要があります。

補足: コードを使用している誰かが、あなたが構造的等価性テストを定義したと仮定した場合、つまり==パターン マッチングによるデータ サブコンポーネントの置換を正当化するためのチェックを行った場合、そのコードは壊れる可能性があります。それが重要な場合は、コンストラクターを非表示にしてパターン マッチングを禁止するか、独自のclass(たとえばandEquivを使用して) 両方の概念を分離することができます。(これは、Agda や Coq のような定理証明者にとって最も重要です。Haskell では、最終的に何かが壊れるほど間違った実用的/現実世界のコードを取得することは非常に困難です。)====/=

Really Stupid(TM) の例: ある人が巨大な Rats の長いリストを印刷したいと考えており、s の文字列表現をメモInteger化することで 2 進数から 10 進数への変換を節約できると信じているとしましょう。Rat等しい Rats が 2 回変換されないように、s のルックアップ テーブルがあり、整数のルックアップ テーブルがあります。の場合 、不足している整数エントリは- / -間をコピーして変換をスキップ(a:/b) == (c:/d)することで埋められます(痛い!)。listの場合、が変換されてから、 の文字列がルックアップ エントリにコピーされる ためです。最終結果はボークです。acbd[ 1:/1, 2:/2, 2:/4 ]11:/1 == 2:/212"1/1, 1/1, 1/4"

于 2012-09-19T23:51:33.417 に答える