なぜコンテキストリダクションが必要ですか？

Question

私はちょうどハスケルの初期型クラスシステムのいくつかの問題点とその改善方法について、this paper（「タイプクラス：Peyton Jones &ジョーンズのデザインクラスの探索」を読んだところです。

発生する問題の多くは、コンテキスト縮小に関連しています。これは、「逆の関係」の関係に従ってインスタンスと関数の宣言に対する制約のセットを減らす方法です。

コンテキスト内でinstance (Ord a, Ord b) => Ord (a, b) ...のどこかにある場合は、が{Ord a, Ord b}に縮小されます（縮小では必ずしも制約の数が縮小されるわけではありません）。

この縮小がなぜ必要なのかを私は論文から理解しませんでした。

これは、タイプチェックのいくつかの形式を実行するために使用されました。削減された制約のセットがある場合、それらを満たすことができるインスタンスが存在するかどうかをチェックできます。それ以外の場合はエラーです。私はあなたが使用サイトで問題に気づくだろうから、それの付加価値が何であるかはあまり確信していませんが、大丈夫です。

あなたがそのチェックをしなければならない場合でも、推論型の中でなぜ縮小結果を使うのですか？この論文は、直感的ではない推論型につながると指摘する。

この論文はかなり古く（1997年）、私が知る限り、文脈の縮小は依然として懸念されています。 Haskell 2010の仕様では、私が上で説明した推論の動作（link）について言及しています。

だから、なぜこのようにするのですか？

Answer 1

これはThe Reasonかどうか分かりませんが、それは必ずしもA Reasonと考えられます。Haskellの初期段階では、タイプシグネチャには単純な制約、つまりタイプ変数。したがって、例えば、これらのすべては大丈夫だった：

Ord a => a -> a -> Bool 
Eq a => a -> a -> Bool 
Graph gr => gr n e -> [n] 

しかし、これらのどれも： - だけでなく、今日はまだと -

Ord (Tree a) => Tree a -> Tree a -> Bool 
Eq (a -> b) => (a -> b) -> (a -> b) -> Bool 
Graph Gr => Gr n e -> [n] 

私は気持ちがそこだったと思うことができていることコンパイラは手動で書くことができないタイプを推測することは少し残念です。文脈の縮小は、上記の署名を手で書くこともできるようにする方法でした。またはは有益な誤りです。例えば、1ので、合理的に

instance Ord a => Ord (Tree a) 

がスコープ内に、我々は法的署名Ord a => ...に違法署名Ord (Tree a) => ...を回すことができるかもしれません。一方、範囲内の関数に対してEqのインスタンスがない場合、そのコンテキストでEq (a -> b)が必要と推測されたタイプについてのエラーを報告します。直感的に気持ちの良い

1. ：

   は、これは他の利点のいくつかを持っています。文脈縮小規則の多くは、その型が合法であるかどうかを変更するのではなく、型を書くときに人間が行うことを反映します。ここでは重複排除と包含ルールについて考えています。(Eq a, Eq a, Ord a)にちょうどOrd a - 可読性のために確かにしたい変形1。

2. これは、しばしば愚かなエラーを捕らえることができます。法律に準拠した方法では満足できないEq (Integer -> Integer) => Boolのようなタイプを推測するのではなく、Perhaps you did not apply a function to enough arguments?のようなエラーを報告することができます。もっと親切！
3. 何が問題になったのかを特定するのは、コンパイラの仕事になります。 Eq (Tree (Grizwump a, [Flagle (Gr n e) (Gr n' e') c]))のような複雑なコンテキストを推測するのではなく、コンテキストが充足可能ではないと訴えるのではなく、代わりにこれを構成制約に縮小する必要があります。代わりに、既存のコンテキストからEq (Grizwump a)を特定できないという不満があります。これははるかに正確で実行可能なエラーです。

Answer 2

これは実際には辞書の実装を実装する場合に望ましいと思います。そのような実装では、 "辞書"、つまりタプルまたは関数のレコードは、適用された関数の型のすべての型クラス制約の暗黙の引数として渡されます。

ここで、問題はその辞書がいつどのように作成されるかです。すべてのタイプのクラスIntのためのすべての辞書は定数である必要がありますように単純なタイプのためにIntを観察してください。 リスト、Maybeまたはタプルなどのパラメータ化された型の場合はそうではありません。たとえば、タプルを表示するには、実際のタプル要素のインスタンスを知る必要があることが明らかです。したがって、そのような多型辞書は定数であることはできません。

辞書パッシングを導く原則は、適用された関数の型に型変数として現れる型の辞書だけが渡されるように見えます。または、別の言い方をすると、冗長な情報は複製されません。

f :: (Show a, Show b) => (a,b) -> Int 
f ab = length (show ab) 

showable要素のタプルは、このようにShow (a,b)のような制約は、我々はすでに(Show a, Show b)を知ったときに表示される必要はない、またshowableであることを情報：

は、この機能を考えてみましょう。

ただし、呼び出し元が辞書の作成と渡しを担当する必要がある代替の実装も可能です。これはfの種類は次のようになりますように、コンテキスト低下させることなく仕事ができる：

f :: Show (a,b) => (a,b) -> Int 

しかし、これはタプル辞書を作成するためのコードは、すべての呼び出しサイトで繰り返さなければならないことを意味します。そして、必要な制約の数が実際のように、増加の例を思い付くことは簡単です：

g :: (Show (a,a), Show(b,b), Show (a,b), Show (b, a)) => a -> b -> Int 
g a b = maximum (map length [show (a,a), show (a,b), show (b,a), show(b,b)]) 

明示的に渡され、実際のレコードを持つタイプクラス/インスタンスのシステムを実装することは有益です。例：

data Show' a = Show' { show' :: a -> String } 
showInt :: Show' Int 
showInt = Show' { show' = intshow } where 
     intshow :: Int -> String 
     intshow = show 

これを実行すると、「コンテキストの縮小」の必要性を容易に認識できます。