例えば、平等
map g (f xs) = f (map g xs)
は、すべての機能g :: tau -> tau'、すべてのリストxs :: [tau]及び全ての多機能f :: [a] -> [a]のために保持しています。基本的には、fは、引数リストの要素を並べ替えたり、要素を削除または複製したりすることはできますが、新しい要素を作成することはできません。
正直なところ、エラーの種類がポリモーフィックなので、非終端計算/ランタイムエラーをリストに「挿入」する可能性があるため、要素を作成できます。つまり、この平等はすでにseqのないHaskellのようなプログラミング言語で壊れています。以下の関数定義は、方程式の反例を提供します。基本的に、左側のgはエラーを「隠す」。式を固定するために
g _ = True
f _ = [undefined]
、gは厳密でなければならない、すなわち、それはエラーにエラーをマッピングしなければなりません。この場合、再び平等が成立する。
多形seq演算子を追加すると、式が再び破損します。たとえば、次のインスタンス生成は反例です。
g True = True
f (x:y:_) = [seq x y]
我々はリストxs = [False, True]を考えると、私たちはある一方
f (map g [False, True]) = f [undefined, True] = [undefined]
に、あなたが特定の要素を作るためにseqを使用することができ、
map g (f [False, True]) = map g [True] = [True]
を持っていますが、リストの位置は、リスト内の別の要素の定義に依存します。 gが合計である場合、等式は再び成立する。あなたが自由な定理でinteresetedされている場合、あなたはエラーやseqでさえ、言語と言語を検討しているかどうかを指定することを可能にする、free theorem generatorをチェックしてください。これはあまり実用的な関連性があるように見えるかもしれません、が、seqfoldr/build融合がseqの存在下で失敗し、例えば、機能的なプログラムのperformenceを改善するために使用されるいくつかの変換を破ります。 seqの存在下で無料定理についてもっと詳しく知りたい場合は、Free Theorems in the Presence of seqを見てください。
ポリモーフーフseqは、特定の変換が言語に追加されたときに破損することが分かっていました。しかし、南方にも欠点がある。あなたがseqをベース型クラスを追加する場合は、あなたがどこかに深いダウンseqを追加する場合は、あなたのプログラムに型クラス制約の多くを追加する必要があります。さらに、seqを使用して修正できるスペースリークが既にあることが判明したので、seqを省略することは選択肢ではありませんでした。
最後に、私は何かが恋しいかもしれませんが、a -> aのseq演算子がどのように機能するかわかりません。 seqの手がかりは、他の式が正規形になると評価された場合に、正規形にする式を評価することです。 seqのタイプがa -> aの場合、別の式の評価に依存して1つの式の評価を行う方法がありません。
'seq'機能は、我々は' seq'を持っているとき、ラムダ計算からのすべての結果は、もはや、信頼できないことを意味ラムダ定義可能（I.R.、ラムダ計算に定義することはできません）、ではありません。 – augustss