量化约束如何转换为字典传递样式?

Question

^{QuantifiedConstraints1}已登陆 GHC 8.6，我正在阅读派生类型类(第 7 节(²首次建议的地方。但是，从操作角度来看，我无法理解QuantifiedConstraints是如何翻译成字典的。以下为论文摘录。

data Rose a = Branch a [(Rose a)]
data GRose f a = GBranch a (f (GRose f a))
class Binary a where
showBin :: a -> String
-- assuming following exists
-- instance (Binary a) => Binary [a]
instance (Binary a) => Binary (Rose a) where
showBin (Branch x ts) = showBin x ++ showBin ts 
-- illegal
instance ( Binary a
, Binary (f (GRose f a))
) => Binary (GRose f a) where
showBin (GBranch x ts) = showBin x ++ showBin ts

我们需要的是一种简化谓词的方法f (GRose f a).诀窍是采用"常量"实例 我们为上述Binary [a]承担的声明，以及 摘要：

-- using QuantifiedConstraints
instance ( Binary a
, forall b. (Binary b) => Binary (f b)
) => Binary (GRose f a) where
showBin (GBranch x ts) = showBin x ++ showBin ts

现在，除了(Binary a)，上下文还包含 多态谓词。此谓词可用于 将谓词Binary (f (GRose f a))减少到仅Binary (GRose f a)，我们有一个实例声明 为此。

从操作角度来看，谓词(Binary a)在上下文中对应于为类传递字典Binary.谓词forall b. Binary b => Binary (f b)对应 将字典转换器传递给函数。

特别是我无法摸索以下内容：

1. 将谓词Binary (f (GRose f a))减少到仅Binary (GRose f a)

2. 谓词对应于将字典转换器传递给函数。

Answer 1

对于常规约束，转换映射

class Colored a where
isRed :: a -> Bool
foo :: Colored a => T

自

newtype ColoredDict a = CD (a -> Bool)
foo :: ColoredDict a -> T

同样地

bar :: (forall a. Colored a => Colored [a]) => U

可以翻译为

bar :: (forall a. ColoredDict a -> ColoredDict [a]) -> U

2(谓词对应于将字典转换器传递给 功能。

bar的第一个参数是OP提到的"字典转换器"。

bar涉及等级 2 类型，但 Haskell 已经使用了很长时间。

1(将谓词Binary (f (GRose f a))减少到只有Binary (GRose f a)

关键是：每次bar需要解决约束Colored [t]时，它都可以利用量化约束，转而尝试解决更简单的约束Colored a。