通过蕴含削弱乙烯基的 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 module in the exists 包中的 :&: 组合器。（注意：如果你安装了其他东西，这个包将不会构建，因为它依赖于 contravariant 的超旧版本。你可以只复制我提到的那个模块。）有了这个，我可以得到一些非常漂亮的约束，同时最小化类型类烤盘。例如：

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 (Ord a) 类型的值 Dict 的模式匹配将约束 Ord a 引入范围，从中可以推导出 Eq a（因为 Eq是 Ord 的超类），因此 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 进行模式匹配，以确定是将工作委托给 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.

通过蕴含削弱乙烯基的 RecAll 约束

Weakening vinyl's RecAll constraint through entailment

haskell

constraints

ghc

vinyl