haskell - 通过蕴涵削弱黑胶唱片的 RecAll 约束

Question

在 vinyl图书馆，有一个RecAll类型族，让我们要求部分应用的约束对于类型级别列表中的每个类型都是正确的。例如，我们可以这样写:

myShowFunc :: RecAll f rs Show => Rec f rs -> String

这一切都很可爱。现在，如果我们有约束 RecAll f rs c在哪里 c是未知的，我们知道 c x包含 d x (借用ekmett的 contstraints包的语言)，我们怎样才能得到 RecAll f rs d ?

我问的原因是我正在处理一些需要满足几个类型类约束的函数中的记录。为此，我使用 :&:来自 Control.Constraints.Combine 的组合器 exists 中的模块包裹。 (注意:如果您安装了其他东西，该软件包将无法构建，因为它依赖于 contravariant 的 super 旧版本。不过，您可以复制我提到的一个模块。)有了这个，我可以得到一些非常漂亮的东西约束，同时最小化 typeclass broilerplate。例如:

RecAll f rs (TypeableKey :&: FromJSON :&: TypeableVal) => Rec f rs -> Value

但是，在这个函数的主体内部，我调用了另一个需要较弱约束的函数。它可能看起来像这样:

RecAll f rs (TypeableKey :&: TypeableVal) => Rec f rs -> Value

GHC 看不到第二个语句是从第一个语句开始的。我以为会是这样。我看不到的是如何证明它以实现它并帮助 GHC。到目前为止，我有这个:

import Data.Constraint

weakenAnd1 :: ((a :&: b) c) :- a c                                                                    
weakenAnd1 = Sub Dict -- not the Dict from vinyl. ekmett's Dict.

weakenAnd2 :: ((a :&: b) c) :- b c                                                                    
weakenAnd2 = Sub Dict

这些工作正常。但这就是我卡住的地方:

-- The two Proxy args are to stop GHC from complaining about AmbiguousTypes
weakenRecAll :: Proxy f -> Proxy rs -> (a c :- b c) -> (RecAll f rs a :- RecAll f rs b)
weakenRecAll _ _ (Sub Dict) = Sub Dict

这不编译。有没有人知道一种方法来获得我正在寻找的效果。如果它们有帮助，这里是错误。另外，我有 Dict作为我实际代码中的合格导入，这就是它提到 Constraint.Dict 的原因:

Table.hs:76:23:
    Could not deduce (a c) arising from a pattern
    Relevant bindings include
      weakenRecAll :: Proxy f
                      -> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
        (bound at Table.hs:76:1)
    In the pattern: Constraint.Dict
    In the pattern: Sub Constraint.Dict
    In an equation for ‘weakenRecAll’:
        weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict

Table.hs:76:46:
    Could not deduce (RecAll f rs b)
      arising from a use of ‘Constraint.Dict’
    from the context (b c)
      bound by a pattern with constructor
                 Constraint.Dict :: forall (a :: Constraint).
                                    (a) =>
                                    Constraint.Dict a,
               in an equation for ‘weakenRecAll’
      at Table.hs:76:23-37
    or from (RecAll f rs a)
      bound by a type expected by the context:
                 (RecAll f rs a) => Constraint.Dict (RecAll f rs b)
      at Table.hs:76:42-60
    Relevant bindings include
      weakenRecAll :: Proxy f
                      -> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
        (bound at Table.hs:76:1)
    In the first argument of ‘Sub’, namely ‘Constraint.Dict’
    In the expression: Sub Constraint.Dict
    In an equation for ‘weakenRecAll’:
        weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict

Answer 1

让我们首先回顾一下 Dict和 (:-)旨在使用。

ordToEq :: Dict (Ord a) -> Dict (Eq a)
ordToEq Dict = Dict

值的模式匹配 Dict类型 Dict (Ord a)带来约束 Ord a进入范围，从中 Eq a可以推导出(因为 Eq 是 Ord 的父类(super class))，所以 Dict :: Dict (Eq a)是很好的类型。

ordEntailsEq :: Ord a :- Eq a
ordEntailsEq = Sub Dict

同样， Sub在参数的持续时间内将其输入约束带入范围，允许 Dict :: Dict (Eq a)也可以很好地打字。

然而，虽然 Dict 上的模式匹配将约束带入范围， Sub Dict 上的模式匹配没有将一些新的约束转换规则纳入范围。事实上，除非输入约束已经在范围内，否则无法在 Sub Dict 上进行模式匹配。一点也不。

-- Could not deduce (Ord a) arising from a pattern
constZero :: Ord a :- Eq a -> Int
constZero (Sub Dict) = 0

-- okay
constZero' :: Ord a => Ord a :- Eq a -> Int
constZero' (Sub Dict) = 0

这解释了您的第一个类型错误， "Could not deduce (a c) arising from a pattern" : 您尝试在 Sub Dict 上进行模式匹配, 但输入约束 a c尚未在范围内。

当然，另一种类型的错误是说您确实设法进入范围的约束不足以满足 RecAll f rs b约束。那么，需要哪些部分，哪些部分缺失？我们来看看 RecAll的定义.

type family RecAll f rs c :: Constraint where
  RecAll f [] c = ()     
  RecAll f (r : rs) c = (c (f r), RecAll f rs c)

啊哈! RecAll是一个类型族，因此未经评估，具有完全抽象的 rs , 约束 RecAll f rs c是一个黑盒子，不能从任何较小的部分中得到满足。一旦我们专业 rs至 []或 (r : rs) ，很明显我们需要哪些部分:

recAllNil :: Dict (RecAll f '[] c)
recAllNil = Dict

recAllCons :: p rs
           -> Dict (c (f r))
           -> Dict (RecAll f rs c)
           -> Dict (RecAll f (r ': rs) c)
recAllCons _ Dict Dict = Dict

我正在使用 p rs而不是 Proxy rs因为它更灵活:如果我有一个 Rec f rs ，例如我可以用它作为我的代理 p ~ Rec f .

接下来，让我们用 (:-) 实现上面的一个版本。而不是 Dict :

weakenNil :: RecAll f '[] c1 :- RecAll f '[] c2
weakenNil = Sub Dict

weakenCons :: p rs
           -> c1 (f r) :- c2 (f r)
           -> RecAll f rs c1 :- RecAll f rs c2
           -> RecAll f (r ': rs) c1 :- RecAll f (r ': rs) c2
weakenCons _ entailsF entailsR = Sub $ case (entailsF, entailsR) of
    (Sub Dict, Sub Dict) -> Dict

Sub带来其输入约束 RecAll f (r ': rs) c1在它的参数持续时间内进入范围，我们已经安排它包括函数体的其余部分。类型族的方程 RecAll f (r ': rs) c1扩展到 (c1 (f r), RecAll f rs c1) ，因此它们也都被纳入范围。它们在范围内的事实允许我们在两个 Sub Dict 上进行模式匹配。 ，还有那两个 Dict将它们各自的约束纳入范围: c2 (f r) , 和 RecAll f rs c2 .这两个正是目标约束 RecAll f (r ': rs) c2扩展到，所以我们的 Dict右边是很好的类型。

完成我们对 weakenAllRec 的实现，我们需要在 rs 上进行模式匹配以确定是否将工作委托(delegate)给 weakenNil或 weakenCons .但是自从 rs在类型级别，我们不能直接对其进行模式匹配。 Hasochism论文解释了如何在类型级别上进行模式匹配 Nat ，我们需要创建一个包装器数据类型 Natty .方式 Natty有效的是，它的每个构造函数都由相应的 Nat 索引。构造函数，所以当我们对 Natty 进行模式匹配时值级别的构造函数，相应的构造函数也隐含在类型级别。我们可以为类型级列表定义这样的包装器，例如 rs , 但恰好 Rec f rs已经有与 [] 对应的构造函数和 (:) ，以及 weakenAllRec 的调用者无论如何，很可能会有一个躺在那里。

weakenRecAll :: Rec f rs
             -> (forall a. c1 a :- c2 a)
             -> RecAll f rs c1 :- RecAll f rs c2
weakenRecAll RNil       entails = weakenNil
weakenRecAll (fx :& rs) entails = weakenCons rs entails
                                $ weakenRecAll rs entails

注意 entails 的类型必须是 forall a. c1 a :- c2 a ，而不仅仅是 c1 a :- c2 a ，因为我们不想声称 weakenRecAll适用于任何 a调用者的选择，而是我们希望要求调用者证明 c1 a包含 c2 a对于每个 a .