haskell - 制約パッケージはどのように機能しますか？

Question

Data.Constraint.Forallの背後にある考え方は、私が理解しているように、実装で強制を使用することですが、型システムを使用して安全性を確保します。後者に関して2つの質問があります。

1. なぜ2つのスコーレム変数（AとB）が必要なのですか？制約が「不明」タイプによって満たされる場合、それは多形であると想像します。2番目のタイプはどのように安全性を高めますか？
2. これらのタイプがスコーレム変数と呼ばれるのはなぜですか？存在記号を取り除くためにスコーレム化が使われていると思いましたが、ここでは全称記号が見られます。私が見逃したサインフリッピングはどこかにありますか？

Answer 1

MPTCと関数従属性を使用すると、制約でパラメーター化された制約を使用することにより、単一変数である場合にスコーレムを識別することができます。私が以前行っていたトリックは、2つある場合は機能しません。

このモジュールの外部で記述されたコードの観点から、変数はSkolemizedされます。それらは事実上「新鮮な」型コンストラクターです。

ただし、これらのタイプはエクスポートされないため、モジュールの外部で明示的に参照できないため、これらのSkolemをカバーするインスタンスは全称記号で定量化する必要があります。

これが私が実存から普遍にアップグレードする方法です。「サインフリップ」は、技術的にはスコーレムとしての役割からではなく、輸出されていない性質から来ています。