QuantifiedConstraints如何翻译成字典传递风格？

Question

QuantifiedConstraints¹已经登陆GHC 8.6,我正在阅读最初建议的衍生类型(第7节) ².但是,在操作方面,我无法理解如何QuantifiedConstraints将其翻译成字典.以下是该文件的摘录.

我们需要的是一种简化谓词的方法 f (GRose f a).诀窍是采取我们在Binary (List a)上面假设的"常量"实例声明,并对其进行抽象:

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))为just Binary (GRose f a),我们有一个实例声明.

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

特别是我不能理解以下内容:

1)将谓词简化Binary (f (GRose f a))为just 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))为just Binary (GRose f a)

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