型文脈にはt1 ~ t2
という形の等式制約を含めることができる。これは、t1
とt2
の二つの型が同じでなければならないということを示す。型族の存在下では、一般に二つの型が等しいかどうかを局所的に決めることは出来ない。このため、次の例のように、関数のシグネチャの文脈に等式制約が使われることがある。
sumCollects :: (Collects c1, Collects c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2
ここでは、c1
とc2
の要素の型が同じであることを要求している。一般に、等式制約におけるt1
とt2
は任意の単相型であってよい。単相型であるというのは、ランクの高い型が有効になっているかどうかにかかわらず、量化子を含んでいてはならないということである。
等式制約は、クラスとインスタンスの文脈でも使うことができる。前者によって、関数従属を使うプログラムから、代わりに族シノニムを使うプログラムへの、単純な翻訳が出来るようになる。一般的な考え方として、次のような形のクラス宣言があったとする。
class C a b | a -> b
これを、以下のように書き換える。
class (F a ~ b) => C a b where type F a
つまり、すべてのa1 .. an -> b
という関数従属性(FD)について、これをF a1 .. an
というFD型族とF a1 .. an ~ b
というスーパークラス文脈の等式で表現することで、実質的に関数従属性に名前を与えている。クラスインスタンスでは、FD族の型インスタンスをクラス頭部に沿った形で定義する。この過程でメソッドのシグネチャは影響を受けない。
Coercible
制約制約Coercible t1 t2
はt1 ~ t2
に似ているが、t1
とt2
が役割(7.25. 役割 )の意味で表現等価であることを記述するものである。これはData.Coerce
によってエクスポートされ、説明書もここにある。さらなる詳細と議論が論文Safe Coercions"にある。