haskell - 约束分布类型族的转换

Question

假设：导致Constraints 的类型族总是分布在它们的representational参数上。

例如，Fam x Eq `And` Fam x Show相当于Fam x (Eq `And` Show)ifFam的第二个参数具有代表性。

问题：

• 上述假设真的正确吗？有没有参考？
• GHC 是否允许利用此规则转换等效约束？

Answer 1

直观地说，如果以逆变方式Fam x c使用，这将失效。c现在可以使用量化约束来实现。例如

Fam x c = (forall a. c a => D a x)

对于一些D a x :: Constraint.

（我认为这是representational，即使我并不完全肯定。）

因此Fam x (Show `And` Eq)意味着

forall a. (Show a, Eq a) => D a x

虽然(Fam x Eq, Fam x Show)意味着

( forall a. (Show a) => D a x
, forall a. (Eq a) => D a x )

这两个约束是不等价的。例如，如果D a x = (Show a, Eq a)前者满足，而后者则不满足。