通过蕴涵削弱乙烯基的召回约束

Question

在vinyl库中，有一个recall类型族，让我们询问，对于类型级别列表中的每个类型，部分应用的约束都是真的。例如，我们可以这样写：

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

这一切都很可爱。现在，如果我们有约束recallfrsc，其中c是未知的，并且我们知道cx包含dx（借用Ekmett的contstraints包的语言），那么我们如何获得recallfrsd呢？

我问的原因是我正在处理一些函数中的记录，这些函数需要满足几个类型类约束。为此，我使用了exists包中Control.Constraints.Combine模块中的:&:组合子。（注意：如果您安装了其他功能，则该包将无法构建，因为它依赖于contravariant的超旧版本。不过，您可以复制我提到的一个模块。）这样，我就可以在最小化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

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(EQA)具有良好的类型。

然而，虽然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 desduce（a c）ering from a pattern”:您尝试对sub dict进行模式匹配，但输入约束a c不在作用域中。

当然，另一个类型错误是，您设法进入范围的约束不足以满足recallfrsb约束。那么，哪些是需要的，哪些是缺失的呢？让我们看看recall的定义。

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

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

接下来，让我们用(:-)而不是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将其输入约束recallf(r':rs)c1在其参数的持续时间内纳入作用域，我们已安排该作用域包括函数主体的其余部分。类型族recallf(r':rs)c1的方程扩展到(c1(Fr)，recallfrsC1)，因此它们也被纳入范围。它们在作用域中的事实允许我们对两个sub dict进行模式匹配，这两个dict将它们各自的约束纳入作用域:C2(fr)和recallfrsc2。这两个正是目标约束recallf(r':rs)c2扩展到的，因此我们的dict右侧的类型很好。

要完成weakenallrec的实现，我们需要对rs进行模式匹配，以便确定是将工作委托给weakenil还是weakencons。但是由于rs是类型级别的，我们不能直接对其进行模式匹配。Hasochism论文解释了为了在类型级别的NAT上进行模式匹配，我们需要创建一个包装数据类型NATTY。natty的工作方式是，它的每个构造函数都由相应的nat构造函数索引，因此当我们在值级别对natty构造函数进行模式匹配时，相应的构造函数也在类型级别隐含。我们可以为类型级列表（如rs）定义这样的包装器，但恰好rec frs已经有了与[]和(:)相对应的构造函数，而且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的类型必须为。c1 a:-c2 a，而不仅仅是c1 a:-c2 a，因为我们不想声称weakenrecall对调用方选择的任何a都有效，而是我们想要求调用方证明c1 a对每个a都包含c2 a。