7

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

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

这一切都很可爱。现在，如果我们有未知的约束RecAll f rs c，c并且我们知道c x蕴含d x（从 ekmett 的约束包中借用语言），我们怎么能得到RecAll f rs d？

我问的原因是我正在处理一些需要满足几个类型类约束的函数中的记录。为此，我使用了exists包中Control.Constraints.Combine模块中的:&:组合器。（注意：如果您安装了其他东西，则该软件包将不会构建，因为它依赖于. typeclass broilerplate。例如：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
4

1 回答 1

12

让我们首先回顾一下如何使用Dict以及如何(:-)使用。

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

Dict对类型值的模式匹配Dict (Ord a)将约束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于[]or (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已经有对应于[]and(:)的构造函数，并且调用者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

请注意，entailsmust的类型forall a. c1 a :- c2 a不仅是c1 a :- c2 a，因为我们不想声称这对调用者的weakenRecAll任何a选择都有效，而是我们希望要求调用者证明对 every的c1 a蕴含。c2 aa

于 2015-04-28T04:08:12.920 回答